# Questions tagged [parametricity]

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

23 questions
Filter by
Sorted by
Tagged with
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$ (...
• 389
3 votes
3 answers
189 views

• 389
4 votes
1 answer
180 views

### What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this: funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2 One may ...
• 1,187
5 votes
2 answers
189 views

### Relating functors to relational functors with the parametricity translation

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
• 195
1 vote
1 answer
202 views

### Extended Church's thesis and internal parametricity

I am wondering if there is any known relationship between these 2 concepts in intensional MLTT as formulated here. Does $Internal\ parametricity \implies ECT$ hold? For forumlation of ECT see https://...
• 920
7 votes
2 answers
436 views

• 32.5k
16 votes
4 answers
766 views

### Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
• 1,092
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 ...