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?

Question

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

Fabio

undefined is not subtyping. It is an error. Why do you think this is subtyping? – Entranceway

Here's a different example: mempty :: forall m. Monoid m => m and let x = mempty :: [Int]. – Razor

But I distract - what's really going on here is any value of type forall a. a is equivalent to bottom - "bottom is an inhabitant of every type (though with some caveats concerning types of unboxed kind), bottoms can be used wherever a value of that type would be." – Razor

The Monoid example is quite different, since what's really happening is that the typeclass instances are passed behind the scenes like a dictionary, so that the type restriction ::[Int] causes a lookup in that dictionary. – Razor

Nontermination (bottom) is about the value. This question is about the type. – Fabio

Just a practical example: you can write [Int] but you can't write [forall a. a] (unless you enable impredicativity, which does not work so well with type inference). – Leathaleather

I'd like to mention that the lens library has a quite impressive "subtyping hierarchy" encoded using forall polymorphism and typeclasses. So whether or not this counts as subtyping, it can certainly be used that way. – Ganister

Answer 1

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.

Havre

Doesn't t ⊑ s mean that t is more specific than s, rather than more general? – Cyr

@Cyr I used the same notation as the Wikipedia page on HM where ⊑ means "more general than". It could be that the page is wrong :). – Havre

You write also "meaning that if M : t then also M : s" which doesn't seem to match. I could be wrong though. – Cyr

@Cyr As I understand it, if t is more general, it has less values (this is probably the reason for ⊑). So it M : t and s is a specialization of t, then also M : s. – Havre

Hmm, yeah, that's probably it. I know how to use these relationships properly, but I have no idea how to name them properly. – Cyr

Answer 2

With a question like this, I would take a step back and say that, fundamentally, the mathematical theories that underlie Haskell's design are System F variants that do not have the concept of subtyping.

Yes, it is possible to look at Haskell's surface syntax and notice that there are cases like what you bring up, where an expression of some type T can be used in any context where T' is expected. But this doesn't arise because Haskell was designed to support subtypes. Rather, it arises as an accident of the fact that Haskell was designed to be more user-friendly than a faithful rendering of System F would be.

In this case, it has to do with the fact that type-level quantifiers are generally not written explicitly in Haskell code, and type level lambdas and applications never are. If you look at the type forall a. a from a System F angle, the substitutability into Int contexts goes away. a :: forall a. a is a type level function and cannot be used in a context that expects Int—you need to first apply it to Int to get a Int :: Int, which is then what you can actually use in an Int context. Haskell's syntax hides that in the name of user-friendliness, but it's there in the underlying theory.

So in short, while you could analyze Haskell by tabulating which expression types can be substituted into which context types and demonstrate that there is some sort of crypto-subtype relation, it's just not fruitful because it yields analyses that swim against the current of the design. And it's not so much a matter of technicalities as it is of intent and other human factors.

Ringtailed

It is worth noting that some formalisations of polymorphic type systems (i.e. close relatives of Haskell's) actually do model the more-polymorphic-than relation as a form of subtyping. See my answer for an example reference. – Psychomotor

While GHC uses a System F variant as its underlying theory, that doesn't seem inherent in the Haskell type system. I wonder if the sorts of theories @DominiqueDevriese mentions could be used instead. – Cyr

@Cyr The two types of "core language" (the one from "Putting type annotations to work" vs. GHC's System F extension) are different in scope/purpose. The former includes a form of type inference since, for example, values of type forall a. a can be used where Ints are needed. GHC's System F descendents requires explicit type applications to convert forall a. a values to Ints. The language only models Haskell when type inference has first added necessary type applications/abstractions. Not modelling type inference is an advantage/disadvantage depending on the application, I guess. – Psychomotor

Answer 3

You are correct that the types a value of type forall a. a can be used wherever an Int is expected and that this implies a subtype relationship between the two types. The other answers above try to convince you that this "more-polymorphic-than"-relation is not subtyping. However, while it is certainly different from the forms of subtyping found in typical object-oriented languages, this does not mean that the "more-polymorphic-than"-relation cannot be seen as a (different) form of subtyping. In fact, some formalisations of polymorphic type systems model exactly this relation in their subtype relation. This is the case, for example, in the type system in Odersky and Läufer's paper "Putting type annotations to work".

Psychomotor

I think calling it subtyping is misleading. It is not OOP-style subtyping in the true sense. Though that paper is an interesting one indeed. – Entranceway

I disagree: the point is that there is more to subtyping than OOP-style subtyping. – Psychomotor

Answer 4

By :: a we mean "Any type", but not a subtype. a could be Int, or Bool, or IO (Maybe Ordering), but none in particular. a is not a type exactly, but a type variable.

Let's say we have a function like this:

id x = x

The compiler understands that there is no specific type for our argument x. We can use any type for x, just as long as it's equivalent to whatever comes out of id. So, we write the signature as so:

--    /- Any type in...
--    |    /- ...same type out.
--    V    V
id :: a -> a

Remember that types begin with a capital letter in Haskell. This is not a type: it is a type variable!

We use polymorphism because it's easier to do so. For instance, composition is a useful idea:

(>>>) :: (a -> b) -> (b -> c) -> (a -> c)
(>>>) f g a = g (f a)

So we can write things like:

plusOneTimesFive :: Int -> Int
plusOneTimesFive = (+1) >>> (* 5)

reverseHead :: [Bool] -> Bool
reverseHead = reverse >>> head

But what if we had to write every type out like this:

(>>>) :: (Bool -> Int) -> (Int -> String) -> (Bool -> String)
(>>>) f g a = g (f a)

(>>>') :: (Ordering -> Double) -> (Double -> IO ()) -> (Ordering -> IO ())
(>>>') f g a = g (f a)

(>>>'') :: (Int -> Int) -> (Int -> Bool) -> (Int -> Bool)
(>>>'') f g a = g (f a)

-- ...and so on.

That'd just be silly.

So the compiler infers the type using type unification like so:

Let's say I input this into GHCi. Let's say 6 in an Int for simplicity here.

id 6

The compiler thinks: "id :: a -> a, and it's being passed an Int, so a = Int, so id 6 :: Int.

This is not subtyping. Subtyping could be captured using typeclasses, but this is basic polymorphism at play.

Entranceway

I think you are wrong that this is not subtyping. See my answer below. – Psychomotor

Answer 5

It's not subtyping, it's type unification!

a :: forall a. a
a = undefined

b :: Int
b = a

In b = a, we're constraining b and a to be of the same type, so the compiler checks that that is possible. a has type forall a. a, which, by definition, unifies with every type, so the compiler oks our constraint.

Type unification also lets us do things like:

f :: (a -> Int) -> a
g :: (String -> b) -> b
h :: String -> Int
h = f g

Walking through the unification, f :: (a -> Int) -> a means g must have type a -> Int, which means a -> Int must unify with (String -> b) -> b, so b must b must be Int, which gives g the concrete type (String -> Int) -> Int, which means a is String -> Int.

Neither a -> Int nor (String -> b) -> b is a subtype of the other, but they can be unified as (String -> Int) -> Int.

Razor

I do not see how this answer addresses the question: "why is forall a. a not considered as a subtype of Int?". – Psychomotor

@DominiqueDevriese The primary reason would be that it's not a type? – Retort

@Cubic: What is not a type? forall a. a and Int are clearly types, right? – Psychomotor

What could it be other than a type? – Cyr