Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE Rank2Types #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE TypeOperators #-}
   9 module Language.Symantic.Typing.Type where
  10
  11 import Data.Maybe (isJust)
  12 import Data.Proxy
  13 import Data.Type.Equality
  14 import GHC.Prim (Constraint)
  15
  16 import Language.Symantic.Typing.Kind
  17 import Language.Symantic.Typing.Constant
  18
  19 -- * Type 'Type'
  20
  21 -- | /Type of terms/.
  22 --
  23 -- * @cs@: /type constants/.
  24 -- * @ki@: 'Kind' (/type of the type/).
  25 -- * @h@: Haskell type projected onto.
  26 --
  27 -- * 'TyConst': /type constant/
  28 -- * '(:$)': /type application/
  29 -- * '(:~)': /type constraint constructor/
  30 --
  31 -- NOTE: when used, @h@ is a 'Proxy',
  32 -- because @GADTs@ constructors cannot alter kinds.
  33 -- Neither is it possible to assert that @(@'UnProxy'@ f :: * -> *)@,
  34 -- and therefore @(@'UnProxy'@ f (@'UnProxy'@ x))@ cannot kind check;
  35 -- however a type application of @f@ is needed in 'App' and 'Con',
  36 -- so this is worked around with the introduction of the 'App' type family,
  37 -- which handles the type application when @(@'UnProxy'@ f :: * -> *)@
  38 -- is true from elsewhere, or stay abstract otherwise.
  39 -- However, since type synonym family cannot be used within the pattern
  40 -- of another type family, the kind of an abstract
  41 -- @(@'App'@ f x)@ cannot be derived from @f@,
  42 -- so this is worked around with the introduction of the @ki@ parameter.
  43 data Type (cs::[*]) (ki::Kind) (h:: *) where
  44         TyConst
  45          :: Const cs c
  46          -> Type cs (Kind_of_Proxy c) c
  47         (:$)
  48          :: Type cs (ki_x ':> ki) f
  49          -> Type cs ki_x x
  50          -> Type cs ki (App f x)
  51         (:~)
  52          :: Con q x
  53          => Type cs (ki_x ':> 'KiCon) q
  54          -> Type cs ki_x x
  55          -> Type cs 'KiCon (App q x)
  56         {-
  57         TyVar
  58          :: SKind ki
  59          -> SPeano v
  60          -> Type cs ki v
  61         -}
  62 infixl 5 :$
  63 infixl 5 :~
  64
  65 -- ** Type family 'UnProxy'
  66 -- | Useful to have 'App' and 'Con' type families working on all @a@.
  67 type family UnProxy px :: k where
  68         UnProxy (Proxy h) = h
  69
  70 -- ** Type family 'App'
  71 -- | Lift the Haskell /type application/ within a 'Proxy'.
  72 type family App (f:: *) (a:: *) :: *
  73 type instance App (Proxy (f:: ki_a -> ki_fa)) a = Proxy (f (UnProxy a))
  74
  75 -- ** Type family 'Con'
  76 -- | Lift the Haskell /type constraint/ within a 'Proxy'.
  77 type family Con (q:: *) (a:: *) :: Constraint
  78 type instance Con (Proxy (q:: ki_a -> Constraint)) a = q (UnProxy a)
  79
  80 -- ** Type 'Type_of'
  81 -- | Convenient wrapper when @t@ is statically known.
  82 type Type_of cs t = Type cs (Kind_of t) (Proxy t)
  83
  84 kind_of :: Type cs ki h -> SKind ki
  85 kind_of ty =
  86         case ty of
  87          TyConst c -> kind_of_const c
  88          f :$ _x -> case kind_of f of _ `SKiArrow` ki -> ki
  89          q :~ _x -> case kind_of q of _ `SKiArrow` ki -> ki
  90
  91 eq_type
  92  :: Type cs ki_x x -> Type cs ki_y y
  93  -> Maybe (x :~: y)
  94 eq_type (TyConst x) (TyConst y)
  95  | Just Refl <- testEquality x y
  96  = Just Refl
  97 eq_type (xf :$ xx) (yf :$ yx)
  98  | Just Refl <- eq_type xf yf
  99  , Just Refl <- eq_type xx yx
 100  = Just Refl
 101 eq_type (xq :~ xx) (yq :~ yx)
 102  | Just Refl <- eq_type xq yq
 103  , Just Refl <- eq_type xx yx
 104  = Just Refl
 105 eq_type _ _ = Nothing
 106
 107 instance TestEquality (Type cs ki) where
 108         testEquality = eq_type
 109
 110 -- * Type 'EType'
 111 -- | Existential for 'Type'.
 112 data EType cs = forall ki h. EType (Type cs ki h)
 113
 114 instance Eq (EType cs) where
 115         EType x == EType y = isJust $ eq_type x y
 116 instance Show_Const cs => Show (EType cs) where
 117         show (EType ty) = show_type ty
 118
 119 show_type :: Show_Const cs => Type cs ki_h h -> String
 120 show_type (TyConst c) = show c
 121 show_type ((:$) f@(:$){} a@(:$){}) = "(" ++ show_type f ++ ") (" ++ show_type a ++ ")"
 122 show_type ((:$) f@(:$){} a) = "(" ++ show_type f ++ ") " ++ show_type a
 123 show_type ((:$) f a@(:$){}) = show_type f ++ " (" ++ show_type a ++ ")"
 124 show_type ((:$) f a) = show_type f ++ " " ++ show_type a
 125 show_type ((:~) q a) = show_type q ++ " " ++ show_type a
 126 -- show_type (TyVar v) = "t" ++ show (integral_from_peano v::Integer)
 127
 128 -- * Type 'Args'
 129 data Args (cs::[*]) (args::[*]) where
 130         ArgZ :: Args cs '[]
 131         ArgS :: Type cs ki arg
 132              -> Args cs args
 133              -> Args cs (arg ': args)
 134 infixr 5 `ArgS`
 135
 136 -- | Build the left spine of a 'Type'.
 137 spine_of_type
 138  :: Type cs ki_h h
 139  -> (forall c as. Const cs c
 140                -> Args cs as -> ret) -> ret
 141 spine_of_type (TyConst c)   k = k c ArgZ
 142 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
 143 spine_of_type (q :~ a) k = spine_of_type q $ \c as -> k c (a `ArgS` as)
 144
 145 -- * Usual 'Type's
 146
 147 -- | The 'Bool' 'Type'
 148 tyBool :: Inj_Const cs Bool => Type_of cs Bool
 149 tyBool = TyConst inj_const
 150
 151 -- | The 'Eq' 'Type'
 152 tyEq :: Inj_Const cs Eq => Type_of cs Eq
 153 tyEq = TyConst inj_const
 154
 155 -- | The 'Int' 'Type'
 156 tyInt :: Inj_Const cs Int => Type_of cs Int
 157 tyInt = TyConst inj_const
 158
 159 -- | The 'IO'@ a@ 'Type'
 160 tyIO :: Inj_Const cs IO => Type_of cs IO
 161 tyIO = TyConst inj_const
 162
 163 -- | The 'Traversable'@ a@ 'Type'
 164 tyTraversable :: Inj_Const cs Traversable => Type_of cs Traversable
 165 tyTraversable = TyConst inj_const
 166
 167 -- | The 'Monad'@ a@ 'Type'
 168 tyMonad :: Inj_Const cs Monad => Type_of cs Monad
 169 tyMonad = TyConst inj_const
 170
 171 -- | The 'Int' 'Type'
 172 tyFun :: Inj_Const cs (->) => Type_of cs (->)
 173 tyFun = TyConst inj_const
 174
 175 -- | The function 'Type' @(\->) a b@
 176 -- with an infix notation more readable.
 177 (~>) :: forall cs a b. Inj_Const cs (->)
 178  => Type cs 'KiTerm (Proxy a)
 179  -> Type cs 'KiTerm (Proxy b)
 180  -> Type_of cs (a -> b)
 181 (~>) a b = TyConst (inj_const::Const cs (Proxy (->))) :$ a :$ b
 182 infixr 5 ~>