Hindley Milner type inference only permits “top-level polymorphism”

In other words, Hindley Milner type inference only permits universal quantification at the top-level of a program or at the top-level of a let-bound expression

This is, at best, unclearly formulated, and some interpretations of it are wrong. It is very easy to infer polymorphic types for any sub-expression in an HM-style inference system, the question is what to do with those types then – for let there is a clear answer. In OCaml for example, <expr> is generalized for example in <expr> <args> or in match <expr> with ... or in { field = <expr>; ... }.

Otherwise: I think this is a nice blog post, but I think that there are other differences between HM and bidirectional that could have been pointed out explicitly:

Hinley-Damas-Milner inference typically provides a stronger form of principality (the property that type inference never “chooses” among incompatible, valid types for subexpressions; then it’s ambiguous which one the user intended)

one reason why people like HM (in the fragment where it works well) is that it typically requires less type annotations than bidirectional typing. I think there is a building consensus now that annotating top-level functions is a good thing anyway, so in practice this is often not perceived as an issue, but even inside terms you may have to insert more annotations in a bidirectional world.

as a consequence, certain program transformations preserve annotation-less typability in a HM system, while they break the well-typedness in bidirectional systems unless you add more annotations. From memory, unless you add special tricks to your system (that don’t always work well in general), turning f x into f $ x or flip ($) x f may typically break well-typedness in a bidirectional system, which users may find inconvenient.

I think unification-based type inference is more than a hack. It addresses a
fundamental weakness of traditional bidirectional typing systems. I think that a
combination of the two - a bidirectional typing system with unification - will
be the best approach.

The weakness is that bidirectional typing systems do not talk about
“partially-known” types.

Bidirectional typing systems require “complete” types, but the inference rules
of the lambda calculus fundamentally give us partial information about types.

For example, the inference rule for lambdas:

Ctx, x : A |- e : B
-----------------------
Ctx |- \x -> e : A -> B

is translated to this rule in a bidirectional typing system (where <= means
“check” and => means “infer”):

Ctx, x : A |- e <= B
------------------------
Ctx |- \x -> e <= A -> B

While it’s true that upon examining the \x -> e we don’t know A or B, we’re
not completely in the dark. At this point we know we’re looking at a function
type, regardless of its inputs and outputs.

So it would be better to say that lambdas synthesise a partial type:

Ctx, x : ?0 |- e => B
-------------------------
Ctx |- \x -> e => ?0 -> B

Mandating that “introduction forms are checked” is overly restrictive, which is
why it comes with the (necessary) caveat: “but you can add synthesis rules for
cases where the types are obvious”. Saying that “introduction forms
synthesise partial types” might be a monotonic improvement.

Yes, you read that right; I didn’t get the subtyping direction backwards. A polymorphic type is a subtype of a more specialized type.

I cannot seem to be able to wrap my head around this. Why is this the case? And in which type systems (or is it something that’s independent of the type system?)?

Am I correct in remembering that in the context of Hindley-Milner, we usually say id : Text -> Text “is an instantiation of” id : 'a -> 'a, and thus the direction is the other way round?

Going back to the definition of a subtype: the type A is a subtype of another type B if every expression of type A is also an expression of type B

So in this example an expression of type forall (a : Type) . a -> a is a subtype of Text -> Text, because every expression of type forall (a : Type) . a -> a is also an expression of type Text -> Text. Whether or not either type is instantiated from the other type does not come into play

So I’m guessing saying something like “we can instantiate the type of id to Text -> Text” really just means that whatever we instantiate to is a valid supertype? Or does it have a different meaning (it being “instantiate”, or whatever word people use when talking about turning polymorphic types into concrete ones), since you said it does not come into play?

Yes, if you instantiate a universally quantified type then the result is a valid supertype

I should not have said “does not come into play”. Rather, I should have said “the definition of the subtype relation does not explicitly reference instantiation”, but you can derive that an instantiated type is a supertype as a consequence of the definition of subtypes

Classifying expressions is the mechanism of a type system, but its ultimate purpose is to constrain values. In particular, subtyping ensures that values can be used in legal ways, even when the relevant types do not match exactly.

