CODEWITHSUNDEEP
haskellghctype-inference
Kyuuhachi
Kyuuhachi

Reputation: 719

Type inference in where clauses

If I write

foo :: [Int]
foo = iterate (\x -> _) 0

GHC happily tells me that x is an Int and that the hole should be another Int. However, if I rewrite it to

foo' :: [Int]
foo' = iterate next 0
  where next x = _

it has no idea what the type of x, nor the hole, is. The same happens if I use let.

Is there any way to recover type inference in where bindings, other than manually adding type signatures?

Upvotes: 6

Views: 97

Answers (1)

K. A. Buhr
K. A. Buhr

Reputation: 50819

Not really. This behavior is by design and is inherited from the theoretical Hindley-Milner type system that formed the initial inspiration for Haskell's type system. (The behavior is known as "let-polymoprhism" and is arguably the most critical feature of the H-M system.)

Roughly speaking, lambdas are typed "top-down": the expression (\x -> _) is first assigned the type Int -> Int when type-checking the containing expression (specifically, when type-checking iterate's arguments), and this type is then used to infer the type of x :: Int and of the hole _ :: Int.

In contrast, let and where-bound variables are typed "bottom-up". The type of next x = _ is inferred first, independently of its use in the main expression, and once that type has been determined, it's checked against its use in the expression iterate next 0. In this case, the expression next x = _ is inferred to have the rather useless type p -> t. Then, that type is checked against its use in the expression iterate next 0 which specializes it to Int -> Int (by taking p ~ Int and t ~ Int) and successfully type-checks.

In languages/type-systems without this distinction (and ignoring recursive bindings), a where clause is just syntactic sugar for a lambda binding and application:

foo = expr1 where baz = bazdefn   ==>   foo = (\baz -> expr1) bazdefn

so one thing you could do is "desugar" the where clause to the "equivalent" lambda binding:

foo' :: [Int]
foo' = (\next -> iterate next 0) (\x -> _)

This syntax is physically repulsive, sure, but it works. Because of the top-down typing of lambdas, both x and the hole are typed as Int.

Upvotes: 4

Related Questions