Search code examples
haskellparametric-polymorphismsubtypingtype-theory

Why is forall a. a not considered a subtype of Int while I can use an expression of type forall a. a anywhere one of type Int is expected?

Consider the following pair of function definitions, which pass the type checker:

a :: forall a. a
a = undefined

b :: Int
b = a

I.e. an expression of type forall a. a can be used where one of type Int is expected. This seems to me a lot like subtyping but it is claimed the type system of Haskell lacks subtyping. How do these forms of substitutability differ?

This question is not specific to forall a. a. Other examples include:

id :: forall a. a -> a
id x = x

idInt :: Int -> Int
idInt = id
Solution

  • In typed lambda calculi, we have the typing relation, usually denoted as : or in Haskell as ::. In general the relation is "many to many", so a type can contain multiple values and also a value can have many types.

    In particular in polymorphic type systems a value can have multiple types. For example

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

    but also

    map :: (Int -> Int) -> [Int] -> [Int].

    In such type systems it's (sometimes) possible to define a relation on types with the meaning "more general type than", a type order. If t ⊑ s then t is more general than s, meaning that if M : t then also M : s, and the typing rules of such a type system allow to infer exactly that. Or we say that s is a specialization of t. So in this sense, there is a subtyping relation on types.

    However, when we talk about subtyping in object oriented languages, we usually mean nominal subtyping, that is, we declare which types are subtypes of what, like when we define class inheritance. While in Haskell, it's a property of types, independent of any declarations. For example any type is a specialization of forall a . a.

    For the Hindley-Milner type system, which allows type inference and which is the base for most functional languages, there is the notion of principal type: If an expression M has a (any) type, then it also has its principal type, and the principal type is the most general type of all the possible types of M. The key feature is that the HM type inference algorithm always finds the most general type. So the most general, inferred principal type can be specialized to any valid type of M.