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