Language/Symantic/Typing/Kind.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE GADTs #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE PolyKinds #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE TypeInType #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 -- {-# LANGUAGE TypeInType #-}
  15 module Language.Symantic.Typing.Kind where
  16
  17 import qualified Data.Kind as Kind
  18 import Data.Proxy
  19 import Data.Type.Equality
  20 import GHC.Exts (Constraint)
  21 import GHC.Prim (Any)
  22
  23 -- * Type 'SKind'
  24 -- | Singleton for kind types.
  25 data SKind k where
  26         SKiType       :: SKind Kind.Type
  27         SKiConstraint :: SKind Constraint
  28         SKiArrow        :: SKind ka -> SKind kb -> SKind (ka -> kb)
  29 infixr 5 `SKiArrow`
  30
  31 instance Show (SKind k) where
  32         show SKiType = "*"
  33         show SKiConstraint  = "Constraint"
  34         show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
  35 instance TestEquality SKind where
  36         testEquality = eq_skind
  37
  38 eq_skind :: SKind x -> SKind y -> Maybe (x:~:y)
  39 eq_skind SKiType SKiType = Just Refl
  40 eq_skind SKiConstraint SKiConstraint = Just Refl
  41 eq_skind (SKiArrow xa xb) (SKiArrow ya yb)
  42  | Just Refl <- eq_skind xa ya
  43  , Just Refl <- eq_skind xb yb
  44  = Just Refl
  45 eq_skind _ _ = Nothing
  46
  47 -- * Type 'IKind'
  48 -- | Implicit 'SKind'.
  49 --
  50 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
  51 -- makes it fail to properly build an implicit 'SKind',
  52 -- this can however be worked around by having the class instances
  53 -- work on a data type 'Ty' instead of 'Data.Kind.Type',
  54 -- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'IKindP'.
  55 class (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k where
  56         kind :: SKind k
  57         kind = kindP (Proxy::Proxy (Ty_of_Type k))
  58 instance (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k
  59
  60 -- ** Type 'IKindP'
  61 class IKindP k where
  62         kindP :: Proxy k -> SKind (Type_of_Ty k)
  63 instance IKindP Constraint where
  64         kindP _ = SKiConstraint
  65 instance IKindP Ty where
  66         kindP _ = SKiType
  67 instance (IKindP a, IKindP b) => IKindP (a -> b) where
  68         kindP _ = kindP (Proxy::Proxy a) `SKiArrow` kindP (Proxy::Proxy b)
  69
  70 -- ** Type 'Ty'
  71 data Ty
  72
  73 -- ** Type family 'Ty_of_Type'
  74 type family   Ty_of_Type (ty::Kind.Type) :: Kind.Type
  75 type instance Ty_of_Type Kind.Type  = Ty
  76 type instance Ty_of_Type Constraint = Constraint
  77 type instance Ty_of_Type (a -> b)   = Ty_of_Type a -> Ty_of_Type b
  78
  79 -- ** Type family 'Type_of_Ty'
  80 type family   Type_of_Ty (ty::Kind.Type) :: Kind.Type
  81 type instance Type_of_Ty Ty         = Kind.Type
  82 type instance Type_of_Ty Constraint = Constraint
  83 type instance Type_of_Ty (a -> b)   = Type_of_Ty a -> Type_of_Ty b
  84
  85 -- * Type 'EKind'
  86 -- | Existential for 'Kind'.
  87 data EKind = forall k. EKind (SKind k)
  88 instance Eq EKind where
  89         EKind x == EKind y
  90          | Just _ <- eq_skind x y = True
  91         _x == _y = False
  92 instance Show EKind where
  93         show (EKind x) = show x
  94
  95 -- * Type family 'Kind_Of'
  96 type family   Kind_Of (x::k) :: Kind.Type
  97 type instance Kind_Of (x::Constraint) = Constraint
  98 type instance Kind_Of (x::Kind.Type)  = Kind.Type
  99 type instance Kind_Of (x::a -> b)     = Kind_Of (Any::a) -> Kind_Of (Any::b)
 100
 101 {-
 102 instance Show (x :~~: y) where
 103         show _ = "HRefl"
 104
 105 type family Eq_KindF (x::kx) (y::ky) :: Bool where
 106         Eq_KindF (x::k) (y::k) = 'True
 107         Eq_KindF x y = 'False
 108
 109 type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
 110 class Eq_KindB (b::Bool) (x::kx) (y::ky) where
 111         eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
 112 instance Eq_KindB 'False x y where
 113         eq_kindB _b _x _y = Nothing
 114 instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
 115         eq_kindB _b _x _y = Just HRefl
 116 instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
 117         eq_kindB _b _x _y = Just HRefl
 118 instance
 119  ( Eq_Kind (Any::k0) (Any::k2)
 120  , Eq_Kind (Any::k1) (Any::k3)
 121  ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
 122         eq_kindB _b _x _y
 123          | Just HRefl <- eq_kind (Proxy::Proxy (Any::k0)) (Proxy::Proxy (Any::k2))
 124          , Just HRefl <- eq_kind (Proxy::Proxy (Any::k1)) (Proxy::Proxy (Any::k3))
 125          = Just HRefl
 126         eq_kindB _b _x _y = Nothing
 127
 128 eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
 129 eq_kind = eq_kindB (Proxy::Proxy (Eq_KindF x y))
 130 -}