Talk:Parametric polymorphism

"Let-polymorphism".

Does the let in the term let-polymorphism refer to some ML dialects' use of let to mean what Standard ML calls val? For a long time I was confused because I didn't see what it has to do with what SML called let, but I recently learned that OCaml uses let for val, and suddenly it seems to make sense . . . —Ruakh_TALK 06:48, 15 August 2013 (UTC)

Milner's original type inference algorithm worked on an idealized programming language: a lambda-calculus with let-bindings. These let-bindings correspond approximately to SML's val-bindings, although things get a bit more tricky when you also have to take mutually recursive definitions and the value restriction into account. —Ruud 14:30, 15 August 2013 (UTC)

Traits and Parametric Polymorphism

After reading through this article, and the article on trait (computer programming), I'm having trouble distinguishing between the two concepts: they seem to be talking about the same thing, as best as I can tell. This article takes a decidedly computer-sciencey type-theoretic tack in it's presentation, while the article on traits seems to be more along the lines of ordinary programmers trying to wrap their minds around some new-fangled buzz-word. If there are differences, could these be explained? Could some examples be given? If it really is the same concept, could some clarifying discussion be added? 67.198.37.16 (talk) 16:15, 30 December 2021 (UTC)

They do have in common the underlying concept of polymorphism, but they are different concepts. Parametric polymorphism is a formal property of typed lambda calculi and logics, whereas traits are a specific language construct. Traits provide one particular way of achieving ad-hoc polymorphism. In ad hoc polymorphism, "a polymorphic function can denote a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied". Think of a trait as a function from a type (the class implementing the trait) to a record of functions (those methods belonging to the class that are required by the trait). Then this function can end up giving us "heterogeneous implementations" depending on the class it's applied to. E.g., consider the trait Stringable = { val toString : self -> string }. Now imagine implementing toString for class String extends Stringable for class Int extends Stringable. The two implementations will end up quite different. But in the case of, e.g., the append function used as an example in this article, the exact same implementation is used for both append : [Int] x [Int] -> [Int] and for append : [String] x [String] -> [String].

Do you think it would help improve the clarity of these two articles and their relation by

• Making it explicit on trait that this is a form of ad-hoc polymorphism
• Ensure traits are mentioned as a common approach to ad-hoc polymorphism on that page?

Synechist (talk) 21:19, 28 February 2022 (UTC)

Predicativity does not imply rank-1 polymorphism

There is confusion in the article about the relationship between predicativity and rank-1 polymorphism. I'll give a concrete example showing an error in the article and then give a broader discussion.

At the time of writing, the article says

"A consequence of predicativity is that all types can be written in a form that places all quantifiers at the outermost (prenex) position."

This is incorrect. Consider the following Haskell code (it requires GHC and can be tested at https://play.haskell.org/):

{-# LANGUAGE RankNTypes #-}
run :: (forall a. [a] -> a) -> (Int, String)
run picker = (picker [1, 2, 3], picker ["a", "b", "c"])
main = print (run head)

Here picker can be any function that extracts an element from a list. Haskell is predicative (unless the ImpredicativeTypes extension is enabled), so clearly this code snippet is predicative. But the type of run is rank-2, and it cannot be written as a rank-1 type or as a type in prenex form.

There seems to be a broader confusion (not just in this article) between rank-1 and predicativity. I'll begin with some uncontroversial definitions:

• "monotype" means a type that does not contain quantifiers.
• "predicative type system" means quantified variables may only be instantiated with monotypes.
• "rank-1 type" means no quantifiers may appear to the left of a function arrow.
• "prenex form" (strict sense) means all the quantifiers appear in the prefix.

It can be observed that any function whose type is rank-1 can be easily converted to a function whose type is in prenex form (assuming quantifiers cannot appear in arguments to other type constructors), so the terms "rank-1" and "prenex form" could be treated as effectively equivalent.

The tricky terms is "prenex polymorphism" (broad sense). The standard meaning appears to be that types are in prenex form (or rank-1 depending on the author) and the system is predicative. For example, from Types and Programming Languages (Pierce, 2002):

... the let-polymorphism of ML (§22.7), which is sometimes called prenex polymorphism because it can be viewed as a fragment of System F in which type variables range only over quantifier-free types (monotypes) and in which quantified types (polytypes, or type schemes) are not allowed to appear on the left-hand sides of arrows."

Also https://academicweb.nd.edu/~dchiang/teaching/pl/2025/hm.html:

The restriction to prenex types has some further consequences on syntax:

• ...
• In type applications t [T] as well, we restrict the type to be monomorphic. This restriction is called predicativity. Given that we’ve already restricted to prenex types, predicativity does not shrink the set of typable terms.

Question. If we did allow t [S] where S is polymorphic, what would t have to look like in order for the result to have a prenex type?"

The last quote hints at the reason that the term "prenex polymorphism" typically implies that the system is predicative (note the direction of the implication). Namely, instantiating a prenex type with a polytype will usually result in a type that is not in prenex form. For example, instantiating $\forall \alpha .\alpha \to \alpha$ with $\forall \beta .\beta \to \beta$ results in $(\forall \beta .\beta \to \beta )\to (\forall \beta .\beta \to \beta )$. Similarly, instantiating a rank-1 type with a polytype will usually result in a type that is not rank-1 (in the previous example, the result is a rank-2 type), hence "rank-1" would typically only be used in the context of a predicative system.

But the converse does not hold – it is perfectly reasonable to have a predicative system which is not limited to prenex/rank-1 types (for example Haskell with the RankNTypes extension). The article tries to argue that rank-N implies an "impredicative function type constructor"; I dislike that. In the logic sense, the definition of the function type constructor is actually predicative: using the notation of Pierce, we would define it as Arrow = λA::*. λB::*. ...; in this definition A and B range over types, while the thing being defined is a type constructor (aka type operator) -- so there is no impredicativity in this definition (in the logic sense), regardless of whether A and B range over monotypes or polytypes. Now, it does seem that in type systems "impredicatively" is used more loosely to refer to the instantiation of any type parameter with a polytype (as opposed to only the instantiation of a polytype's type parameter with a polytype), and in that sense the phrase "impredicative function type constructor" could be considered correct, but I still think that it should be avoided – if one views the function type constructor as a syntactic part of the language rather than an entity with type parameters, then calling it "impredicative" does not make sense.

Here is another good description from https://www.andres-loeh.de/qmlf-str.pdf:

.. This is a rank-2 type, as it contains quantifiers to the left of the function arrow. The Haskell implementations GHC and Hugs support higher-rank polymorphism such as it occurs in the definition of f above. If f is equipped with a type signature, the compiler accepts the definition. However, even though higher-ranked, the implementations are still limited due to a second restriction of Hindley-Milner: quantified variables can only be instantiated with a monomorphic type. Systems with this restriction are called predicative. The MLF type system is an extension of Hindley-Milner that fully supports first-class polymorphism: universal quantifiers can appear anywhere in a type, and quantified variables can be instantiated with a polymorphic type. Because of the last feature, MLF is an impredicative type system."

--Hddqsb (talk) 11:06, 22 June 2026 (UTC)