# Tag Info

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 ...
• 225

### 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 ...
• 12.2k

### 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 ...
• 307
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.9k
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 ...
• 29.2k
Accepted

### Is Linear Evaluation Parametric?

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

### 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,639
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 ...
• 206
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 &...
• 542
Accepted

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 =... • 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$... • 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 ... • 206 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 ... • 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 ... • 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 ...
• 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 ...
• 542

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