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