Changes between Version 10 and Version 11 of ImplementingTreesThatGrow/TreesThatGrowGuidance


Ignore:
Timestamp:
Jun 11, 2018 8:05:14 AM (15 months ago)
Author:
Shayan-Najd
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ImplementingTreesThatGrow/TreesThatGrowGuidance

    v10 v11  
    2020== General pattern for TTG ==
    2121
    22 In general a TTG-idiom data type has
     22In general, a TTG-idiom data type has
    2323* A type parameter, called the ''phase descriptor'', that indexes which particular instantiation is required
    2424* One ''extension field'' in each data constructor, whose type is given by a type family.  By giving phase-specific instances to this type family, we can add phase-specific information to the constructor.
     
    2626
    2727For example:
    28 {{{
     28{{{#!hs
    2929data Exp x
    3030  = Var (XVar x) (IdP x)
    31   | Lam (XLam x) (IdP x)  (Exp x)
     31  | Lam (XLam x) (IdP x) (Exp x)
    3232  | App (XApp x) (Exp x) (Exp x)
    3333  | New (XNew x)
     
    3737type family XApp x
    3838type family XNew x
    39 
    40 }}}
    41 Here the phase descriptor is `x`.  The first field of each constructor (of type `XVar x` etc) are the extension fields.  The data construcotr `XNew` is the extension constructor.
     39}}}
     40Here the phase descriptor is `x`.  The first field of each constructor (of type `XVar x` etc) are the extension fields.  The data constructor `XNew` is the extension constructor.
    4241
    4342All fields of the data constructors except the first (extension) field are called ''payload fields''.  They are present in every instantiation of the data type.
     
    5049
    5150b. Note, however, that the type of a payload field of a constructor may vary with phase.  For example, in `Lam` above, the first payload field has type `Id x`, and that may vary with phase:
    52 {{{
     51{{{#!hs
    5352type family IdP x
    5453type instance IdP GhcPs = RdrName
     
    7372Consider the following three simple datatypes `ExpPs`, `ExpRn`, and `ExpTc` representing correspondingly expressions in a parsing, renaming and typechecking phase:
    7473
    75 {{{
     74{{{#!hs
    7675module Parsing where
    7776
     
    8584}}}
    8685
    87 {{{
     86{{{#!hs
    8887module Renaming where
    8988
     
    9897}}}
    9998
    100 {{{
     99{{{#!hs
    101100module Typechecking where
    102101
     
    113112Based on the TTG idiom, we will have a base declaration such as the following.
    114113
    115 {{{
     114{{{#!hs
     115{-# LANGUAGE TypeFamilies , EmptyCase #-}
    116116module AST where
    117117
    118118data Exp x
    119   = Var (XVar x) (IdP x)
    120   | Lam (XLam x) (IdP x) (Exp x)
     119  = Var (XVar x) (XId x)
     120  | Abs (XAbs x) (XId x) (Exp x)
    121121  | App (XApp x) (Exp x) (Exp x)
    122122  | New (XNew x)
    123123
    124124type family XVar x
    125 type family XLam x
     125type family XAbs x
    126126type family XApp x
    127127type family XNew x
    128128
    129 type family IdP  x
     129type family XId  x
     130
     131data NoExt = NoExt -- no field extension
     132
     133data NoNewCon      -- no constructor extension
     134
     135noNewCon :: NoNewCon -> a
     136noNewCon x = case x of {}
    130137}}}
    131138
    132139and the following three instantiations:
    133140
    134 {{{
     141{{{#!hs
     142{-# LANGUAGE TypeFamilies #-}
    135143module Parsing where
    136144
    137145import AST
    138 -- the definition of RdrName
    139 -- ...
     146
     147data RdrName -- = ...
    140148
    141149data Ps
     
    143151type ExpPs = Exp Ps
    144152
    145 type instance XVar Ps = ()
    146 type instance XLam Ps = ()
    147 type instance XApp Ps = ()
    148 type instance XNew Ps = Void
    149 
    150 type instance IdP  Ps = RdrName
    151 }}}
    152 
    153 {{{
     153type instance XVar Ps = NoExt
     154type instance XAbs Ps = NoExt
     155type instance XApp Ps = NoExt
     156type instance XNew Ps = NoNewCon
     157
     158type instance XId  Ps = RdrName
     159}}}
     160
     161{{{#!hs
     162{-# LANGUAGE TypeFamilies #-}
    154163module Renaming where
    155164
    156165import AST
    157 -- the definition of `Name` and `UnboundVar`
    158 -- ...
     166
     167data Name       -- = ...
     168data UnboundVar -- = ...
     169
    159170data Rn
    160171
    161172type ExpRn = Exp Rn
    162173
    163 type instance XVar Rn = ()
    164 type instance XLam Rn = ()
    165 type instance XApp Rn = ()
     174type instance XVar Rn = NoExt
     175type instance XAbs Rn = NoExt
     176type instance XApp Rn = NoExt
    166177type instance XNew Rn = UnboundVar
    167178
    168 type instance IdP  Rn = Name
    169 }}}
    170 
    171 {{{
     179type instance XId  Rn = Name
     180}}}
     181
     182{{{#!hs
     183{-# LANGUAGE TypeFamilies #-}
    172184module Typechecking where
    173185
    174186import AST
    175 -- the definition of `Id`, `UnboundVar`, and `Type`
    176 -- ...
     187
     188data Id         -- = ...
     189data UnboundVar -- = ...
     190data Type       -- = ...
     191
    177192data Tc
    178193
    179194type ExpTc = Exp Tc
    180195
    181 type instance XVar Tc = ()
    182 type instance XLam Tc = ()
     196type instance XVar Tc = NoExt
     197type instance XAbs Tc = NoExt
    183198type instance XApp Tc = Type
    184199type instance XNew Tc = UnboundVar
    185200
    186 type instance IdP  Tc = Id
    187 }}}
     201type instance XId  Tc = Id
     202}}}
     203
     204
     205
     206Note that we define a specific pair of datatypes to mark and handle empty extension fields and constructors.
     207
     208