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

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
361 views

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

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
74 views

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

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

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

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
857 views

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
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://...
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 ...
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 ...
9 votes
1 answer
366 views

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
404 views

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
94 views

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
393 views

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
472 views

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
912 views

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