Skip to main content
3 votes

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism. Take a model of computatation (an "...
Andrej Bauer's user avatar
  • 28.9k
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

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
1 vote
Accepted

Formalising Church numerals in Agda

I think your neutral-bad lemma is too general. For instance: $$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$ $σ$ does not occur in the context, but there is a neutral term with its ...
Dan Doel's user avatar
  • 1,021
1 vote

How do continuations represent negations (under the Curry–Howard correspondence)?

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of ...
NinjaDarth's user avatar

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