4
$\begingroup$

I've been trying to understand type inference for Hindley-Milner-based languages, and I'm struggling to understand how generalization works. Let's say I have the following program in Haskell:

x :: Int
x = id 1

y :: Char
y = id 'a'

id :: a -> a
id x = x

If the type-checker traverses the program from top to bottom, then from x we can infer that the type of id must generalize Int -> Int, and from y we can infer that id must generalize Char -> Char, but I'm unclear how we can use these constraints without inferring a too-specific type for id.

If we check id first, then we can just instantiate its type in x and y, and use unification. However, if we have recursive or mutually recursive bindings, ensuring that all mentioned top-level bindings are typechecked before the binding itself would lead the type-checker into an infinite loop.

How are these issues resolved?

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ Note that Haskell topologically sorts the bindings according to the "occurs-in" relation. This is so id will be type checked, and given a polymorphic type, before x and y are type checked. This might find mutually recursive loops. If some binding in the loop is explicitly annotated, that's exploited to break the loop (the annotation is at first assumed, the other bindings are type checked, and finally the annotated binding are type checked last). If there's a loop without annotations, then generalization is only performed last: this might reject some well-typed programs. $\endgroup$ – chi Jul 23 '17 at 13:11
  • $\begingroup$ @chi Thanks for the great comment, perhaps it would be better as an answer. Can you please expand on what you mean by 'generalization is only performed last'? $\endgroup$ – user1502040 Jul 23 '17 at 13:50
  • $\begingroup$ and is this related to polymorphic recursion? $\endgroup$ – user1502040 Jul 23 '17 at 13:51
  • $\begingroup$ By that I mean that you first infer monotypes for all the bindings in the loop, using unification, and only after that you generalize (add universal quantification) over the variables. This means that e.g. let id1 :: a -> a ; id1 x = id2 x ; id2 y = const y (id1 True, id1 ()) type checks only because id1 is annotated, hence it is assumed to be polymorphic. I have not put this into an answer since it might be too much Haskell-specific -- one might use a different strategy. $\endgroup$ – chi Jul 23 '17 at 14:31
  • $\begingroup$ Polymorphic recursion requires an explicit annotation in Haskell. I think it's undecidable in the general case, so that's understandable. Perhaps you might want to read this question. $\endgroup$ – chi Jul 23 '17 at 14:34
4
$\begingroup$

There are a few things to realize:

First, top level declarations are implicitly let-bound, so your code is equivalent to the following:

let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'

  id :: a -> a
  id x = x

Secondly, as was mentioned in the comments, Haskell will sort the let statements topologically, nesting them when it can, and any recursive uses are monotyped unless annotated.

Finally, the types of let-variables are generalized at their definition, but specialized at their use. So now we have (something close to):

let
  id :: a -> a
  id x = x
in let
  x :: Int
  x = id 1

  y :: Char
  y = id 'a'

Finally, we need to see that while variable types are generalized at their definition, they are specialized at their use.

So, this is roughly what inference does:

  • The checker infers the type $id : \alpha \to \alpha$, then generalizes this to $\forall a \ldotp a \to a$.
  • The checker puts $id : \forall a \ldotp a \to a$ into the environment for checking $x$ and $y$
  • While checking the definitions of $x$, at the use of $id$, the type $\forall a \ldotp a \to a$ is instantiated to $\beta \to \beta$, where $\beta$ is a fresh unification variable.
  • While checking the definitions of $y$, at the use of $id$, the type $\forall a \ldotp a \to a$ is instantiated to $\gamma \to \gamma$, where $\gamma$ is a different fresh unification variable.

Because the polymorphic type scheme is instantiated with unique variables at each use, the inference is able proceed without error.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.