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