symantic/Language/Symantic/Typing/Family.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 module Language.Symantic.Typing.Family where
   5
   6 import Control.Applicative ((<|>))
   7 import Data.Proxy
   8 import Data.String (IsString(..))
   9
  10 import Language.Symantic.Parsing
  11 import Language.Symantic.Typing.Kind
  12 import Language.Symantic.Typing.Constant
  13 import Language.Symantic.Typing.Type
  14
  15 -- * Type 'Proj_TyFam'
  16 -- | Convenient type synonym wrapping 'Proj_TyFamR'
  17 -- to initiate its recursion.
  18 type Proj_TyFam cs = Proj_TyFamR cs cs
  19
  20 -- | Project the 'Constraint' indexed by the given 'Type'
  21 -- onto its proof, captured by 'Dict' when it holds.
  22 proj_TyFam
  23  :: forall fam src ctx ss cs hs.
  24  Proj_TyFam cs fam
  25  => fam -> TypesKi src ctx ss cs hs
  26  -> Maybe (Type src ctx ss cs (TyFam fam hs))
  27 proj_TyFam = proj_TyFamR (Proxy @cs)
  28
  29 -- ** Class 'Proj_TyFamR'
  30 -- | Intermediate type class to construct an instance of 'Proj_TyFam'
  31 -- from many instances of 'Proj_TyFamC', one for each item of @cs@.
  32 --
  33 -- * @cs@: starting  list of /type constants/.
  34 -- * @rs@: remaining list of /type constants/.
  35 class Proj_TyFamR (cs::[*]) (rs::[*]) fam where
  36         proj_TyFamR
  37          :: Proxy rs -> fam -> TypesKi src ctx ss cs hs
  38          -> Maybe (Type src ctx ss cs (TyFam fam hs))
  39         proj_TyFamR _rs _fam _ty = Nothing
  40
  41 -- | Test whether @c@ handles the work of 'Proj_TyFam' or not,
  42 -- or recurse on @rs@, preserving the starting list of /type constants/.
  43 instance
  44  ( Proj_TyFamC cs    fam c
  45  , Proj_TyFamR cs rs fam
  46  ) => Proj_TyFamR cs (Proxy c ': rs) fam where
  47         proj_TyFamR _rs fam typ =
  48                 proj_TyFamC (Proxy @c)  fam typ <|>
  49                 proj_TyFamR (Proxy @rs) fam typ
  50 -- | End the recursion.
  51 instance Proj_TyFamR cs '[] fam
  52
  53 -- ** Class 'Proj_TyFamC'
  54 -- | Handle the work of 'Proj_TyFam' for a given /type family/ @fam@ and /type constant/ @c@,
  55 -- that is: maybe the /type family/ has an instance for the given 'TypesKi'.
  56 class Proj_TyFamC cs fam (c::kc) where
  57         proj_TyFamC
  58          :: Proxy c -> fam -> TypesKi src ctx ss cs hs
  59          -> Maybe (Type src ctx ss cs (TyFam fam hs))
  60         proj_TyFamC _c _fam _ty = Nothing
  61
  62 unTyFam
  63  :: ( Inj_Error (Con_Type src ctx ss cs) err
  64     , Proj_TyFam cs fam
  65     , Show fam )
  66  => At src fam
  67  -> TypesKi src ctx ss cs hs
  68  -> (Type src ctx ss cs (TyFam fam hs) -> Either err ret)
  69  -> Either err ret
  70 unTyFam fam tys k =
  71         case proj_TyFam (unAt fam) tys of
  72          Just t -> k t
  73          Nothing -> Left $ inj_Error $
  74                 Con_TyFam
  75                  (fromString . show <$> fam)
  76                  (eTypesKi tys)
  77
  78 -- | Like 'TyFam', but 'sourceLess'.
  79 --
  80 -- NOTE: to be use with @TypeApplications@.
  81 tyFam :: forall fam hs ss cs src ctx.
  82  Source src
  83  => Inj_TyConst cs fam
  84  => Types src ctx ss cs hs
  85  -> Type src ctx ss cs (TyFam fam hs)
  86 tyFam = TyFam sourceLess (inj_TyConst @fam)
  87  -- NOTE: this requires @AllowAmbiguousTypes@.
  88
  89 {-
  90 tyFam
  91  :: Source src
  92  => Proj_TyFam cs fam
  93  => fam -> TypesKi src ctx ss cs hs
  94  -> Type src ctx ss cs (TyFam fam hs)
  95 tyFam fam hs =
  96         case proj_TyFam fam hs of
  97          Just h  -> h
  98          Nothing -> undefined
  99 infix 1 `tyFam`
 100
 101 tyQuant
 102  :: forall src ctx ss cs kv k.
 103     Source src
 104  => Inj_Kind kv
 105  => NameHint
 106  -> (forall (v::kv). Type src ctx ss cs v -> KT src ctx ss cs k)
 107  -> KT src ctx ss cs k
 108 tyQuant n f = KT $ TyQuant sourceLess n inj_Kind f
 109 -}