let-bind more types to save space
GHC Core has support for
let-binding type variables. This feature is little used today. But a conversation at an HIW talk by @edsko, including @nomeata, @kosmikus, @christiaanb, and @sweirich made me wonder if it could be the answer to a problem.
See Edsko's large-records blog post for a wonderfully detailed exposition of the problem.
The problem is that type applications force a quadratic representation of, say, heterogeneous lists. Here is an example:
type HList :: [Type] -> Type data HList tys where HNil :: HList ' HCons :: forall a as. a -> HList as -> HList (a : as)
Now, suppose I want a list
[42, True, 'x', 3.14]. This would be
HCons @Int @((:) @Type Bool ((:) @Type Char ((:) @Type Double (' @Type)))) 42 (HCons @Bool @((:) @Type Char ((:) @Type Double (' @Type))) True (HCons @Char @((:) @Type Double (' @Type)) 'x' (HCons @Double @(' @Type) 3.14 HNil)))
You can see that the tails of the type list are repeated. Using type-level
let, we can rewrite this as
let t3 = ' @Type in let t2 = (:) @Type Double t3 in let t1 = (:) @Type Char t2 in let t0 = (:) @Type Bool t1 in HCons @Int @t0 42 (HCons @Bool @t1 True (HCons @Char @t2 'x' (HCons @Double @t3 3.14 HNil)))
That's much better! It's not quadratic. There is still some redundancy, but at least it's not quadratic.
Implementing this seems relatively easy: instead of filling in metavariables in the solver, we just bind them in the
EvBindsVar. I know it won't be quite that easy (we have to figure out which
EvBindsVar(s) are associated with which variables), but I think we have the structure to experiment with this. (Another problem: it won't work in, say, type signatures, when we have no
Open question: in the absence of -dcore-lint, will this speed up programs? Open question: does the optimizer re-expand type-lets?