#10906: `SPECIALIZE instance` could be better -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- 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: 1. `{-# 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 say `INLINABLE` in the right spots. 2. `{-# SPECIALIZE instance ... #-}` doesn't allow one specialization to use another. 3. (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10906 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler