New answers tagged

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
0 votes

Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?

Another proof technique that is more intuitive in my biased opinion is to enumerate normal forms of System F terms of the given type. The most interesting example among those five given is $\forall a. ...
Li-yao Xia's user avatar
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

Top 50 recent answers are included