]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Typing/Kind.hs
Add Gram_Term.
[haskell/symantic.git] / Language / Symantic / Typing / Kind.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE UndecidableInstances #-}
4 module Language.Symantic.Typing.Kind where
5
6 import qualified Data.Kind as Kind
7 import Data.Proxy
8 import Data.Type.Equality
9 import GHC.Exts (Constraint)
10 import GHC.Prim (Any)
11
12 -- * Type 'SKind'
13 -- | Singleton for kind types.
14 data SKind k where
15 SKiType :: SKind Kind.Type
16 SKiConstraint :: SKind Constraint
17 SKiArrow :: SKind ka -> SKind kb -> SKind (ka -> kb)
18 infixr 5 `SKiArrow`
19
20 instance Show (SKind k) where
21 show SKiType = "*"
22 show SKiConstraint = "Constraint"
23 show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
24 instance TestEquality SKind where
25 testEquality = eq_skind
26
27 eq_skind :: SKind x -> SKind y -> Maybe (x:~:y)
28 eq_skind SKiType SKiType = Just Refl
29 eq_skind SKiConstraint SKiConstraint = Just Refl
30 eq_skind (SKiArrow xa xb) (SKiArrow ya yb)
31 | Just Refl <- eq_skind xa ya
32 , Just Refl <- eq_skind xb yb
33 = Just Refl
34 eq_skind _ _ = Nothing
35
36 -- * Type 'IKind'
37 -- | Implicit 'SKind'.
38 --
39 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
40 -- makes it fail to properly build an implicit 'SKind',
41 -- this can however be worked around by having the class instances
42 -- work on a data type 'Ty' instead of 'Data.Kind.Type',
43 -- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'IKindP'.
44 class (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k where
45 kind :: SKind k
46 kind = kindP (Proxy @(Ty_of_Type k))
47 instance (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k
48
49 -- ** Type 'IKindP'
50 class IKindP k where
51 kindP :: Proxy k -> SKind (Type_of_Ty k)
52 instance IKindP Constraint where
53 kindP _ = SKiConstraint
54 instance IKindP Ty where
55 kindP _ = SKiType
56 instance (IKindP a, IKindP b) => IKindP (a -> b) where
57 kindP _ = kindP (Proxy @a) `SKiArrow` kindP (Proxy @b)
58
59 -- ** Type 'Ty'
60 -- | FIXME: to be removed when
61 -- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
62 -- will be fixed.
63 data Ty
64
65 -- ** Type family 'Ty_of_Type'
66 type family Ty_of_Type (typ::Kind.Type) :: Kind.Type
67 type instance Ty_of_Type Kind.Type = Ty
68 type instance Ty_of_Type Constraint = Constraint
69 type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b
70
71 -- ** Type family 'Type_of_Ty'
72 type family Type_of_Ty (typ::Kind.Type) :: Kind.Type
73 type instance Type_of_Ty Ty = Kind.Type
74 type instance Type_of_Ty Constraint = Constraint
75 type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b
76
77 -- * Type 'EKind'
78 -- | Existential for 'Kind'.
79 data EKind = forall k. EKind (SKind k)
80 instance Eq EKind where
81 EKind x == EKind y
82 | Just _ <- eq_skind x y = True
83 _x == _y = False
84 instance Show EKind where
85 show (EKind x) = show x
86
87 -- * Type family 'Kind_Of'
88 type family Kind_Of (x::k) :: Kind.Type
89 type instance Kind_Of (x::Constraint) = Constraint
90 type instance Kind_Of (x::Kind.Type) = Kind.Type
91 type instance Kind_Of (x::a -> b) = Kind_Of (Any::a) -> Kind_Of (Any::b)
92
93 {-
94 instance Show (x :~~: y) where
95 show _ = "HRefl"
96
97 type family Eq_KindF (x::kx) (y::ky) :: Bool where
98 Eq_KindF (x::k) (y::k) = 'True
99 Eq_KindF x y = 'False
100
101 type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
102 class Eq_KindB (b::Bool) (x::kx) (y::ky) where
103 eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
104 instance Eq_KindB 'False x y where
105 eq_kindB _b _x _y = Nothing
106 instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
107 eq_kindB _b _x _y = Just HRefl
108 instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
109 eq_kindB _b _x _y = Just HRefl
110 instance
111 ( Eq_Kind (Any::k0) (Any::k2)
112 , Eq_Kind (Any::k1) (Any::k3)
113 ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
114 eq_kindB _b _x _y
115 | Just HRefl <- eq_kind (Proxy @(Any::k0)) (Proxy @(Any::k2))
116 , Just HRefl <- eq_kind (Proxy @(Any::k1)) (Proxy @(Any::k3))
117 = Just HRefl
118 eq_kindB _b _x _y = Nothing
119
120 eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
121 eq_kind = eq_kindB (Proxy @(Eq_KindF x y))
122 -}