Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE PolyKinds #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE StandaloneDeriving #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Typing.Type where
  14
  15 import Data.Maybe (fromMaybe, isJust)
  16 import Data.Proxy
  17 import Data.Type.Equality
  18 import qualified Data.Kind as K
  19
  20 import Language.Symantic.Typing.Kind
  21 import Language.Symantic.Typing.Constant
  22 import Language.Symantic.Typing.Syntax
  23
  24 -- * Type 'Type'
  25
  26 -- | /Type of terms/.
  27 --
  28 -- * @cs@: /type constants/.
  29 -- * @ki@: 'Kind' (/type of the type/).
  30 -- * @h@: indexed Haskell type.
  31 --
  32 -- * 'TyConst': /type constant/.
  33 -- * @(:$)@: /type application/.
  34 --
  35 -- NOTE: when used, @h@ is a 'Proxy',
  36 -- because @GADTs@ constructors cannot alter kinds.
  37 -- Neither is it possible to assert that @(@'UnProxy'@ f :: ka -> kb)@,
  38 -- and therefore @(@'UnProxy'@ f (@'UnProxy'@ x))@ cannot kind check;
  39 -- however a type application of @f@ is needed,
  40 -- so this is worked around with the introduction of the 'App' type family,
  41 -- which handles the type application when @(@'UnProxy'@ f :: ka -> kb)@
  42 -- is true from elsewhere, or stay abstract otherwise.
  43 -- However, since type synonym family cannot be used within the pattern
  44 -- of another type family, the kind of an abstract
  45 -- @(@'App'@ f x)@ cannot be derived from @f@,
  46 -- so this is worked around with the introduction of the @ki@ parameter.
  47 data Type (cs::[K.Type]) (ki::Kind) (h:: K.Type) where
  48         TyConst
  49          :: Const cs c
  50          -> Type cs (Kind_of_UnProxy c) c
  51         (:$)
  52          :: Type cs (ki_x ':> ki) f
  53          -> Type cs ki_x x
  54          -> Type cs ki (App f x)
  55         {-
  56         TyVar
  57          :: SKind ki
  58          -> SPeano v
  59          -> Type cs ki v
  60         -}
  61 infixl 5 :$
  62
  63 -- ** Type family 'App'
  64 -- | Lift the Haskell /type application/ within a 'Proxy'.
  65 type family App (f:: K.Type) (a:: K.Type) :: K.Type
  66 type instance App (Proxy (f:: ki_a -> ki_fa)) a = Proxy (f (UnProxy a))
  67
  68 -- ** Type 'Type_of'
  69 -- | Convenient wrapper when @t@ is statically known.
  70 type Type_of cs t = Type cs (Kind_of t) (Proxy t)
  71
  72 kind_of :: Type cs ki h -> SKind ki
  73 kind_of ty =
  74         case ty of
  75          TyConst c -> kind_of_const c
  76          f :$ _x -> case kind_of f of _ `SKiArrow` ki -> ki
  77
  78 eq_type
  79  :: Type cs ki_x x -> Type cs ki_y y
  80  -> Maybe (x :~: y)
  81 eq_type (TyConst x) (TyConst y)
  82  | Just Refl <- testEquality x y
  83  = Just Refl
  84 eq_type (xf :$ xx) (yf :$ yx)
  85  | Just Refl <- eq_type xf yf
  86  , Just Refl <- eq_type xx yx
  87  = Just Refl
  88 eq_type _ _ = Nothing
  89
  90 instance TestEquality (Type cs ki) where
  91         testEquality = eq_type
  92 instance Eq (Type cs ki h) where
  93         _x == _y = True
  94 instance Show_Const cs => Show (Type cs ki h) where
  95         show = show_type
  96
  97 -- * Type 'EType'
  98 -- | Existential for 'Type'.
  99 data EType cs = forall ki h. EType (Type cs ki h)
 100
 101 instance Eq (EType cs) where
 102         EType x == EType y = isJust $ eq_type x y
 103 instance Show_Const cs => Show (EType cs) where
 104         show (EType ty) = show_type ty
 105
 106 show_type :: Show_Const cs => Type cs ki_h h -> String
 107 show_type (TyConst c) = show c
 108 show_type ((:$) f@(:$){} a@(:$){}) = "(" ++ show_type f ++ ") (" ++ show_type a ++ ")"
 109 show_type ((:$) f@(:$){} a) = "(" ++ show_type f ++ ") " ++ show_type a
 110 show_type ((:$) f a@(:$){}) = show_type f ++ " (" ++ show_type a ++ ")"
 111 show_type ((:$) f a) = show_type f ++ " " ++ show_type a
 112 -- show_type (TyVar v) = "t" ++ show (integral_from_peano v::Integer)
 113
 114 -- * Type 'KType'
 115 -- | Existential for 'Type' of a known 'Kind'.
 116 data KType cs ki = forall h. KType (Type cs ki h)
 117
 118 instance Eq (KType cs ki) where
 119         KType x == KType y = isJust $ eq_type x y
 120 instance Show_Const cs => Show (KType cs ki) where
 121         show (KType ty) = show_type ty
 122
 123 -- * Class 'Type_from'
 124 -- | Try to build a 'Type' from raw data.
 125 class Type_from ast cs where
 126         type_from
 127          :: ast
 128          -> (forall ki_h h. Type cs ki_h h -> Either (Error_Type cs ast) ret)
 129          -> Either (Error_Type cs ast) ret
 130
 131 instance
 132  ( Const_from (Lexem ast) cs
 133  , AST ast
 134  ) => Type_from ast cs where
 135         type_from ast kk =
 136                 fromMaybe (Left $ Error_Type_Constant_unknown $ At (Just ast) $ ast_lexem ast) $
 137                 const_from (ast_lexem ast) $ \c -> Just $
 138                 go (ast_nodes ast) (TyConst c) kk
 139                 where
 140                 go :: forall ki h ret. [ast]
 141                  -> Type cs ki h
 142                  -> (forall ki' h'. Type cs ki' h' -> Either (Error_Type cs ast) ret)
 143                  -> Either (Error_Type cs ast) ret
 144                 go [] ty k = k ty
 145                 go (ast_x:ast_xs) ty_f k =
 146                         type_from ast_x $ \ty_x ->
 147                         case kind_of ty_f of
 148                          ki_f_a `SKiArrow` _ki_f_b ->
 149                                 let ki_x = kind_of ty_x in
 150                                 case testEquality ki_f_a ki_x of
 151                                  Just Refl -> go ast_xs (ty_f :$ ty_x) k
 152                                  Nothing -> Left $ Error_Type_Kind_mismatch
 153                                          (At (Just ast)   $ EKind ki_f_a)
 154                                          (At (Just ast_x) $ EKind ki_x)
 155                          ki -> Left $ Error_Type_Kind_not_applicable $ At (Just ast) $ EKind ki
 156
 157 -- ** Type 'Error_Type'
 158 data Error_Type cs ast
 159  =   Error_Type_Constant_unknown    (At ast (Lexem ast))
 160  |   Error_Type_Kind_mismatch       (At ast EKind) (At ast EKind)
 161  |   Error_Type_Kind_not_applicable (At ast EKind)
 162 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
 163 deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)
 164
 165 -- * Type 'Args'
 166 data Args (cs::[K.Type]) (args::[K.Type]) where
 167         ArgZ :: Args cs '[]
 168         ArgS :: Type cs ki arg
 169              -> Args cs args
 170              -> Args cs (arg ': args)
 171 infixr 5 `ArgS`
 172
 173 -- | Build the left spine of a 'Type'.
 174 spine_of_type
 175  :: Type cs ki_h h
 176  -> (forall c as. Const cs c -> Args cs as -> ret) -> ret
 177 spine_of_type (TyConst c) k = k c ArgZ
 178 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
 179
 180 -- * Usual 'Type's
 181
 182 -- | The 'Bool' 'Type'
 183 tyBool :: Inj_Const cs Bool => Type_of cs Bool
 184 tyBool = TyConst inj_const
 185
 186 -- | The 'Eq' 'Type'
 187 tyEq :: Inj_Const cs Eq => Type_of cs Eq
 188 tyEq = TyConst inj_const
 189
 190 -- | The 'Functor' 'Type'
 191 tyFunctor :: Inj_Const cs Functor => Type_of cs Functor
 192 tyFunctor = TyConst inj_const
 193
 194 -- | The 'Int' 'Type'
 195 tyInt :: Inj_Const cs Int => Type_of cs Int
 196 tyInt = TyConst inj_const
 197
 198 -- | The 'IO'@ a@ 'Type'
 199 tyIO :: Inj_Const cs IO => Type_of cs IO
 200 tyIO = TyConst inj_const
 201
 202 -- | The 'Ord' 'Type'
 203 tyOrd :: Inj_Const cs Ord => Type_of cs Ord
 204 tyOrd = TyConst inj_const
 205
 206 -- | The 'Ordering' 'Type'
 207 tyOrdering :: Inj_Const cs Ordering => Type_of cs Ordering
 208 tyOrdering = TyConst inj_const
 209
 210 -- | The 'Traversable'@ a@ 'Type'
 211 tyTraversable :: Inj_Const cs Traversable => Type_of cs Traversable
 212 tyTraversable = TyConst inj_const
 213
 214 -- | The 'Monad'@ a@ 'Type'
 215 tyMonad :: Inj_Const cs Monad => Type_of cs Monad
 216 tyMonad = TyConst inj_const
 217
 218 -- | The 'Int' 'Type'
 219 tyFun :: Inj_Const cs (->) => Type_of cs (->)
 220 tyFun = TyConst inj_const
 221
 222 -- | The function 'Type' @((->) a b)@
 223 -- with an infix notation more readable.
 224 (~>) :: forall cs a b. Inj_Const cs (->)
 225  => Type cs 'KiTerm a
 226  -> Type cs 'KiTerm b
 227  -> Type_of cs (UnProxy a -> UnProxy b)
 228 (~>) a b = TyConst (inj_const::Const cs (Proxy (->))) :$ a :$ b
 229 infixr 5 ~>