Changes between Initial Version and Version 1 of Design/TemplateHaskellGADTs


Ignore:
Timestamp:
Oct 19, 2014 7:01:15 PM (5 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Design/TemplateHaskellGADTs

    v1 v1  
     1= A Proposal for using GADTs within the implementation of Template Haskell =
     2
     3== The problem ==
     4
     5Haskell declarations and pragmas can appear in a variety of contexts, but not all declarations/pragmas can appear in all contexts. For examples, data declarations can appear only at top level; type family instances can appear at top-level, in classes (as defaults), and in instances, but never in `let`/`where` blocks; fixity declarations can be used anywhere other than in an instance declaration; etc. Yet, the Template Haskell `Dec` type monolithically includes ''all'' possible declarations. Currently, consumers of `Dec`s need to eliminate the possibility of `Dec`s in various contexts by emitting errors. Many users of Template Haskell might not know the intricate details of where which declarations can appear, making these "impossible" scenarios error-prone. And, with the solutions to #8100 (adding standalone-deriving) and #9064 (adding `default` type signatures to class declarations), the problem gets worse.
     6
     7== A proposed solution ==
     8
     9Use the type system to track which declaration form can be used where. First, declare
     10
     11{{{
     12data InTopLevel = YesInTopLevel | NoInTopLevel  deriving Typeable
     13data InClass    = YesInClass    | NoInClass     deriving Typeable
     14data InInstance = YesInInstance | NoInInstance  deriving Typeable
     15data InLet      = YesInLet      | NoInLet       deriving Typeable
     16}}}
     17
     18These are all Boolean-like flags with more perspicuous names.
     19
     20Then, pack these flags into a type:
     21
     22{{{
     23data DecContext = DC InTopLevel InClass InInstance InLet deriving Typeable
     24}}}
     25
     26Now, define `Dec` as a GADT indexed by `DecContext`:
     27
     28{{{
     29data Dec :: DecContext -> * where
     30  FunD ::  Name -> [Clause] -> Dec (DC top NoInClass inst lt)
     31    -- ^ @{ f p1 p2 = b where decs }@
     32  ValD ::  Pat -> Body -> [LetDec] -> Dec (DC top NoInClass inst lt)
     33    -- ^ @{ p = b where decs }@
     34  DataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name]
     35        -> Dec (DC top NoInClass NoInInstance NoInLet)
     36    -- ^ @{ data Cxt x => T x = A x | B (T x)
     37    --       deriving (Z,W)}@
     38  NewtypeD :: Cxt -> Name -> [TyVarBndr] -> Con -> [Name]
     39           -> Dec (DC top NoInClass NoInInstance NoInLet)
     40    -- ^ @{ newtype Cxt x => T x = A (B x)
     41    --       deriving (Z,W)}@
     42  TySynD :: Name -> [TyVarBndr] -> Type -> Dec (DC top NoInClass NoInInstance NoInLet)
     43    -- ^ @{ type T x = (x,x) }@
     44  ClassD :: Cxt -> Name -> [TyVarBndr] -> [FunDep] -> [ClassDec]
     45         -> Dec (DC top NoInClass NoInInstance NoInLet)
     46    -- ^ @{ class Eq a => Ord a where ds }@
     47  InstanceD :: Cxt -> Type -> [InstanceDec] -> Dec (DC top NoInClass NoInInstance NoInLet)
     48    -- ^ @{ instance Show w => Show [w]
     49                                  --       where ds }@
     50  SigD :: Name -> Type -> Dec (DC top cls inst lt)
     51    -- ^ @{ length :: [a] -> Int }@
     52  ForeignD :: Foreign -> Dec (DC top NoInClass NoInInstance NoInLet)
     53    -- ^ @{ foreign import ... }
     54    -- { foreign export ... }@
     55
     56  InfixD :: Fixity -> Name -> Dec (DC top cls NoInInstance lt)
     57    -- ^ @{ infix 3 foo }@
     58
     59  -- | pragmas
     60  PragmaD :: Pragma loc -> Dec loc
     61    -- ^ @{ {\-# INLINE [1] foo #-\} }@
     62
     63  -- | type families (may also appear in [Dec] of 'ClassD' and 'InstanceD')
     64  FamilyD :: FamFlavour -> Name -> [TyVarBndr] -> Maybe Kind
     65          -> Dec (DC top cls NoInInstance NoInLet)
     66    -- ^ @{ type family T a b c :: * }@
     67
     68  DataInstD :: Cxt -> Name -> [Type] -> [Con] -> [Name]
     69            -> Dec (DC top NoInClass inst NoInLet)
     70    -- ^ @{ data instance Cxt x => T [x] = A x
     71    --                                | B (T x)
     72    --       deriving (Z,W)}@
     73  NewtypeInstD :: Cxt -> Name -> [Type] -> Con -> [Name]
     74               -> Dec (DC top NoInClass inst NoInLet)
     75    -- ^ @{ newtype instance Cxt x => T [x] = A (B x)
     76    --       deriving (Z,W)}@
     77  TySynInstD :: Name -> TySynEqn -> Dec (DC top cls inst NoInLet)
     78    -- ^ @{ type instance ... }@
     79
     80  ClosedTypeFamilyD :: Name -> [TyVarBndr] -> Maybe Kind -> [TySynEqn]
     81                    -> Dec (DC top NoInClass NoInInstance NoInLet)
     82    -- ^ @{ type family F a b :: * where ... }@
     83
     84  RoleAnnotD :: Name -> [Role] -> Dec (DC top NoInClass NoInInstance NoInLet)
     85    -- ^ @{ type role T nominal representational }@
     86}}}
     87
     88Each constructor's return type tells you where the declaration is prohibited.
     89
     90Then, specialize `Dec` to the four cases that exist:
     91
     92{{{
     93type TopLevelDec = Dec (DC YesInTopLevel NoInClass  NoInInstance  NoInLet)
     94type ClassDec    = Dec (DC NoInTopLevel  YesInClass NoInInstance  NoInLet)
     95type InstanceDec = Dec (DC NoInTopLevel  NoInClass  YesInInstance NoInLet)
     96type LetDec      = Dec (DC NoInTopLevel  NoInClass  NoInInstance  YesInLet)
     97}}}
     98
     99And now, we can use these last 4 types as simple datatypes that have fewer constructors than the full `Dec` type. Types to the rescue!
     100
     101For example:
     102{{{
     103data Clause = Clause [Pat] Body [LetDec]
     104                                  -- ^ @f { p1 p2 = body where decs }@
     105    deriving( Show, Eq, Data, Typeable, Generic )
     106}}}
     107
     108The `[LetDec]` is the `where` stanza of a declaration. Or:
     109
     110{{{
     111data Exp
     112  =  ...
     113  | LetE [LetDec] Exp                  -- ^ @{ let x=e1;   y=e2 in e3 }@
     114  | ...
     115  deriving( Show, Eq, Data, Typeable, Generic )
     116}}}
     117
     118Here, we include only `LetDec`s in a `let`. You can see above that `ClassDec` and `InstanceDec` are used as appropriate in `Dec`.
     119
     120Under this scenario, `[d| ... |]` would have the type `Q [TopLevelDec]`, and if you have a top-level splice, it must also be of type `Q [TopLevelDec]`.
     121
     122`Pragma`, which are similarly sometimes available and sometimes unavailable, depending on context, are similarly indexed:
     123
     124{{{
     125data Pragma :: DecContext -> * where
     126  InlineP :: Name -> Inline -> RuleMatch -> Phases
     127          -> Pragma (DC top cls inst lt)
     128  SpecialiseP :: Name -> Type -> Maybe Inline -> Phases
     129              -> Pragma (DC top NoInClass inst lt)
     130  SpecialiseInstP :: Type -> Pragma (DC NoInTopLevel NoInClass inst NoInLet)
     131  RuleP :: String -> [RuleBndr] -> Exp -> Exp -> Phases
     132        -> Pragma (DC top NoInClass NoInInstance NoInLet)
     133  AnnP :: AnnTarget -> Exp -> Pragma (DC top NoInClass NoInInstance NoInLet)
     134  LineP :: Int -> String -> Pragma (DC top NoInClass NoInInstance NoInLet)
     135}}}
     136
     137== Discussion ==
     138
     139=== Pros ===
     140
     141This seems to work, in preliminary tests. Matching on this GADT does not trigger #3927 (that is, it does not warn about vacuous incomplete patterns), and you can't squeeze, say, a `DataD` into a `LetDec`.
     142
     143=== Cons ===
     144
     145* `Data` and `Generic` (see #9527, requesting `Generic` instances) don't play well with GADTs. I can hand-write `Data` instances for `Dec` and `Pragma`, but these implement only `gfoldl` and error on `gunfold`. I have not yet tried to write hand-written `Generic` instances, but I'm not hopeful.
     146
     147* I frequently use `:info Dec` in GHCi when writing TH code. The output after this transformation is much noisier than it was before.
     148
     149== Questions ==
     150
     151* Does anyone use `gunfold` for TH types?
     152
     153* Is there a need for `Generic` instances for `Dec` and `Pragma`? Are these possible for GADTs?