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
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
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
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 ...
Russoul's user avatar
  • 229
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-...
Russoul's user avatar
  • 229
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 ...
vigenary's user avatar
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 ...
vigenary's user avatar
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 ...
winitzki's user avatar
  • 389
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
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 ...
Łukasz Lew's user avatar
  • 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 ...
Couchy's user avatar
  • 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://...
Ilk's user avatar
  • 920
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 ....
Łukasz Lew's user avatar
  • 1,187
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
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 ...
Max New's user avatar
  • 1,685
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.
Steven Shaw's user avatar
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 ...
isekaijin's user avatar
  • 501
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. ...
Tom Ellis's user avatar
  • 511
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 ...
sonat's user avatar
  • 381
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' ...
Tom Ellis's user avatar
  • 511
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 ...
user13264's user avatar
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 $\...
Neel Krishnaswami's user avatar
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 ...
Christopher Monsanto's user avatar
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