Can we have type variables in constructor position in the Hindley Milner type system?

Question

In Haskell we can write the following data type:

data Fix f = Fix { unFix :: f (Fix f) }

The type variable f has the kind * -> * (i.e. it is an unknown type constructor). Hence, Fix has the kind (* -> *) -> *. I was wondering whether Fix was a valid type constructor in the Hindley Milner type system.

From what I read on Wikipedia, it seems that Fix is not a valid type constructor in the Hindley Milner type system because all type variables in HM must be concrete (i.e. must have the kind *). Is this indeed the case? If type variables in HM were not always concrete then would HM become undecidable?

Answer 1

What matters is whether type constructors form a first-order term language (no reduction behavior of type constructor expressions) or a higher-order one (with lambdas or similar constructs at type level).

In the former case, constraints arising from Fix are always unifiable in a most general way (assuming we stick to HM). In each c a b ~ t equation, t must be resolved to a concrete type application expression with the same shape as c a b, since c a b cannot possibly reduce to some other expression. Higher-kinded parameters aren't a problem, since they too just sit there in a static manner, for instance c [] ~ c f is solved by f = [].

In the latter case, c a b ~ t may or may not be solvable. In some cases it's solved by c = \a b -> t, in other cases there's no most general unifier.

Answer 2

Higher kinds go beyond the basic Hindley-Milner type system, but they can be handled in the same way.

Very roughly, HM parses the syntax tree of an expression, associates a free type variable to every subexpression, and generates a set of equational constraints over type-terms involving type variables according to the typing rules. The same can be done using higher kinds.

Then, the constraints are solved through unification. A typical step in the unification algorithm is (pseudo-haskell follows)

(F t1 ... tn := G s1 ... sk) =
  | n/=k || F/=G  -> fail
  | otherwise     -> { t1 := s1 , ... , tn := sn }

(Note that this is only a part of the unification algorithm.)

Above F, G are type constructor symbols, and not variables. In higher kinded unification, we need to account for F,G being variables as well. We could try the following rule:

(f t1 ... tn := g s1 ... sk) =
  | n/=k          -> fail
  | otherwise     -> { f := g , t1 := s1 , ... , tn := sn }

But wait! The above is not correct, since e.g. f Int ~ Either Bool Int must unify when f ~ Either Bool. So, we need to also consider the case where n/=k. In general, a simple rule set is

(f t := g s) =
  { f := g , t := s }
(F := G) =      -- rule for atomic terms
  | F /= G    -> fail
  | otherwise -> {}

(Again, this is only a part of the unification algorithm. Other cases must also be handled, as Andreas Rossberg points out below.)