I really don't like let generalization

I just don’t think it’s worth it.

I’ve written before about how let generalization makes language constructs like GADTs, that don’t necessarily have principal types, much harder to use. Note that this doesn’t only happen if a declaration mentions local variables from an outer scope as described in Let Should Not Be Generalized!

For example, as written, this Haskell code doesn’t compile because test doesn’t have a principal type, but uncommenting the let _ = x declaration prevents the type checker from generalizing test, which means that, based on the only usage site, its type is inferred to the much more specific T Bool -> Bool -> Bool, which compiles just fine.

data T :: Type -> Type where
  T1 :: Int -> T Bool
  T2 :: T a

f x =
  let 
    test (T1 n) _ = n > 0
    test T2     r = 
      -- let _ = x in
      r
  in
  test (T1 5)

But that’s not even the only reason to dislike let generalization!

Even in extremely simple programs, the tooling experience suffers a lot when lets are generalized. A pattern I like is defining function arguments to functions like zipWith (List.map2 in OCaml) as a local binding. For example

let doSomething index char = ... in

zipWith doSomething [0..10] ['A'..'Z']

Now, what is the type of char in this case that shows up when I hover over it in my editor or in error messages it’s involved in?

a

Yeah. That’s not useful. The type is Char at the only usage site, but because doSomething is unnecessarily generalized, the compiler cannot assume that and instead infers the most general - but definitely not most relevant - type.

And what do we gain in return?

Let generalization lets us avoid writing a type signature for polymorphic local declarations, that are used more than once and at different instantiations.

I’d rather have better error messages.