`SPECIALIZE instance` could be better
END GOAL: Use dependent types (or their approximation) to make code run faster.
Suppose we have a heterogeneous list type that can only hold a nice, limited set of things, as defined by this universe:
data U = INT | BOOL | LIST U
-- interpret the universe into Haskell types
type family El u where
El 'INT = Int
El 'BOOL = Bool
El ('LIST u) = [El u]
Here's our list type:
data HList :: [U] -> * where
Nil :: HList '[]
(:>) :: El u -> HList us -> HList (u ': us)
infixr 5 :>
Now, suppose I want to write a Show
instance for HList us
. This should certainly be possible -- we can see that such a list can contain only things that have instances for Show
. But I don't really expect GHC to do the nested induction to figure that out.
Through moderate pyrotechnics, I can get something like this to type-check, where I'm eliding the pyrotechnics:
-- space separated (terminated, actually), just for ease
instance {- don't look here -} => Show (HList us) where
show Nil = ""
show (x :> xs) = {- convince GHC that we can `show x` -} $
show x ++ " " ++ show xs
(The full file is attached. But it's nothing extraordinary.)
Now, suppose in client code, I know I'm often dealing with HList '[INT, BOOL, LIST INT]
. Let's call that type MyList
. When printing a MyList
, the Show
instance above has to do a runtime lookup to figure how to print the elements of MyList
. It must do this //every time//.
This is very silly. The whole point of putting the element types in the index to HList
is so that GHC can know, statically, what types the elements are. We shouldn't have to check!
The next step in my thought process was to use {-# SPECIALIZE instance ... #-}
to specialize the Show
instance. But then I ran into two problems:
-
{-# SPECIALIZE instance ... #-}
is allowed only in the context of the instance declaration. You can't do it in an importing module, even if the exporting module is kind enough to sayINLINABLE
in the right spots. -
{-# SPECIALIZE instance ... #-}
doesn't allow one specialization to use another. - (For more complicated scenarios)
{-# SPECIALIZE instance ... #-}
doesn't allow type families in the...
.
About point (1): Is there a good reason for this restriction? Of course, the concrete implementations of the methods of the instance to be specialized must be available, but the exporting module should be able to arrange that with the right pragmas.
To illustrate (2), I said {-# SPECIALIZE instance Show (HList '[ 'INT, 'BOOL, 'LIST 'INT ]) #-}
and GHC specialized only the first layer. OK. Reasonable enough. But then I tried
{-# SPECIALIZE instance Show (HList '[ 'LIST 'INT ]) #-}
{-# SPECIALIZE instance Show (HList '[ 'BOOL, 'LIST 'INT ]) #-}
{-# SPECIALIZE instance Show (HList '[ 'INT, 'BOOL, 'LIST 'INT]) #-}
and it still only went one layer deep. One specialization didn't call another. (Examined with -ddump-simpl
on -O2
.) That's frustrating.
About point (3): While it would be a bad idea to allow type families in normal instance heads, it seems sensible to allow them in SPECIALIZE instance
. This is rather like allowing expressions (instead of, say, bare variables) on the LHS of rules.
This ticket posting may be a little overly broad, but I'd love to know what others think about all of this. As we pick off the pieces that we decide are actually feasible, they should probably become separate tickets. But I think these are all of a piece and might benefit from some general thought about the whole SPECIALIZE instance
pragma and how improvements here can make a big difference when we have dependent types.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |