Skip to main content
8 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 ...
Nick Rioux's user avatar
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 ...
D.W.'s user avatar
  • 12.2k
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 ...
gadmm's user avatar
  • 307
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 ...
cody's user avatar
  • 13.9k
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 ...
Andrej Bauer's user avatar
  • 29.2k
4 votes
Accepted

Is Linear Evaluation Parametric?

Here's an Agda formalization of the non-linear version of your argument, and my comment above: ...
Dan Doel's user avatar
  • 1,021
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 ...
András Kovács's user avatar
3 votes
Accepted

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation ...
Li-yao Xia's user avatar
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 &...
winitzki's user avatar
  • 542
3 votes
Accepted

How to encode a function from an existential type

Using function extensionality, it suffices to prove: $$∀ Z\ z. e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ z$$ The naturality rule for $e$ is: $$f\ (e\ A\ k) = e\ B\ (ΛR. λr. f\ (k\ R\ r))$$ If we pick $k =...
Dan Doel's user avatar
  • 1,021
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$ ...
Max New's user avatar
  • 1,695
2 votes

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

Using syntactic methods, it's quite easy to see the correspondence between $\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$ and $1 + 2 + 3 + \dots$ You already had that intuition, and it ...
Li-yao Xia's user avatar
2 votes
Accepted

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

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$ The ...
winitzki's user avatar
  • 542
1 vote

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Is this not just confusion about notation? If the notation (X, y) is used to signify the introduction rule for then it does ...
Andrej Bauer's user avatar
  • 29.2k
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 ...
winitzki's user avatar
  • 542
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 ...
winitzki's user avatar
  • 542

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