Zulip Chat Archive

Stream: general

Topic: notes on parametricity

Reid Barton (Apr 28 2018 at 06:30):

Since the subject of parametricity came up, here are some papers which may be of interest and should be relatively readable for mathematicians (especially those who are also Lean users). These papers pertain to non-dependently typed languages; I don't know what differences there might be in the dependently typed setting.

Johan Commelin (Apr 28 2018 at 07:01):

Reid, thanks for those links. The Fable about complex numbers was a good illustration.

Johan Commelin (Apr 28 2018 at 07:05):

However, I think it is slightly different from transport of structure

Mario Carneiro (Apr 28 2018 at 08:26):

Theorems for free! is exactly the paper that covers the right generic approach to parametricity

Reid Barton (Apr 28 2018 at 17:06):

@Johan Commelin You're right that what those papers talk about isn't quite transport of structure. Instead it's the question about transfer of structure commuting with user-defined functions. For example the free theorem for list implies in particular that any defined function of type list a \to list a must commute with the "transfer of structure" equivalence list a \simeq list b that arises from an equivalence a \simeq b.

Reid Barton (Apr 28 2018 at 17:07):

(The "transfer of structure" equivalence in this case just being the list map function.)

Reid Barton (Apr 28 2018 at 17:11):

I think the reason that the scope does not extend to transfer of structure itself is that in the languages used in those papers, type constructors like list : Type \to Type are not definable, or at least do not have the same status as value-level functions, and so they are not in the universe of things to which one might apply parametricity theorems.

Reid Barton (Apr 28 2018 at 17:14):

But I guess if you extend the idea of parametricity to a setting (like Lean) where you can have user-defined functions which produce Type, then you get a parametricity result which is "one category level higher" in that it produces an equivalence between two types, rather than an equation between two values

Johan Commelin (Apr 28 2018 at 17:58):

I see. I'm going to give Wadlers "Theorems for free" a close look. I think it contains important ideas.

Last updated: Dec 20 2023 at 11:08 UTC