symantic/Language/Symantic/Typing/Constant.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE TypeInType #-}
   5 module Language.Symantic.Typing.Constant where
   6
   7 import qualified Data.Kind as K
   8 import Data.Proxy
   9 import Data.Type.Equality
  10
  11 import Language.Symantic.Helper.Data.Type.List
  12 import Language.Symantic.Helper.Data.Type.Peano
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing.Kind
  15
  16 -- | Like (:~:) but prove also that the kinds are equal.
  17 data (:~~:) (a::ka) (b::kb) where
  18         KRefl :: a :~~: a
  19
  20 -- * Type 'TyConst'
  21 -- | A /type constant/,
  22 -- indexed at the Haskell type and term level amongst a list of them.
  23 -- When used, @c@ is actually wrapped within a 'Proxy'
  24 -- to be able to handle constants of different 'Kind's.
  25 data TyConst src (cs::[K.Type]) (c::k) where
  26         TyConstZ :: Kind src k -> TyConst src (Proxy c ': cs) (c::k)
  27         TyConstS :: TyConst src cs c -> TyConst src (not_c ': cs) c
  28 infixr 5 `TyConstS`
  29
  30 eqTyConst :: TyConst xs cs (x::k) -> TyConst ys cs (y::k) -> Maybe (x:~:y)
  31 eqTyConst TyConstZ{} TyConstZ{}     = Just Refl
  32 eqTyConst (TyConstS x) (TyConstS y) = eqTyConst x y
  33 eqTyConst _ _                       = Nothing
  34
  35 eqKiTyConst :: TyConst xs cs (x::kx) -> TyConst ys cs (y::ky) -> Maybe (x:~~:y)
  36 eqKiTyConst TyConstZ{} TyConstZ{}     = Just KRefl
  37 eqKiTyConst (TyConstS x) (TyConstS y) = eqKiTyConst x y
  38 eqKiTyConst _ _                       = Nothing
  39
  40 instance TestEquality (TyConst src cs) where
  41         testEquality = eqTyConst
  42
  43 kindTyConst :: TyConst src cs (h::k) -> Kind src k
  44 kindTyConst (TyConstZ ki) = ki
  45 kindTyConst (TyConstS c)  = kindTyConst c
  46
  47 -- * Type 'Inj_TyConst'
  48 -- | Convenient type synonym wrapping 'Inj_TyConstP'
  49 -- applied on the correct 'Index'.
  50 type Inj_TyConst cs c = Inj_TyConstP (Index cs (Proxy c)) cs c
  51
  52 -- | Inject a given /type constant/ @c@ into a list of them,
  53 -- by returning a proof that 'Proxy'@ c@ is in @cs@.
  54 inj_TyConst :: forall src cs c. (Inj_TyConst cs c, Source src) => TyConst src cs c
  55 inj_TyConst = inj_TyConstP (Proxy @(Index cs (Proxy c)))
  56
  57 -- ** Class 'Inj_TyConstP'
  58 class Inj_TyConstP p cs c where
  59         inj_TyConstP :: Source src => Proxy p -> TyConst src cs c
  60 {- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933
  61          which makes it fail to calculate the right kind,
  62          it seems to wrongly reuse the kind of the first use (sic)…
  63 instance IKind k => Inj_TyConstP Zero (Proxy c ': cs) (c::k) where
  64         inj_TyConstP _ = TyConstZ kind
  65 -}
  66 instance
  67  ( IKindP (Ty_of_Type k)
  68  , Type_of_Ty (Ty_of_Type k) ~ k
  69  ) => Inj_TyConstP Zero (Proxy c ': cs) (c::k) where
  70         inj_TyConstP _ = TyConstZ (kindP (Proxy @(Ty_of_Type k)) sourceLess)
  71 instance Inj_TyConstP p cs c => Inj_TyConstP (Succ p) (not_c ': cs) c where
  72         inj_TyConstP _p = TyConstS (inj_TyConstP (Proxy @p))
  73
  74 -- ** Type 'Inj_TyConsts'
  75 type Inj_TyConsts cs cs_to_inj
  76  = Concat_Constraints (Inj_TyConstsR cs cs_to_inj)
  77
  78 -- *** Type family 'Inj_TyConstsR'
  79 type family Inj_TyConstsR cs cs_to_inj where
  80  Inj_TyConstsR cs '[] = '[]
  81  Inj_TyConstsR cs (Proxy x ': xs) = Inj_TyConst cs x ': Inj_TyConstsR cs xs
  82
  83 -- * Class 'Proj_TyConst'
  84 -- | Convenient type synonym wrapping 'Proj_TyConstP'
  85 -- applied on the correct 'Index'.
  86 type Proj_TyConst cs c = Proj_TyConstP (Index cs (Proxy c)) cs c
  87
  88 -- | Project a 'TyConst' onto a Haskell type level /type constant/ @c@,
  89 -- returning a proof that the 'TyConst' indexes @c@ iif. it's the case.
  90 proj_TyConst :: forall src cs k (c::k) (u::k).
  91  Proj_TyConst cs c => TyConst src cs u -> Proxy c -> Maybe (c :~: u)
  92 proj_TyConst = proj_TyConstP (Proxy @(Index cs (Proxy c)))
  93
  94 -- | Project a 'TyConst' onto a Haskell type level /type constant/ @c@,
  95 -- returning a proof that the 'TyConst' indexes @c@ iif. it's the case.
  96 projTyConst :: forall c src cs u.
  97  Proj_TyConst cs c => TyConst src cs u -> Maybe (c :~: u)
  98 projTyConst u = proj_TyConstP (Proxy @(Index cs (Proxy c))) u (Proxy @c)
  99
 100 -- | Like 'projTyConst', but prove also that the 'Kind's are equal.
 101 projKiTyConst :: forall kc (c::kc) src cs ku (u::ku).
 102  IKind kc => Proj_TyConst cs c =>
 103  TyConst src cs u -> Maybe (c :~~: u)
 104 projKiTyConst u = do
 105         Refl <- eqKi (kind @kc @()) (kindTyConst u)
 106         Refl <- proj_TyConstP (Proxy @(Index cs (Proxy c))) u (Proxy @c)
 107         Just KRefl
 108
 109 (=?) :: forall src cs c u. Proj_TyConst cs c => TyConst src cs u -> Proxy c -> Maybe (c :~: u)
 110 (=?) = proj_TyConstP (Proxy @(Index cs (Proxy c)))
 111
 112 -- ** Type 'Proj_TyConstP'
 113 class Proj_TyConstP p cs c where
 114         proj_TyConstP :: Proxy p -> TyConst src cs u -> Proxy c -> Maybe (c :~: u)
 115 instance Proj_TyConstP Zero (Proxy c ': cs) c where
 116         proj_TyConstP _p TyConstZ{} _c = Just Refl
 117         proj_TyConstP _p TyConstS{} _c = Nothing
 118 instance Proj_TyConstP p cs c => Proj_TyConstP (Succ p) (not_c ': cs) c where
 119         proj_TyConstP _p TyConstZ{} _c  = Nothing
 120         proj_TyConstP _p (TyConstS u) c = proj_TyConstP (Proxy @p) u c
 121
 122 -- ** Type 'Proj_TyConsts'
 123 type Proj_TyConsts cs cs_to_proj
 124  = Concat_Constraints (Proj_TyConstsR cs cs_to_proj)
 125
 126 -- *** Type family 'Proj_TyConstsR'
 127 type family Proj_TyConstsR cs cs_to_proj where
 128  Proj_TyConstsR cs '[] = '[]
 129  Proj_TyConstsR cs (Proxy x ': xs) = Proj_TyConst cs x ': Proj_TyConstsR cs xs
 130
 131 -- * Class 'Show_TyConst'
 132 class Show_TyConst cs where
 133         show_TyConst :: TyConst src cs c -> String
 134
 135 -- deriving instance Show (TyConst cs c)
 136 instance Show_TyConst cs => Show (TyConst src cs c) where
 137         show = show_TyConst
 138 instance Show_TyConst '[] where
 139         show_TyConst = error "Show_TyConst unreachable pattern"
 140
 141 -- TODO: move each of these to a dedicated module.
 142 instance Show_TyConst cs => Show_TyConst (Proxy Fractional ': cs) where
 143         show_TyConst TyConstZ{} = "Fractional"
 144         show_TyConst (TyConstS c) = show_TyConst c