]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Typing/Kind.hs
Simplify the Constraint projection
[haskell/symantic.git] / Language / Symantic / Typing / Kind.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE Rank2Types #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE TypeOperators #-}
7 module Language.Symantic.Typing.Kind where
8
9 import Data.Proxy
10 import Data.Type.Equality
11 import GHC.Prim (Constraint)
12
13 -- * Type 'Kind'
14 -- | /Type of types/.
15 data Kind
16 = KiTerm -- ^ \*
17 | KiCon -- ^ 'Constraint'
18 | (:>) Kind Kind -- ^ \->
19 infixr 0 :>
20
21 -- * Type family 'Kind_of'
22 -- | To be completed on need, according to the /type constants/ used.
23 type family Kind_of (x::k) :: Kind
24 type instance Kind_of (x:: Constraint) = 'KiCon
25 type instance Kind_of (x:: * -> Constraint) = 'KiTerm ':> 'KiCon
26 type instance Kind_of (x:: *) = 'KiTerm
27 type instance Kind_of (x:: * -> *) = 'KiTerm ':> 'KiTerm
28 type instance Kind_of (x:: (* -> *) -> *) = ('KiTerm ':> 'KiTerm) ':> 'KiTerm
29 type instance Kind_of (x:: (* -> *) -> Constraint) = ('KiTerm ':> 'KiTerm) ':> 'KiCon
30 type instance Kind_of (x:: * -> * -> *) = 'KiTerm ':> 'KiTerm ':> 'KiTerm
31
32 -- ** Type family 'Kind_of_UnProxy'
33 type family Kind_of_UnProxy (x:: *) :: Kind where
34 Kind_of_UnProxy (Proxy x) = Kind_of x
35
36 -- * Type 'EKind'
37 -- | Existential for 'Kind'.
38 data EKind = forall k. EKind (SKind k)
39 instance Eq EKind where
40 EKind x == EKind y
41 | Just _ <- testEquality x y = True
42 _x == _y = False
43 instance Show EKind where
44 show (EKind x) = show x
45
46 -- * Type 'SKind'
47 -- | Singleton for 'Kind'.
48 data SKind (k::Kind) where
49 SKiTerm :: SKind 'KiTerm
50 SKiCon :: SKind 'KiCon
51 SKiArrow :: SKind a -> SKind b -> SKind (a ':> b)
52 instance TestEquality SKind where
53 testEquality SKiTerm SKiTerm = Just Refl
54 testEquality SKiCon SKiCon = Just Refl
55 testEquality (SKiArrow xa xb) (SKiArrow ya yb)
56 | Just Refl <- testEquality xa ya
57 , Just Refl <- testEquality xb yb
58 = Just Refl
59 testEquality _ _ = Nothing
60 instance Show (SKind k) where
61 show SKiTerm = "*"
62 show SKiCon = "Constraint"
63 show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
64
65 -- * Type 'IKind'
66 -- | Implicit for 'Kind'.
67 class IKind (k::Kind) where
68 kind :: SKind k
69 instance IKind 'KiTerm where
70 kind = SKiTerm
71 instance IKind 'KiCon where
72 kind = SKiCon
73 instance (IKind a, IKind b) => IKind (a ':> b) where
74 kind = kind `SKiArrow` kind