Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE TypeInType #-}
   3 {-# LANGUAGE UndecidableInstances #-}
   4 {-# LANGUAGE ViewPatterns #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Language.Symantic.Typing.Type where
   7
   8 import Data.Monoid ((<>))
   9 import Data.Proxy
  10 import Data.Maybe (fromMaybe, isJust)
  11 import Data.Text (Text)
  12 import Data.Type.Equality
  13 import qualified Data.Kind as K
  14
  15 import Language.Symantic.Typing.Kind
  16 import Language.Symantic.Typing.Constant
  17 import Language.Symantic.Parsing.Token
  18
  19 -- * Type 'Type'
  20
  21 -- | /Type of terms/.
  22 --
  23 -- * @cs@: /type constants/, fixed at compile time.
  24 -- * @h@: indexed Haskell type.
  25 --
  26 -- * 'TyConst': /type constant/, selected amongst @cs@.
  27 -- * @(:$)@: /type application/.
  28 data Type (cs::[K.Type]) (h::k) where
  29         TyConst :: Const cs c -> Type  cs c
  30         (:$) :: Type cs f -> Type cs x -> Type cs (f x)
  31         -- TODO: TyVar :: SKind k -> Type cs (v::k)
  32 infixl 9 :$
  33
  34 -- | 'Type' constructor to be used
  35 -- with @TypeApplications@
  36 -- and @NoMonomorphismRestriction@.
  37 ty :: forall c cs. Inj_Const cs c => Type cs c
  38 ty = TyConst inj_const
  39  -- NOTE: The forall brings @c@ first in the type variables,
  40  -- which is convenient to use @TypeApplications@.
  41
  42 instance TestEquality (Type cs) where
  43         testEquality = eq_type
  44 instance Eq (Type cs h) where
  45         _x == _y = True
  46 instance Show_Const cs => Show (Type cs h) where
  47         show = show_type
  48 -- deriving instance Show_Const cs => Show (Type cs h)
  49
  50 kind_of :: Type cs (h::k) -> SKind k
  51 kind_of t =
  52         case t of
  53          TyConst c -> kind_of_const c
  54          f :$ _x ->
  55                 case kind_of f of
  56                  _kx `SKiArrow` kf -> kf
  57
  58 eq_type
  59  :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
  60 eq_type (TyConst x) (TyConst y)
  61  | Just Refl <- testEquality x y
  62  = Just Refl
  63 eq_type (xf :$ xx) (yf :$ yx)
  64  | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
  65  , Just Refl <- eq_type xf yf
  66  , Just Refl <- eq_type xx yx
  67  = Just Refl
  68 eq_type _ _ = Nothing
  69
  70 eq_kind_type
  71  :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
  72 eq_kind_type (TyConst x) (TyConst y)
  73  | Just Refl <- eq_kind_const x y
  74  = Just Refl
  75 eq_kind_type (xf :$ xx) (yf :$ yx)
  76  | Just Refl <- eq_kind_type xf yf
  77  , Just Refl <- eq_kind_type xx yx
  78  = Just Refl
  79 eq_kind_type _x _y = Nothing
  80
  81 show_type :: Show_Const cs => Type cs h -> String
  82 show_type (TyConst c) = show c
  83 show_type ((:$) f@(:$){} a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
  84 show_type ((:$) f@(:$){} a) = "(" <> show_type f <> ") " <> show_type a
  85 show_type ((:$) f a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
  86 show_type ((:$) f a) = show_type f <> " " <> show_type a
  87 -- show_type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
  88
  89 -- * Type 'EType'
  90 -- | Existential for 'Type'.
  91 data EType cs = forall h. EType (Type cs h)
  92
  93 instance Eq (EType cs) where
  94         EType x == EType y
  95          | Just Refl <- eq_kind_type x y
  96          = isJust $ eq_type x y
  97         _x == _y = False
  98 instance Show_Const cs => Show (EType cs) where
  99         show (EType t) = show t
 100
 101 -- * Type 'KType'
 102 -- | Existential for 'Type' of a known 'Kind'.
 103 data KType cs k = forall (h::k). KType (Type cs h)
 104
 105 instance Eq (KType cs ki) where
 106         KType x == KType y = isJust $ eq_type x y
 107 instance Show_Const cs => Show (KType cs ki) where
 108         show (KType t) = show_type t
 109
 110 -- * Type 'Token_Type'
 111 type Token_Type = Type '[] ()
 112
 113 data instance TokenT meta ts (Proxy Token_Type)
 114  = Token_Type Text [EToken meta ts]
 115 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
 116 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))
 117
 118 instance Const_from Text cs => Const_from Text (Proxy Token_Type ': cs) where
 119         const_from "Type" k = k (ConstZ kind)
 120         const_from s k = const_from s $ k . ConstS
 121 instance Show_Const cs => Show_Const (Proxy Token_Type ': cs) where
 122         show_const ConstZ{} = "Type"
 123         show_const (ConstS c) = show_const c
 124
 125 -- * Class 'Compile_Type'
 126 -- | Try to build a 'Type' from raw data.
 127 class Compile_Type ts cs where
 128         compile_type
 129          :: ( MonoLift (Error_Type meta ts) err
 130             , MonoLift (Constraint_Kind meta ts) err )
 131          => EToken meta ts
 132          -> (forall k h. Type cs (h::k) -> Either err ret)
 133          -> Either err ret
 134
 135 -- ** Type 'Constraint_Kind'
 136 data Constraint_Kind meta ts
 137  =   Constraint_Kind_Eq    (At meta ts EKind) (At meta ts EKind)
 138  |   Constraint_Kind_Arrow (At meta ts EKind)
 139 deriving instance (Eq_TokenR meta ts ts) => Eq (Constraint_Kind meta ts)
 140 deriving instance (Show_TokenR meta ts ts) => Show (Constraint_Kind meta ts)
 141
 142 check_kind
 143  :: MonoLift (Constraint_Kind meta ts) err
 144  => At meta ts (SKind x)
 145  -> At meta ts (SKind y)
 146  -> ((x :~: y) -> Either err ret) -> Either err ret
 147 check_kind x y k =
 148         case unAt x `eq_skind` unAt y of
 149          Just Refl -> k Refl
 150          Nothing -> Left $ olift $
 151                 Constraint_Kind_Eq (EKind <$> x) (EKind <$> y)
 152
 153 check_kind_arrow
 154  :: MonoLift (Constraint_Kind meta ts) err
 155  => At meta ts (SKind x)
 156  -> (forall a b. (x :~: (a -> b)) -> SKind a -> SKind b -> Either err ret)
 157  -> Either err ret
 158 check_kind_arrow x k =
 159         case unAt x of
 160          a `SKiArrow` b -> k Refl a b
 161          _ -> Left $ olift $
 162                 Constraint_Kind_Arrow (EKind <$> x)
 163
 164 -- ** Type 'Error_Type'
 165 data Error_Type meta ts
 166  =   Error_Type_Token_invalid    (EToken meta ts)
 167  |   Error_Type_Constant_unknown (At meta ts Text)
 168  |   Error_Type_Constraint_Kind  (Constraint_Kind meta ts)
 169 deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
 170 deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)
 171
 172 instance
 173  ( Const_from Text cs
 174  , Proj_Token ts Token_Type
 175  ) => Compile_Type ts cs where
 176         compile_type
 177          :: forall meta err ret.
 178          ( MonoLift (Error_Type meta ts) err
 179          , MonoLift (Constraint_Kind meta ts) err
 180          ) => EToken meta ts
 181          -> (forall k h. Type cs (h::k) -> Either err ret)
 182          -> Either err ret
 183         compile_type tok@(proj_etoken -> Just (Token_Type cst args)) kk =
 184                 fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
 185                 const_from cst $ \c -> Just $
 186                 go args (TyConst c) kk
 187                 where
 188                 go :: [EToken meta ts]
 189                  -> Type cs h
 190                  -> (forall k' h'. Type cs (h'::k') -> Either err ret)
 191                  -> Either err ret
 192                 go [] typ k = k typ
 193                 go (tok_x:tok_xs) ty_f k =
 194                         compile_type tok_x $ \(ty_x::Type cs (h'::k')) ->
 195                         check_kind_arrow
 196                          (At (Just tok) $ kind_of ty_f) $ \Refl ki_f_a _ki_f_b ->
 197                         check_kind
 198                          (At (Just tok) ki_f_a)
 199                          (At (Just tok_x) $ kind_of ty_x) $ \Refl ->
 200                         go tok_xs (ty_f :$ ty_x) k
 201         compile_type tok _k = Left $ olift $ Error_Type_Token_invalid tok
 202
 203 -- * Type 'Types'
 204 data Types cs (hs::[K.Type]) where
 205         TypesZ :: Types cs '[]
 206         TypesS :: Type  cs h
 207                -> Types cs hs
 208                -> Types cs (Proxy h ': hs)
 209 infixr 5 `TypesS`
 210
 211 etypes :: Types cs hs -> [EType cs]
 212 etypes TypesZ = []
 213 etypes (TypesS t ts) = EType t : etypes ts
 214
 215 -- | Build the left spine of a 'Type'.
 216 spine_of_type
 217  :: Type cs h
 218  -> (forall kc (c::kc) hs. Const cs c -> Types cs hs -> ret) -> ret
 219 spine_of_type (TyConst c) k = k c TypesZ
 220 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `TypesS` as)
 221
 222 -- * Type 'UnProxy'
 223 type family UnProxy (x::K.Type) :: k where
 224         UnProxy (Proxy x) = x
 225
 226 -- * Class 'MonoLift'
 227 class MonoLift a b where
 228         olift :: a -> b
 229 instance MonoLift
 230  (Error_Type meta ts)
 231  (Error_Type meta ts) where
 232         olift = id
 233 instance
 234  MonoLift (Constraint_Kind meta ts) (Error_Type meta ts) where
 235         olift = olift . Error_Type_Constraint_Kind