20

I'm reading the Wikipedia article on Hindley–Milner Type Inference trying to make some sense out of it. So far this is what I've understood:

  1. Types are classified as either monotypes or polytypes.
  2. Monotypes are further classified as either type constants (like int or string) or type variables (like α and β).
  3. Type constants can either be concrete types (like int and string) or type constructors (like Map and Set).
  4. Type variables (like α and β) behave as placeholders for concrete types (like int and string).

Now I'm having a little difficulty understanding polytypes but after learning a bit of Haskell this is what I make of it:

  1. Types themselves have types. Formally types of types are called kinds (i.e. there are different kinds of types).
  2. Concrete types (like int and string) and type variables (like α and β) are of kind *.
  3. Type constructors (like Map and Set) are lambda abstractions of types (e.g. Set is of kind * -> * and Map is of kind * -> * -> *).

What I don't understand is what do qualifiers signify. For example what does ∀α.σ represent? I can't seem to make heads or tails of it and the more I read the following paragraph the more confused I get:

A function with polytype ∀α.α -> α by contrast can map any value of the same type to itself, and the identity function is a value for this type. As another example ∀α.(Set α) -> int is the type of a function mapping all finite sets to integers. The count of members is a value for this type. Note that qualifiers can only appear top level, i.e. a type ∀α.α -> ∀α.α for instance, is excluded by syntax of types and that monotypes are included in the polytypes, thus a type has the general form ∀α₁ . . . ∀αₙ.τ.

Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299

2 Answers2

20

First, kinds and polymorphic types are different things. You can have a HM type system where all types are of the same kind (*), you could also have a system without polymorphism but with complex kinds.

If a term M is of type ∀a.t, it means that for whatever type s we can substitute s for a in t (often written as t[a:=s] and we'll have that M is of type t[a:=s]. This is somewhat similar to logic, where we can substitute any term for a universally quantified variable, but here we're dealing with types.

This is precisely what happens in Haskell, just that in Haskell you don't see the quantifiers. All type variables that appear in a type signature are implicitly quantified, just as if you had forall in front of the type. For example, map would have type

map :: forall a . forall b . (a -> b) -> [a] -> [b]

etc. Without this implicit universal quantification, type variables a and b would have to have some fixed meaning and map wouldn't be polymorphic.

The HM algorithm distinguishes types (without quantifiers, monotypes) and type schemas (universaly quantified types, polytypes). It's important that at some places it uses type schemas (like in let), but at other places only types are allowed. This makes the whole thing decidable.

I also suggest you to read the article about System F. It is a more complex system, which allows forall anywhere in types (therefore everything there is just called type), but type inference/checking is undecidable. It can help you understand how forall works. System F is described in depth in Girard, Lafont and Taylor, Proofs and Types.

ulidtko
  • 14,740
  • 10
  • 56
  • 88
Petr
  • 62,528
  • 13
  • 153
  • 317
  • Regarding the type quantification in Haskell, [existential types overview](http://www.haskell.org/haskellwiki/Existential_types) can become a worthwhile discovery. – ulidtko Mar 19 '13 at 12:11
  • 2
    Type inference for System F is undecidable, but type checking is easy (if by type checking we mean that terms are annotated with types and we just check that those annotations make sense). – augustss Mar 19 '13 at 16:43
  • 2
    @augustss By typechecking it is meant that you are given a non-annotated term (Curry style) and a type, and you should determine if the term conforms to the type or not. This is undecidable too, as proved by Joe Wells in [Typability and Type Checking in the Second-Order lambda-Calculus Are Equivalent and Undecidable](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.3590). – Petr Mar 19 '13 at 17:28
  • 1
    @PetrPudlák I know that's undecidable. Many people refer to type checking as the process of checking that a Church style term is valid, so I wanted to clarify. – augustss Mar 19 '13 at 18:02
4

Consider l = \x -> t in Haskell. It is a lambda, which represents a term t fith a variable x, which will be substituted later (e.g. l 1, whatever it would mean) . Similarly, ∀α.σ represents a type with a type variable α, that is, f : ∀α.σ if a function parameterized by a type α. In some sense, σ depends on α, so f returns a value of type σ(α), where α will be substituted in σ(α) later, and we will get some concrete type.

In Haskell you are allowed to omit ∀ and define functions just like id : a -> a. The reason to allowing omitting the quantifier is basically since they are allowed only top level (without RankNTypes extension). You can try this piece of code:

id2 : a -> a -- I named it id2 since id is already defined in Prelude
id2 x = x

If you ask ghci for the type of id(:t id), it will return a -> a. To be more precise (more type theoretic), id has the type ∀a. a -> a. Now, if you add to your code:

val = id2 3

, 3 has the type Int, so the type Int will be substituted into σ and we will get the concrete type Int -> Int.

karlicoss
  • 2,501
  • 4
  • 25
  • 29