So code which expects a value of type Text -> Text can be given the polymorphic identity function and nothing will go wrong at runtime. Thus the subtyping relation is crafted to make the polymorphic identity type be a subtype of its concrete instantiation. The converse is not true; a context which holds a value of type a -> a is free to pass it non-Text values, which would blow up when passed to a Text-manipulating function.

This might also give some intuition for function type contravariance. If we have a context (e.g. a function parameter) of type H -> G and we pass it a value of type A -> B, the flow of values at runtime will be H ==> A (the caller is constrained by the context to pass a value of type H, which flows to the bound variable of the function we pass) and B ==> G (for the return value).

This is, at best, unclearly formulated, and some interpretations of it are wrong. It is very easy to infer polymorphic types for any sub-expression in an HM-style inference system, the question is what to do with those types then – for

`let`

there is a clear answer. In OCaml for example,`<expr>`

is generalized for example in`<expr> <args>`

or in`match <expr> with ...`

or in`{ field = <expr>; ... }`

.Otherwise: I think this is a nice blog post, but I think that there are other differences between HM and bidirectional that could have been pointed out explicitly:

`f x`

into`f $ x`

or`flip ($) x f`

may typically break well-typedness in a bidirectional system, which users may find inconvenient.I found this talk from Compose Conference helpful for understanding bidirectional type checking too.

I think unification-based type inference is more than a hack. It addresses a fundamental weakness of traditional bidirectional typing systems. I think that a combination of the two - a bidirectional typing system with unification - will be the best approach.

The weakness is that bidirectional typing systems do not talk about “partially-known” types.

Bidirectional typing systems require “complete” types, but the inference rules of the lambda calculus fundamentally give us partial information about types.

For example, the inference rule for lambdas:

is translated to this rule in a bidirectional typing system (where

`<=`

means “check” and`=>`

means “infer”):While it’s true that upon examining the

`\x -> e`

we don’t know`A`

or`B`

, we’re notcompletelyin the dark. At this point we know we’re looking at a function type, regardless of its inputs and outputs.So it would be better to say that lambdas synthesise a

partialtype:Mandating that “introduction forms are checked” is overly restrictive, which is why it comes with the (necessary) caveat: “but you can add synthesis rules for cases where the types are obvious”. Saying that “introduction forms synthesise partial types” might be a monotonic improvement.

I cannot seem to be able to wrap my head around this. Why is this the case? And in which type systems (or is it something that’s independent of the type system?)?

Am I correct in remembering that in the context of Hindley-Milner, we usually say

`id : Text -> Text`

“is an instantiation of”`id : 'a -> 'a`

, and thus the direction is the other way round?Going back to the definition of a subtype: the type

`A`

is a subtype of another type`B`

if every expression of type`A`

is also an expression of type`B`

So in this example an expression of type

`forall (a : Type) . a -> a`

is a subtype of`Text -> Text`

, because every expression of type`forall (a : Type) . a -> a`

is also an expression of type`Text -> Text`

. Whether or not either type is instantiated from the other type does not come into playThank you, now it clicked.

So I’m guessing saying something like “we can instantiate the type of

`id`

to`Text -> Text`

” really just means that whatever we instantiate to is a valid supertype? Or does it have a different meaning (itbeing “instantiate”, or whatever word people use when talking about turning polymorphic types into concrete ones), since you said it does not come into play?Yes, if you instantiate a universally quantified type then the result is a valid supertype

I should not have said “does not come into play”. Rather, I should have said “the definition of the subtype relation does not explicitly reference instantiation”, but you can derive that an instantiated type is a supertype as a consequence of the definition of subtypes

Classifying expressions is the mechanism of a type system, but its ultimate purpose is to constrain values. In particular, subtyping ensures that values can be used in legal ways, even when the relevant types do not match exactly.

So code which expects a value of type

`Text -> Text`

can be given the polymorphic identity function and nothing will go wrong at runtime. Thus the subtyping relation is crafted to make the polymorphic identity type be a subtype of its concrete instantiation. The converse is not true; a context which holds a value of type`a -> a`

is free to pass it non-`Text`

values, which would blow up when passed to a`Text`

-manipulating function.This might also give some intuition for function type contravariance. If we have a context (e.g. a function parameter) of type

`H -> G`

and we pass it a value of type`A -> B`

, the flow of values at runtime will be H ==> A (the caller is constrained by the context to pass a value of type H, which flows to the bound variable of the function we pass) and B ==> G (for the return value).