Parametricity

Stream: Is there code for X?

[Patrick Nicodemus]

Is there a tool to derive the parametricity translation of a structure or a typeclass?

[Aaron Liu]

What is parametricity translation?

[Patrick Nicodemus]

The parametricity translation is a map from definitions to definitions. It has been worked out on paper for dependent type theories which are pure type systems, it should be possible to handle some reasonable fragment of Lean and fail if it encounters some aspect of the language which it doesn't know how to handle.

it is easier to show some simple examples:

def abc (A : Type) (a : A) := a

would be translated to

def abc_param (A B : Type) (R : A->B->Type) (a : A) (b : B) (r : R a b) := r

So the translation sends type variables to pairs of type variables with a binary relation between them, and elements of types to related pairs of elements of types.

If D is the definition of an algebraic structure, say the type Widget, then the parametricity translation applied to D should return a function Widget -> Widget -> Type which associates to two widgets S, S' the type of spans S <- W -> S' in the category of widgets and widget homomorphisms.

For example, in theory it should be possible to plug in, say, the definition of a category, and get out a definition which sends two categories C, C' to the type of spans between them in the category Cat.

[Aaron Liu]

sounds like a lot of metaprogramming might get you a good approximation

[Markus Himmel]

I believe that @Vincent Kuhlmann is working on this.

[Vincent Kuhlmann]

Yes that is correct. Thanks for noticing Markus! It will be finished in a month or two :)