]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Constant.hs
Add IsString instances.
[haskell/symantic.git] / 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 = eq_skind (kind_of_TyConst x) (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 -- * Class 'Proj_TyConst'
64 -- | Convenient type synonym wrapping 'Proj_TyConstP'
65 -- applied on the correct 'Index'.
66 type Proj_TyConst cs c = Proj_TyConstP (Index cs (Proxy c)) cs c
67
68 -- | Project a 'TyConst' onto a Haskell type level /type constant/ @c@,
69 -- returning a proof that the 'TyConst' indexes @c@ iif. it's the case.
70 proj_TyConst :: forall cs k (c::k) (u::k).
71 Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
72 proj_TyConst = proj_TyConstP (Proxy @(Index cs (Proxy c)))
73
74 (=?) :: forall cs c u. Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
75 (=?) = proj_TyConstP (Proxy @(Index cs (Proxy c)))
76
77 -- ** Type 'Proj_TyConstP'
78 class Proj_TyConstP p cs c where
79 proj_TyConstP :: Proxy p -> TyConst cs u -> Proxy c -> Maybe (c :~: u)
80 instance Proj_TyConstP Zero (Proxy c ': cs) c where
81 proj_TyConstP _p TyConstZ{} _c = Just Refl
82 proj_TyConstP _p TyConstS{} _c = Nothing
83 instance Proj_TyConstP p cs c => Proj_TyConstP (Succ p) (not_c ': cs) c where
84 proj_TyConstP _p TyConstZ{} _c = Nothing
85 proj_TyConstP _p (TyConstS u) c = proj_TyConstP (Proxy @p) u c
86
87 -- ** Type 'Proj_TyConsts'
88 type Proj_TyConsts cs cs_to_proj
89 = Concat_Constraints (Proj_TyConstsR cs cs_to_proj)
90
91 -- *** Type family 'Proj_TyConstsR'
92 type family Proj_TyConstsR cs cs_to_proj where
93 Proj_TyConstsR cs '[] = '[]
94 Proj_TyConstsR cs (Proxy x ': xs) = Proj_TyConst cs x ': Proj_TyConstsR cs xs
95
96 -- * Class 'Show_TyConst'
97 class Show_TyConst cs where
98 show_TyConst :: TyConst cs c -> String
99
100 -- deriving instance Show (TyConst cs c)
101 instance Show_TyConst cs => Show (TyConst cs c) where
102 show = show_TyConst
103 instance Show_TyConst '[] where
104 show_TyConst = error "Show_TyConst unreachable pattern"
105
106 -- TODO: move each of these to a dedicated module.
107 instance Show_TyConst cs => Show_TyConst (Proxy Fractional ': cs) where
108 show_TyConst TyConstZ{} = "Fractional"
109 show_TyConst (TyConstS c) = show_TyConst c