22

Well, relational parametricity is one of the most important ideas introduces by John Reynolds, so it shouldn't be too much of a surprise that it looks like magic. Here is a fairy tale about how he might have invented it. Suppose you're trying to formalize the idea that certain functions (identity, map, fold, reversal of lists) act "the same way on many ...


14

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.


11

The answer to your question is really there in Reynolds's fable (Section 1). Let me try and interpret it for you. In a language or formalism in which types are treated as abstractions, a type variable can stand for any abstract concept whatsoever. We don't assume that types are generated via some syntax of type terms, or some fixed collection of type ...


10

For technical reasons, there hasn't been much work on parametric topos models. The internal logic of a topos is a form of set theory, and F-style impredicative indexing and the powerset axiom are incompatible. See Andy Pitts's Non-trivial Power Types Can't Be Subtypes of Polymorphic Types: This paper establishes a new, limitative relation between the ...


9

No, it's not decidable. The pure simply-typed lambda calculus is parametric in your sense (it has no case analysis) and higher-order unification is undecidable. In general, permitting partial application of type synonyms is equivalent to adding lambda-abstraction to the language of type expressions. This is because type synonyms suffice to encode the SKI ...


8

Unfortunately, the remark of Wadler is too cryptic for me to tell what use he wanted to make of "lax natural transformations". Here is a guess. Relation-preservation squares can often be recast as lax commutative squares. This is how they used to be written in old automata theory papers/books. See paragraph 1.2 in my Notes on Semigroups. To do this kind ...


7

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 example, if you have $A, x : [A], y : [A] \vdash e : [A]$, then in an ordered type system, $e$ must append the lists $x$ and $y$. The short answer is that yes, we ...


7

I'm quite fond of Wadler's paper The Girard-Reynolds Isomorphism which shows that there is a translation from system $\mathrm{F}$ to and from Second Order Predicate Logic (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type. ...


6

I just talked to Dan Doel and he explained that his reference was in fact one Neel Krishnaswami. He saw a comment on n-cafe by you that one could do strong induction using parametricity, so he went ahead and did it as an exercise, not realizing that doing it for sigma was apparently a novel result. The precise quote: "My reference was him. I thought he said ...


6

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 with a fixed number of words and the number of concepts we want to talk about exceeds the number of words in the language. A free group is, roughly, a group that ...


5

This should be a comment to Neel's answer, but it's a bit long. Prompted by a hint from Rasmus Petersen, I found the following in Møgelberg's thesis (emphasize mine): Ivar Rummelhoff [36] has studied the encoding of natural numbers in per-models over different PCA’s, and showed that in some of these models, the encoding contains more than natural ...


5

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 preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique ...


4

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 model of type theory the extended Church's thesis fails (both the internal and the external one) because the object $\mathbb{N}^\mathbb{N}$ has uncountably ...


4

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 system F one can do a relatively straightforward induction. I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "...


3

Another possible answer different from Andrej's is the given by the example of the $\omega$-set model of polymorphism. Since every function in the polymorphic calculus is computable, it's natural to interpret a type by a set of numbers which represent the computable functions of that type. Furthermore, it's tempting to identify functions with the same ...


3

Let me a bit more abstract in answering this. At each arity $n$, you have the following situation: $n$-ary relations $R$ can be embedded into $(n+1)$-ary relations by defining $R'(\vec{x},y) \iff R(\vec{x}) \land y = x_i$ (for some fixed $i \in [1..n]$). In words, you can use some $n$ arguments out of the $n+1$ arguments for simulating the smaller relation ...


1

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$ between $\omega$CPOs is an $\omega$-chain complete subset of $|D|\times |E|$, then the relation $R : \omega + 1 \to \mathbb{N}$ between the ordered naturals plus ...


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