Questions tagged [parametricity]

Parametricity is the semantic theory of parametrically polymorphic functions, i.e., functions parameterized by type parameters.

Filter by
Sorted by
Tagged with
33 votes
4 answers
3k views

What are the differences between logical relations and simulations?

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...
Hongjin Liang's user avatar
10 votes
1 answer
357 views

Parametricity of Linear Logic

Are we able to prove a free parametricity theorems about functions like $f : \forall A . [A] ⊸ [A]$? It is supposed to state that $f$ takes a list and always returns a permutation of it. Another ...
Łukasz Lew's user avatar
  • 1,187
3 votes
1 answer
149 views

Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F. Consider the following types of polymorphic functions: $$ \forall a.\, (...
winitzki's user avatar
  • 389
3 votes
3 answers
189 views

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F. Consider the following type of polymorphic functions: $$T = \forall a. ...
winitzki's user avatar
  • 389
3 votes
1 answer
206 views

How to encode a function from an existential type

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work. It is known that an existential type $\exists t.~P~t$ (...
winitzki's user avatar
  • 389