Language/Symantic/Typing/Family.hs

   1 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   2 module Language.Symantic.Typing.Family where
   3
   4 import Control.Applicative ((<|>))
   5 import Data.Proxy
   6 import Data.Text (Text)
   7
   8 import Language.Symantic.Typing.Type
   9
  10 -- * Type family 'Fam'
  11 -- | Apply the /type family/ selected by @fam@
  12 -- to a list of types (within a 'Proxy').
  13 type family Fam fam (hs::[*]) :: *
  14
  15 -- * Type 'Name_Fam'
  16 type Name_Fam = Text
  17
  18 -- * Type 'Proj_Fam'
  19 -- | Convenient type synonym wrapping 'Proj_FamR'
  20 -- to initiate its recursion.
  21 type Proj_Fam cs = Proj_FamR cs cs
  22
  23 -- | Project the 'Constraint' indexed by the given 'Type'
  24 -- onto its proof, captured by 'Con' when it holds.
  25 proj_fam
  26  :: forall fam cs hs. Proj_Fam cs fam
  27  => fam -> Types cs hs -> Maybe (Type cs (Fam fam hs))
  28 proj_fam = proj_famR (Proxy::Proxy cs)
  29
  30 -- ** Class 'Proj_FamR'
  31 -- | Intermediate type class to construct an instance of 'Proj_Fam'
  32 -- from many instances of 'Proj_FamC', one for each item of @cs@.
  33 --
  34 -- * @cs@: starting  list of /type constants/.
  35 -- * @rs@: remaining list of /type constants/.
  36 class Proj_FamR cs rs fam where
  37         proj_famR
  38          :: Proxy rs -> fam -> Types cs hs
  39          -> Maybe (Type cs (Fam fam hs))
  40         proj_famR _rs _fam _ty = Nothing
  41
  42 -- | Test whether @c@ handles the work of 'Proj_Fam' or not,
  43 -- or recurse on @rs@, preserving the starting list of /type constants/.
  44 instance
  45  ( Proj_FamC cs    fam c
  46  , Proj_FamR cs rs fam
  47  ) => Proj_FamR cs (Proxy c ': rs) fam where
  48         proj_famR _rs fam typ =
  49                 proj_famC (Proxy::Proxy c)  fam typ <|>
  50                 proj_famR (Proxy::Proxy rs) fam typ
  51 -- | End the recursion.
  52 instance Proj_FamR cs '[] fam
  53
  54 -- ** Class 'Proj_FamC'
  55 -- | Handle the work of 'Proj_Fam' for a given /type family/ @fam@ and /type constant/ @c@,
  56 -- that is: maybe it handles the given /type family/,
  57 -- and if so, maybe the /type family/ has an instance for the given 'Type'.
  58 class Proj_FamC cs fam c where
  59         proj_famC
  60          :: Proxy c -> fam -> Types cs hs
  61          -> Maybe (Type cs (Fam fam hs))
  62         proj_famC _c _fam _ty = Nothing