symantic/Language/Symantic/Typing/Constant.hs

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