7
votes
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 ...
- 11.7k
7
votes
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 ...
- 185
7
votes
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 ...
- 197
5
votes
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 ...
- 13.7k
5
votes
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 ...
- 28.3k
4
votes
Accepted
Is Linear Evaluation Parametric?
Here's an Agda formalization of the non-linear version of your argument, and my comment above:
...
- 921
4
votes
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 ...
- 1,444
3
votes
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 &...
- 244
2
votes
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,653
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 ...
- 244
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 ...
- 244
Only top scored, non community-wiki answers of a minimum length are eligible