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 -}