Skip to main content
13 votes

Rigorous proof that parametric polymorphism implies naturality using parametricity?

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's. For $F : \text{Type} \to \text{Type}$, this says that if the ...
András Kovács's user avatar
8 votes
Accepted

Why do we need a separate notation for П-types?

I think we just need to get some things straight here: In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a ...
Andrej Bauer's user avatar
  • 30.9k
7 votes

Higher-ranked polymorphism without explicit application or subtyping?

The Dunfield & Krishnaswami paper's introduction refers to Practical type inference for arbitrary-rank types As can be seen, it scales well to advanced type systems; moreover, it is easy to ...
phadej's user avatar
  • 171
6 votes
Accepted

Can String be a subtype of Character in a programming language?

Character and String are conceptually very, very different. Google for "inheritance vs. composition" - you seem to think that Character and String should be connected via inheritance, but in reality a ...
gnasher729's user avatar
  • 30.7k
5 votes

How can an existential type be defined in terms of universal type?

As a general recipe, to figure out how to encode a type A, write down ∀Z . (A → Z) → Z and massage it to something that does ...
Andrej Bauer's user avatar
  • 30.9k
5 votes

What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

$$\newcommand{\expr}{\mathsf{expr}} \newcommand{\int}{\mathbf{Int}} \newcommand{\List}{\mathbf{List}} \newcommand{\let}{\mathbf{let}} \newcommand{\id}{\mathsf{id}} \newcommand{\in}{\mathbf{in}} \...
Dan Doel's user avatar
  • 2,707
5 votes
Accepted

What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?

You seem to have been confounded by many related and similar but crucially different concepts! Let me attempt to explain them one at a time. Parametric polymorphism is the ability to write types that ...
xuq01's user avatar
  • 1,190
5 votes

How exactly do we define parametric polymorphism?

An informal, but better way of explaining parametric polymorphism is that the term has a uniform definiton/semantics for all types. A simple example is the identity function: $$λ x. x$$ This is one ...
Dan Doel's user avatar
  • 2,707
5 votes
Accepted

Relationship between Higher Kinded Polymorphism, type inference, and Currying

I imagine what the comment writer is referring to is this... Consider type inference in Haskell. At some point, we may be asked to solve the unification problem ...
Dan Doel's user avatar
  • 2,707
5 votes

What's the advantage of "value restriction" over its alternatives?

I'm sure that this isn't the only advantage, but I think the primary advantage is simplicity. This is even identified in the original paper introducing the value restriction: previous solutions all ...
Joey Eremondi's user avatar
5 votes
Accepted

Is subtype polymorphism a kind of ad hoc polymorphism?

Strachey's paper defines only two main classes of polymorphism. Subtyping is certainly not parametric polymorphism, so either subtyping is a form of the remaining class or Strachey's terms are not as ...
itsbruce's user avatar
  • 224
5 votes

Is subtype polymorphism a kind of ad hoc polymorphism?

Keep in mind that, in PL lingo, the term "polymorphism" is used for different notions. In OOP, polymorphism usually means subtype polymorphism. If we have a function ...
chi's user avatar
  • 14.6k
4 votes

Can String be a subtype of Character in a programming language?

Subtyping is conceptually very different from inheritance. Subtyping refers to shared interfaces; $\tau$ is a subtype of $\tau'$, i.e. $\tau <: \tau'$, then all expressions of type $\tau$ could be ...
xuq01's user avatar
  • 1,190
4 votes

Is subtype polymorphism a kind of ad hoc polymorphism?

They're definitely different things, which is easier to see with a clearer definition of ad-hoc polymorphism. Quoting from Wikipedia: ...ad hoc polymorphism is a kind of polymorphism in which ...
Luke Mathieson's user avatar
4 votes
Accepted

What's the difference between Row Polymorphism and Structural Typing?

Structural type systems don't necessarily have anything to do with records. For instance, you could have a system where: ...
Dan Doel's user avatar
  • 2,707
4 votes

Uncurrying and Polymorphism

The other answers are good, I just wanted to make it explicit that currying for dependent types is $$ \textstyle \prod (x : A) . \prod (y : B(x)) . C(x, y) \ \cong \ \prod (p : \sum (x : A) . B(x)) . ...
Andrej Bauer's user avatar
  • 30.9k
3 votes

What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?

The notation is explained in your course material, e.g. here starting on slide 47. In the notation $$T = \forall \alpha_1, \dots, \alpha_n.\tau$$ $\alpha_i$ are type variables, the $\tau$ is a ...
siracusa's user avatar
  • 360
3 votes
Accepted

Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?

You can see an instance of the claimed property in the two definitions of add3. In the ADT style, add3 is defined as: ...
Ptival's user avatar
  • 171
3 votes

How to implement polymorphism in a turing complete environment?

So, first, a question. Are you using dynamic or static dispatch? i.e. if Circle and Shape provide implementations of the same ...
Joey Eremondi's user avatar
3 votes

Higher-ranked polymorphism without explicit application or subtyping?

To check the application of a function like g : (forall a. a -> a) -> Int to f, we need to check that ...
Li-yao Xia's user avatar
2 votes
Accepted

how type checking fails?

I finally figured it out. The key is using sub-typing rules. ...
alim's user avatar
  • 1,014
2 votes
Accepted

Can a $k$-ary relation have polymorphisms of arity greater than $k$?

Let's say that there's a [$k$-ary] relation $R$ and [$m$-ary] function $f$ such that $m>k$. Is $f$ a polymorphism of $R$? Maybe, maybe not: it depends on the function and the relation. A given $k$...
David Richerby's user avatar
2 votes

How exactly do we define parametric polymorphism?

A useful intuition is the one you described: the code of a parametric-polymorphic function f can not access type T and choose to ...
chi's user avatar
  • 14.6k
2 votes

How exactly do we define parametric polymorphism?

Contrary to what you wrote, in many languages with parametric polymorphism, the type usually is not provided as an argument to the function. At least, it's not like the other arguments. You can't ...
D.W.'s user avatar
  • 162k
2 votes
Accepted

Are type abstraction values and universal types not for non functions, but only for functions?

Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example ...
nekketsuuu's user avatar
2 votes
Accepted

Why are all polymorphic functions between functors natural transformations?

I think the easiest thing is to refer you to the famous Theorems for free! paper, which explains the intuition behind the use of the Reynolds parametricity theorem. Intuitively, in System $\mathrm F$ ...
cody's user avatar
  • 8,233
2 votes

Are type variables really only used in mathematical conversation about types?

I am not sure I understand your question, but I believe the answer is "yes". When describing monomorphic languages, an expression such as let id x = x : τ (...
Arthur Azevedo De Amorim's user avatar
2 votes

Uncurrying and Polymorphism

The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{Y})$ and the adjoint of $(\forall X.)$ is $(\exists X.)$, it is appearently inevitable. Also, ...
Trebor's user avatar
  • 170
2 votes

Rigorous proof that parametric polymorphism implies naturality using parametricity?

$\newcommand{\Type}{\text{Type}}\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}\newcommand{\map}{\text{map}}$ Note: This answer is not a standalone answer, but an incomplete attempt to give some ...
Couchy's user avatar
  • 191
1 vote

Uncurrying and Polymorphism

I can only think of some uncurrying of 1 and 3. $\forall X. (X \times int) \rightarrow X$ It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1. $int \...
chi's user avatar
  • 14.6k

Only top scored, non community-wiki answers of a minimum length are eligible