# Tag Info

### What's the relationship between "free theorems" and "free objects"

There is no relationship. They both use the word "free", but with different meanings of the word "free". It's just an accidental collision, which will happen when you have a language like English ...
Accepted

### Parametricity of Linear Logic

Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem here. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For ...

### Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

I'd like to offer some pointers. Is there any research that goes along these lines and perhaps formalizes this intuition? Parametricity by analysis of the shape of (simply-typed) normal forms ...
Accepted

### Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity $\Rightarrow$ Normalization), and the post by Gabriel is somewhat involved, but in ...
Accepted

### Extended Church's thesis and internal parametricity

Internal parametricity does not entail any version of extended Church's thesis. To see this, consider a presheaf model of internal parametricity, for example this one, and observe that in any presheaf ...
Accepted

### Is Linear Evaluation Parametric?

Here's an Agda formalization of the non-linear version of your argument, and my comment above: ...

### Relating functors to relational functors with the parametricity translation

$(F, F^R)$ is not necessarily a relational functor. Define $F : \text{Set} \to \text{Set}$ to be the identity functor on sets and functions, but let ${F_!}^R$ send all relations to the trivial ...
Accepted

### Is is true that every monad transformer is equivalent to its underlying/base monad?

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that &...
Accepted

### Why Reflexive Graphs for Parametricity?

In the months since I asked this question, I think I have found a sensible answer. Often, the type of relations considered do not compose. For instance, if your notion of a relation $R : D \to E$ ...
1 vote
Accepted

### Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?

The solution was suggested in a comment by @DanDoel. Flip the first two curried arguments in the type: $$\forall a.\,((a\rightarrow r)\rightarrow s) \rightarrow(a\rightarrow r)\rightarrow s$$ and ...
1 vote

### What is the relation of parametricity and function extensionality?

Indeed there is a similarity in these two definitions. Function extensionality that you showed is just a condition that specifies when two functions are equal. If we talk about logical relations then ...

Only top scored, non community-wiki answers of a minimum length are eligible