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
3 votes
3 answers

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. ...
2 votes
2 answers

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

This question is similar to Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$? but looks more complicated. It is about using relational ...
3 votes
3 answers

How to prove `(∀(M : Monad). ∀a. a → M a) ≅ 𝟙`

Just like the title says, how to prove that equation? The equation basically says that there is only one function a -> M a parametric in both ...
3 votes
1 answer

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$ (...
8 votes
1 answer

Is is true that every monad transformer is equivalent to its underlying/base monad?

Question originally asked in proofassistants.stackexchange Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-...
3 votes
1 answer

Is Linear Evaluation Parametric?

Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
4 votes
1 answer

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 ...
6 votes
0 answers

List Functions That Don't Depend on Length

Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
5 votes
2 answers

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 ...
20 votes
4 answers

How can relational parametricity be motivated?

Is there some natural way to understand the essence of relational semantics for parametric polymorphism? I have just started reading about the notion of relational parametricity, a la John Reynolds' ...
3 votes
1 answer

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.\, (...
7 votes
2 answers

Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

There are many closed terms of a given type. For instance, both of these terms: $$ \lambda x . x $$ $$ \lambda x . (\lambda y . y) x $$ have a type of a polymorphic identity function: $$ \forall X ....
7 votes
2 answers

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which ...
1 vote
1 answer

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://...
16 votes
4 answers

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( In this paper, they internalize unary ...
10 votes
1 answer

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 ...
9 votes
1 answer

Where is relational parametricity in hyperdoctrine or topos models explored?

Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. ...
13 votes
1 answer

Why Reflexive Graphs for Parametricity?

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used? In particular, why do they not include relational composition? In looking at the models, they ...
1 vote
1 answer

What's the relationship between "free theorems" and "free objects"

What's the relationship between free theorems and free objects from algebra. They seem quite similar. I'm wondering if there's an underlying principle here.
7 votes
1 answer

Decidability of parametric higher-order type unification

I'm making a language that has higher-kinded types (like Haskell) and allows type synonyms to appear partially applied in type expressions (unlike Haskell). As an example, consider the following ...
18 votes
1 answer

Parametricity and projective eliminations for dependent records

It's well-known that in System F, you can encode binary products with the type $$ A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha $$ You can then define projection functions $\...
12 votes
1 answer

Natural Transformations and Parametricity

In Theorems for Free!, Wadler says that the characterization of parametricity can be re-expressed in terms of lax natural transformations and this will be the subject of a further paper. Which paper ...
33 votes
4 answers

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 ...