]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Typing/Kind.hs
Add Compiling.Show.
[haskell/symantic.git] / Language / Symantic / Typing / Kind.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 -- {-# LANGUAGE TypeInType #-}
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::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::Proxy a) `SKiArrow` kindP (Proxy::Proxy b)
58
59 -- ** Type 'Ty'
60 data Ty
61
62 -- ** Type family 'Ty_of_Type'
63 type family Ty_of_Type (typ::Kind.Type) :: Kind.Type
64 type instance Ty_of_Type Kind.Type = Ty
65 type instance Ty_of_Type Constraint = Constraint
66 type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b
67
68 -- ** Type family 'Type_of_Ty'
69 type family Type_of_Ty (typ::Kind.Type) :: Kind.Type
70 type instance Type_of_Ty Ty = Kind.Type
71 type instance Type_of_Ty Constraint = Constraint
72 type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b
73
74 -- * Type 'EKind'
75 -- | Existential for 'Kind'.
76 data EKind = forall k. EKind (SKind k)
77 instance Eq EKind where
78 EKind x == EKind y
79 | Just _ <- eq_skind x y = True
80 _x == _y = False
81 instance Show EKind where
82 show (EKind x) = show x
83
84 -- * Type family 'Kind_Of'
85 type family Kind_Of (x::k) :: Kind.Type
86 type instance Kind_Of (x::Constraint) = Constraint
87 type instance Kind_Of (x::Kind.Type) = Kind.Type
88 type instance Kind_Of (x::a -> b) = Kind_Of (Any::a) -> Kind_Of (Any::b)
89
90 {-
91 instance Show (x :~~: y) where
92 show _ = "HRefl"
93
94 type family Eq_KindF (x::kx) (y::ky) :: Bool where
95 Eq_KindF (x::k) (y::k) = 'True
96 Eq_KindF x y = 'False
97
98 type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
99 class Eq_KindB (b::Bool) (x::kx) (y::ky) where
100 eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
101 instance Eq_KindB 'False x y where
102 eq_kindB _b _x _y = Nothing
103 instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
104 eq_kindB _b _x _y = Just HRefl
105 instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
106 eq_kindB _b _x _y = Just HRefl
107 instance
108 ( Eq_Kind (Any::k0) (Any::k2)
109 , Eq_Kind (Any::k1) (Any::k3)
110 ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
111 eq_kindB _b _x _y
112 | Just HRefl <- eq_kind (Proxy::Proxy (Any::k0)) (Proxy::Proxy (Any::k2))
113 , Just HRefl <- eq_kind (Proxy::Proxy (Any::k1)) (Proxy::Proxy (Any::k3))
114 = Just HRefl
115 eq_kindB _b _x _y = Nothing
116
117 eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
118 eq_kind = eq_kindB (Proxy::Proxy (Eq_KindF x y))
119 -}