The 2024 Developer Survey results are live! See the results

# Questions tagged [parametricity]

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

26 questions
Filter by
Sorted by
Tagged with
113 views

### Can parametricity be applied to show a property of function values?

Say I have the following dictionary of abstract operations, written in Haskell for relatively concise notation: ...
129 views

### How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Following Wadler's paper "Recursive types for free" and having spent some months on reconstructing the proof that $\exists A. ~ A \times (A\to F~ A)$ is the terminal $F$-coalgebra, I am ...
• 552
89 views

### Is the encoding of existential types in System F adequate?

This is somewhat related to How to encode a function from an existential type Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the ...
• 552
240 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$ (...
• 552
205 views

• 552
189 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
195 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
204 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
437 views

• 32.8k