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
  15 import Language.Symantic.Typing.Kind
  16 import Language.Symantic.Typing.Constant
  17
  18 -- * Type 'Type'
  19
  20 -- | /Type of terms/.
  21 --
  22 -- * @cs@: /type constants/.
  23 -- * @ki@: 'Kind' (/type of the type/).
  24 -- * @h@: indexed Haskell type.
  25 --
  26 -- * 'TyConst': /type constant/.
  27 -- * @(:$)@: /type application/.
  28 --
  29 -- NOTE: when used, @h@ is a 'Proxy',
  30 -- because @GADTs@ constructors cannot alter kinds.
  31 -- Neither is it possible to assert that @(@'UnProxy'@ f :: * -> *)@,
  32 -- and therefore @(@'UnProxy'@ f (@'UnProxy'@ x))@ cannot kind check;
  33 -- however a type application of @f@ is needed,
  34 -- so this is worked around with the introduction of the 'App' type family,
  35 -- which handles the type application when @(@'UnProxy'@ f :: * -> *)@
  36 -- is true from elsewhere, or stay abstract otherwise.
  37 -- However, since type synonym family cannot be used within the pattern
  38 -- of another type family, the kind of an abstract
  39 -- @(@'App'@ f x)@ cannot be derived from @f@,
  40 -- so this is worked around with the introduction of the @ki@ parameter.
  41 data Type (cs::[*]) (ki::Kind) (h:: *) where
  42         TyConst
  43          :: Const cs c
  44          -> Type cs (Kind_of_UnProxy c) c
  45         (:$)
  46          :: Type cs (ki_x ':> ki) f
  47          -> Type cs ki_x x
  48          -> Type cs ki (App f x)
  49         {-
  50         TyVar
  51          :: SKind ki
  52          -> SPeano v
  53          -> Type cs ki v
  54         -}
  55 infixl 5 :$
  56
  57 -- * Type family 'UnProxy'
  58 -- | Useful to have the 'App' type family working on all @a@,
  59 -- or to capture a 'Constraint' in a 'Dict'.
  60 type family UnProxy px :: k where
  61         UnProxy (Proxy h) = h
  62
  63 -- ** Type family 'App'
  64 -- | Lift the Haskell /type application/ within a 'Proxy'.
  65 type family App (f:: *) (a:: *) :: *
  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
  93 -- * Type 'EType'
  94 -- | Existential for 'Type'.
  95 data EType cs = forall ki h. EType (Type cs ki h)
  96
  97 instance Eq (EType cs) where
  98         EType x == EType y = isJust $ eq_type x y
  99 instance Show_Const cs => Show (EType cs) where
 100         show (EType ty) = show_type ty
 101
 102 show_type :: Show_Const cs => Type cs ki_h h -> String
 103 show_type (TyConst c) = show c
 104 show_type ((:$) f@(:$){} a@(:$){}) = "(" ++ show_type f ++ ") (" ++ show_type a ++ ")"
 105 show_type ((:$) f@(:$){} a) = "(" ++ show_type f ++ ") " ++ show_type a
 106 show_type ((:$) f a@(:$){}) = show_type f ++ " (" ++ show_type a ++ ")"
 107 show_type ((:$) f a) = show_type f ++ " " ++ show_type a
 108 -- show_type (TyVar v) = "t" ++ show (integral_from_peano v::Integer)
 109
 110 -- * Type 'Args'
 111 data Args (cs::[*]) (args::[*]) where
 112         ArgZ :: Args cs '[]
 113         ArgS :: Type cs ki arg
 114              -> Args cs args
 115              -> Args cs (arg ': args)
 116 infixr 5 `ArgS`
 117
 118 -- | Build the left spine of a 'Type'.
 119 spine_of_type
 120  :: Type cs ki_h h
 121  -> (forall c as. Const cs c -> Args cs as -> ret) -> ret
 122 spine_of_type (TyConst c) k = k c ArgZ
 123 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
 124
 125 -- * Usual 'Type's
 126
 127 -- | The 'Bool' 'Type'
 128 tyBool :: Inj_Const cs Bool => Type_of cs Bool
 129 tyBool = TyConst inj_const
 130
 131 -- | The 'Eq' 'Type'
 132 tyEq :: Inj_Const cs Eq => Type_of cs Eq
 133 tyEq = TyConst inj_const
 134
 135 -- | The 'Int' 'Type'
 136 tyInt :: Inj_Const cs Int => Type_of cs Int
 137 tyInt = TyConst inj_const
 138
 139 -- | The 'IO'@ a@ 'Type'
 140 tyIO :: Inj_Const cs IO => Type_of cs IO
 141 tyIO = TyConst inj_const
 142
 143 -- | The 'Traversable'@ a@ 'Type'
 144 tyTraversable :: Inj_Const cs Traversable => Type_of cs Traversable
 145 tyTraversable = TyConst inj_const
 146
 147 -- | The 'Monad'@ a@ 'Type'
 148 tyMonad :: Inj_Const cs Monad => Type_of cs Monad
 149 tyMonad = TyConst inj_const
 150
 151 -- | The 'Int' 'Type'
 152 tyFun :: Inj_Const cs (->) => Type_of cs (->)
 153 tyFun = TyConst inj_const
 154
 155 -- | The function 'Type' @((->) a b)@
 156 -- with an infix notation more readable.
 157 (~>) :: forall cs a b. Inj_Const cs (->)
 158  => Type cs 'KiTerm (Proxy a)
 159  -> Type cs 'KiTerm (Proxy b)
 160  -> Type_of cs (a -> b)
 161 (~>) a b = TyConst (inj_const::Const cs (Proxy (->))) :$ a :$ b
 162 infixr 5 ~>