CODEWITHSUNDEEP
haskelltype-inferencehindley-milner
sinelaw
sinelaw

Reputation: 16563

Hindley-Milner generalization gone bad?

Consider the following program (in Haskell, but could be any HM-inferred language):

x = []
y = x!!0

Using HM (or by running the compiler), we infer:

x :: forall t. [t]
y :: forall a. a

I understand how this happens, playing by the usual generalization/instantiation rules, but I'm not sure it's desirable to have something like forall a. a.

One question is: since we have an out-of-bounds access here, one can rule out the program as a valid example. Instead, can we say the universal type we inferred is a sign of something wrong in the program? If yes, can we use this "fact" to deliberately fail checking of invalid programs in other cases as well?

The next program gets even stranger types:

c = []
d = (c!!0) + (1 :: Int)

Inferred types:

c :: forall t. [t]
d :: Int

...although d was drawn from c!

Can we augment HM to do a better job here without ruling out valid programs?

EDIT: I suspected this is an artifact of using partial functions (!!0 in this case). But see:

c = []
d = case c of [] -> 0; (x:_) -> x + (1 :: Int)

There are now no partial functions in use. And yet, c :: forall t. [t] and d :: Int.

Upvotes: 2

Views: 471

Answers (2)

Hans Lub
Hans Lub

Reputation: 5678

The Hindley-Milner type of a term doesn't depend on the value of its subterms, only on their types. A HM type-checker will never evaluate expressions, only type-check them, so it sees your x as just "a list of a", not as an "empty list of a", as a human does when informally type-checking your program.

There are type systems that would flag your program as type-incorrect, e.g. dependent types, but those don't have type inference without explicit type declarations, which is one of the luxuries Haskell/ML programmers enjoy, thanks to HM.

Using an extension to HM (GADTs) Haskell can define a type for "safe lists" 

data Empty
data NonEmpty

data SafeList a b where
  Nil :: SafeList a Empty
  Cons:: a -> SafeList a b -> SafeList a NonEmpty

(!!) :: SafeList a NonEmpty -> Int -> a
-- etc

This would make Nil!!0 a type error.

Upvotes: 5

Jon Purdy
Jon Purdy

Reputation: 55069

I’m not sure it's desirable to have something like forall a. a.

It isn’t desirable. By parametricity, the only thing that an expression of such a type can do when you evaluate it is to fail to halt, either by throwing an exception or by looping infinitely. This is what Haskellers mean when we talk about computations producing “bottom” (⊥).

If you’re thinking of what extension to HM would rule out such types, you could disallow any type which, when interpreted as a logical formula, is not a tautology. Such functions would be guaranteed to raise errors for some inputs.

So x :: forall a. [a] would be okay, because for any type a, we can indeed construct a value of type [a]—an empty list! But, for example, head :: forall a. [a] -> a would not be okay, because it’s not true that we can always get a value of type a from a value of type [a]—since the list might be empty.

However, this becomes less useful the more concrete your types are. You would get basically no guarantees about functions of type Int -> Int, for example.

Upvotes: 3

Related Questions