symantic/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.String (IsString(..))
   8
   9 import Language.Symantic.Parsing
  10 import Language.Symantic.Typing.Kind
  11 import Language.Symantic.Typing.Type
  12
  13 -- * Type family 'TyFam'
  14 -- | Apply the /type family/ selected by @fam@
  15 -- to a list of types (within a 'Proxy').
  16 type family TyFam fam (hs::[*]) :: *
  17
  18 -- * Type 'Proj_TyFam'
  19 -- | Convenient type synonym wrapping 'Proj_TyFamR'
  20 -- to initiate its recursion.
  21 type Proj_TyFam cs = Proj_TyFamR cs cs
  22
  23 -- | Project the 'Constraint' indexed by the given 'Type'
  24 -- onto its proof, captured by 'Dict' when it holds.
  25 proj_TyFam
  26  :: forall fam src cs hs.
  27  Proj_TyFam cs fam
  28  => fam -> Types src cs hs
  29  -> Maybe (Type src cs (TyFam fam hs))
  30 proj_TyFam = proj_TyFamR (Proxy @cs)
  31
  32 -- ** Class 'Proj_TyFamR'
  33 -- | Intermediate type class to construct an instance of 'Proj_TyFam'
  34 -- from many instances of 'Proj_TyFamC', one for each item of @cs@.
  35 --
  36 -- * @cs@: starting  list of /type constants/.
  37 -- * @rs@: remaining list of /type constants/.
  38 class Proj_TyFamR (cs::[*]) (rs::[*]) fam where
  39         proj_TyFamR
  40          :: Proxy rs -> fam -> Types src cs hs
  41          -> Maybe (Type src cs (TyFam fam hs))
  42         proj_TyFamR _rs _fam _ty = Nothing
  43
  44 -- | Test whether @c@ handles the work of 'Proj_TyFam' or not,
  45 -- or recurse on @rs@, preserving the starting list of /type constants/.
  46 instance
  47  ( Proj_TyFamC cs    fam c
  48  , Proj_TyFamR cs rs fam
  49  ) => Proj_TyFamR cs (Proxy c ': rs) fam where
  50         proj_TyFamR _rs fam typ =
  51                 proj_TyFamC (Proxy @c)  fam typ <|>
  52                 proj_TyFamR (Proxy @rs) fam typ
  53 -- | End the recursion.
  54 instance Proj_TyFamR cs '[] fam
  55
  56 -- ** Class 'Proj_TyFamC'
  57 -- | Handle the work of 'Proj_TyFam' for a given /type family/ @fam@ and /type constant/ @c@,
  58 -- that is: maybe it handles the given /type family/,
  59 -- and if so, maybe the /type family/ has an instance for the given 'Type'.
  60 class Proj_TyFamC cs fam (c::kc) where
  61         proj_TyFamC
  62          :: Proxy c -> fam -> Types src cs hs
  63          -> Maybe (Type src cs (TyFam fam hs))
  64         proj_TyFamC _c _fam _ty = Nothing
  65
  66 unTyFam
  67  :: ( Inj_Error (Con_Type src cs) err
  68     , Proj_TyFam cs fam
  69     , Show fam )
  70  => At src fam
  71  -> Types src cs hs
  72  -> (Type src cs (TyFam fam hs) -> Either err ret)
  73  -> Either err ret
  74 unTyFam fam tys k =
  75         case proj_TyFam (unAt fam) tys of
  76          Just t -> k t
  77          Nothing -> Left $ inj_Error $
  78                 Con_TyFam
  79                  (fromString . show <$> fam)
  80                  (eTypes tys)