Language/Symantic/Typing/Family.hs

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