Language/Symantic/Typing/Kind.hs

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