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


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


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


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


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

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 "...


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


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

$(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 relation. Then ${F_{\text{map}}^R}$ trivially holds (along with ${F_{\text{id}}^R}$ and ${F_{\text{comp}}^R}$ which always hold for any $F$, because of the proof-...


2

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