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_Proxy'
  33 type family Kind_of_Proxy (x:: *) :: Kind where
  34         Kind_of_Proxy (Proxy x) = Kind_of x
  35 -- | Convenient shorter type synonym.
  36 type Ki h = Kind_of_Proxy h
  37
  38 -- * Type 'EKind'
  39 -- | Existential for 'Kind'.
  40 data EKind = forall k. EKind (SKind k)
  41 instance Eq EKind where
  42         EKind x == EKind y
  43          | Just _ <- testEquality x y = True
  44         _x == _y = False
  45 instance Show EKind where
  46         show (EKind x) = show x
  47
  48 -- * Type 'SKind'
  49 -- | Singleton for 'Kind'.
  50 data SKind (k::Kind) where
  51         SKiTerm  :: SKind 'KiTerm
  52         SKiCon   :: SKind 'KiCon
  53         SKiArrow :: SKind a -> SKind b -> SKind (a ':> b)
  54 instance TestEquality SKind where
  55         testEquality SKiTerm SKiTerm = Just Refl
  56         testEquality SKiCon SKiCon = Just Refl
  57         testEquality (SKiArrow xa xb) (SKiArrow ya yb)
  58          | Just Refl <- testEquality xa ya
  59          , Just Refl <- testEquality xb yb
  60          = Just Refl
  61         testEquality _ _ = Nothing
  62 instance Show (SKind k) where
  63         show SKiTerm = "*"
  64         show SKiCon  = "Constraint"
  65         show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
  66
  67 -- * Type 'IKind'
  68 -- | Implicit for 'Kind'.
  69 class IKind (k::Kind) where
  70         kind :: SKind k
  71 instance IKind 'KiTerm where
  72         kind = SKiTerm
  73 instance IKind 'KiCon where
  74         kind = SKiCon
  75 instance (IKind a, IKind b) => IKind (a ':> b) where
  76         kind = kind `SKiArrow` kind