I really don't like let generalization
03 November 2023I 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.