Language/LOL/Symantic/Type/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE KindSignatures #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE Rank2Types #-}
  10 {-# LANGUAGE ScopedTypeVariables #-}
  11 {-# LANGUAGE TypeFamilies #-}
  12 {-# LANGUAGE TypeOperators #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 module Language.LOL.Symantic.Type.Common where
  15
  16 import Data.Maybe (isJust)
  17 import Data.Peano
  18 import Data.Proxy
  19 import Data.Type.Equality ((:~:))
  20
  21 -- * Class 'Type_Eq'
  22
  23 -- | Test two types for equality,
  24 -- returning an Haskell type-level proof
  25 -- of the equality when it holds.
  26 class Type_Eq ty where
  27         type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  28
  29 -- * Class 'Type_from'
  30 -- | Parse some @raw@ data into a 'Root_of_Type',
  31 -- or return 'Nothing' if the @raw@ value is not supported
  32 -- or an 'Error_Type' if it is not well-formed.
  33 class Type_Eq ty =>
  34       Type_from raw (ty:: * -> *) where
  35         type_from
  36          :: Proxy ty
  37          -> raw
  38          -> (forall h. Root_of_Type ty h
  39                     -> Either (Maybe (Error_of_Type raw (Root_of_Type ty))) ret)
  40          ->            Either (Maybe (Error_of_Type raw (Root_of_Type ty))) ret
  41
  42 -- ** Type family 'Root_of_Type'
  43 -- | Return the root type of a type.
  44 type family Root_of_Type (ty:: * -> *) :: * -> *
  45
  46 -- ** Type family 'Error_of_Type'
  47 -- | Return the error type of a type.
  48 type family Error_of_Type (raw:: *) (ty:: * -> *) :: *
  49
  50 -- * Type 'Type_Root'
  51 -- | The root type, passing itself as parameter to the given type @ty@.
  52 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  53  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  54 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  55 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
  56 type instance Error_of_Type raw (Type_Root ty)
  57  =            Error_of_Type raw (ty (Type_Root ty))
  58  -- NOTE: require UndecidableInstances.
  59 instance -- Type_Eq
  60  Type_Eq (ty (Type_Root ty)) =>
  61  Type_Eq (Type_Root ty) where
  62         type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
  63 instance -- Eq
  64  Type_Eq (Type_Root ty) =>
  65  Eq (Type_Root ty h) where
  66         x == y = isJust $ type_eq x y
  67 instance -- Type_from
  68  ( Type_Eq (Type_Root ty)
  69  , Type_from raw (ty (Type_Root ty))
  70  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  71  ) => Type_from raw (Type_Root ty) where
  72         type_from _px_ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
  73 instance -- String_from_Type
  74  String_from_Type (ty (Type_Root ty)) =>
  75  String_from_Type (Type_Root ty) where
  76         string_from_type (Type_Root ty) = string_from_type ty
  77 instance -- Show
  78  String_from_Type (Type_Root ty) =>
  79  Show (Type_Root ty h) where
  80         show = string_from_type
  81
  82 -- ** Class 'Type_Root_Lift'
  83 -- | Lift a given type to a given root type.
  84 class Type_Root_Lift ty root where
  85         type_root_lift :: forall h. ty root h -> root h
  86 instance
  87  Type_Cons_Lift ty root =>
  88  Type_Root_Lift ty (Type_Root root) where
  89         type_root_lift = Type_Root . type_cons_lift
  90
  91 -- * Type 'Type_Cons'
  92 -- | Combine two types into one.
  93 data Type_Cons curr next (root:: * -> *) h
  94  =   Type_Curr (curr root h)
  95  |   Type_Next (next root h)
  96 type instance Root_of_Type (Type_Cons curr next root) = root
  97 type instance Error_of_Type raw (Type_Cons curr next root)
  98  = Error_Type_Cons (Error_of_Type raw (curr root))
  99                    (Error_of_Type raw (next root))
 100 instance -- Type_Eq
 101  ( Type_Eq (curr root)
 102  , Type_Eq (next root)
 103  ) => Type_Eq (Type_Cons curr next root) where
 104         type_eq (Type_Curr x) (Type_Curr y) = x `type_eq` y
 105         type_eq (Type_Next x) (Type_Next y) = x `type_eq` y
 106         type_eq _ _ = Nothing
 107 instance -- Eq
 108  ( Type_Eq (curr root)
 109  , Type_Eq (next root)
 110  ) => Eq (Type_Cons curr next root h) where
 111         x == y = isJust $ type_eq x y
 112 instance -- Type_from
 113  ( Type_Eq (curr root)
 114  , Type_from raw (curr root)
 115  , Type_from raw (next root)
 116  , Root_of_Type (curr root) ~ root
 117  , Root_of_Type (next root) ~ root
 118  ) => Type_from raw (Type_Cons curr next root) where
 119         type_from _px_ty raw k =
 120                 case type_from (Proxy::Proxy (curr root)) raw (Right . k) of
 121                  Right ret -> ret
 122                  Left Nothing -> type_from (Proxy::Proxy (next root)) raw k
 123                  Left err -> Left err
 124 instance -- String_from_Type
 125  ( String_from_Type (curr root)
 126  , String_from_Type (next root)
 127  ) => String_from_Type (Type_Cons curr next root) where
 128         string_from_type (Type_Curr t) = string_from_type t
 129         string_from_type (Type_Next t) = string_from_type t
 130
 131 -- ** Type 'Type_Cons_Lift'
 132 -- | Apply 'Peano_of_Type' on 'Type_Cons_LiftN'.
 133 type Type_Cons_Lift ty tys
 134  =   Type_Cons_LiftN (Peano_of_Type ty tys) ty tys
 135 -- | Return a 'Peano' number derived from the location
 136 -- of a given type within a given type stack.
 137
 138 -- *** Class 'Type_Cons_LiftN'
 139 -- | Construct the sequence of 'Type_Curr' and 'Type_Next'
 140 -- lifting a given type to the top of a given type stack.
 141 class Type_Cons_LiftN (n::Peano) ty tys where
 142         type_cons_liftN :: forall (root:: * -> *) h. Proxy n -> ty root h -> tys root h
 143 instance Type_Cons_LiftN 'Zero curr curr where
 144         type_cons_liftN _ = id
 145 instance Type_Cons_LiftN 'Zero curr (Type_Cons curr next) where
 146         type_cons_liftN _ = Type_Curr
 147 instance
 148  Type_Cons_LiftN n other next =>
 149  Type_Cons_LiftN ('Succ n) other (Type_Cons curr next) where
 150         type_cons_liftN _ = Type_Next . type_cons_liftN (Proxy::Proxy n)
 151
 152 -- | Lift a type within a type stack to its top,
 153 -- using a 'Peano' number calculated by 'Peano_of_Type'
 154 -- to avoid the overlapping of the 'Type_Cons_LiftN' instances.
 155 type_cons_lift
 156  :: forall ty tys (root:: * -> *) h.
 157  Type_Cons_Lift ty tys =>
 158  ty root h -> tys root h
 159 type_cons_lift = type_cons_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 160
 161 type family Peano_of_Type
 162  (ty::  (* -> *) -> * -> *)
 163  (tys:: (* -> *) -> * -> *) :: Peano where
 164         Peano_of_Type ty ty                       = 'Zero
 165         Peano_of_Type ty (Type_Cons ty next)      = 'Zero
 166         Peano_of_Type other (Type_Cons curr next) = 'Succ (Peano_of_Type other next)
 167
 168 -- ** Type 'Type_Cons_Unlift'
 169 -- | Apply 'Peano_of_Type' on 'Type_Cons_UnliftN'.
 170 type Type_Cons_Unlift ty tys
 171  =   Type_Cons_UnliftN (Peano_of_Type ty tys) ty tys
 172
 173 -- *** Class 'Type_Cons_UnliftN'
 174 -- | Deconstruct a sequence of 'Type_Curr' and 'Type_Next'
 175 -- trying to unlift a given extension out of a given extension stack.
 176 class Type_Cons_UnliftN (n::Peano) ty tys where
 177         type_cons_unliftN :: forall (root:: * -> *) h. Proxy n -> tys root h -> Maybe (ty root h)
 178 instance Type_Cons_UnliftN 'Zero curr curr where
 179         type_cons_unliftN _ = Just
 180 instance Type_Cons_UnliftN 'Zero curr (Type_Cons curr next) where
 181         type_cons_unliftN _ (Type_Curr x) = Just x
 182         type_cons_unliftN _ (Type_Next _) = Nothing
 183 instance
 184  Type_Cons_UnliftN n other next =>
 185  Type_Cons_UnliftN ('Succ n) other (Type_Cons curr next) where
 186         type_cons_unliftN _ (Type_Next x) = type_cons_unliftN (Proxy::Proxy n) x
 187         type_cons_unliftN _ (Type_Curr _) = Nothing
 188
 189 -- | Unlift an extension within an extension stack,
 190 -- using a 'Peano' number calculated by 'Peano_of_Type'
 191 -- to avoid the overlapping of the 'Type_Cons_UnliftN' instances.
 192 type_cons_unlift
 193  :: forall ty tys (root:: * -> *) h.
 194  Type_Cons_Unlift ty tys =>
 195  tys root h -> Maybe (ty root h)
 196 type_cons_unlift = type_cons_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 197
 198 -- * Type 'Error_Type_Cons'
 199 -- | Combine two error types into one.
 200 data Error_Type_Cons curr next
 201  =   Error_Type_Curr curr
 202  |   Error_Type_Next next
 203  deriving (Eq, Show)
 204
 205 -- ** Class 'Error_Type_LiftN'
 206 -- | Construct the sequence of 'Error_Type_Curr' and 'Error_Type_Next'
 207 -- lifting a given error type to the top of a given error type stack.
 208 class Error_Type_LiftN (n::Peano) err errs where
 209         error_type_liftN :: Proxy n -> err -> errs
 210 instance Error_Type_LiftN 'Zero curr curr where
 211         error_type_liftN _ = id
 212 instance Error_Type_LiftN 'Zero curr (Error_Type_Cons curr next) where
 213         error_type_liftN _ = Error_Type_Curr
 214 instance
 215  Error_Type_LiftN n other next =>
 216  Error_Type_LiftN ('Succ n) other (Error_Type_Cons curr next) where
 217         error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)
 218
 219 -- | Lift an error type within a type stack to its top,
 220 -- using a 'Peano' number calculated by 'Peano_of_Error_Type'
 221 -- to avoid the overlapping of the 'Error_Type_LiftN' instances.
 222 error_type_lift
 223  :: forall err errs.
 224  Error_Type_Lift err errs =>
 225  err -> errs
 226 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 227
 228 type Error_Type_Lift err errs
 229  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 230 -- | Return a 'Peano' number derived from the location
 231 -- of a given error type within a given error type stack.
 232 type family Peano_of_Error_Type (err:: *) (errs:: *) :: Peano where
 233         Peano_of_Error_Type err err                           = 'Zero
 234         Peano_of_Error_Type err (Error_Type_Cons err next)    = 'Zero
 235         Peano_of_Error_Type other (Error_Type_Cons curr next) = 'Succ (Peano_of_Error_Type other next)
 236
 237 -- * Class 'String_from_Type'
 238 -- | Return a 'String' from a type.
 239 class String_from_Type ty where
 240         string_from_type :: ty h -> String
 241
 242 -- * Type 'Context'
 243
 244 -- | GADT for a typing context,
 245 -- accumulating an @item@ at each lambda;
 246 -- used to accumulate object-types of lambda variables in 'Sym_from'
 247 -- or host-terms of lambda variables in 'Repr_Host'.
 248 data Context :: (* -> *) -> [*] -> * where
 249         Context_Empty :: Context item '[]
 250         Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
 251 infixr 5 `Context_Next`
 252
 253 -- * Type 'Exists_Type'
 254
 255 -- | Existential data type to wrap an indexed type.
 256 data Exists_Type ty
 257  = forall h. Exists_Type (ty h)
 258 instance -- Eq
 259  Type_Eq ty =>
 260  Eq (Exists_Type ty) where
 261         Exists_Type xh == Exists_Type yh =
 262                 isJust $ type_eq xh yh
 263 instance -- Show
 264  String_from_Type ty =>
 265  Show (Exists_Type ty) where
 266         show (Exists_Type ty) = string_from_type ty
 267
 268 -- * Type 'Exists_Type_and_Repr'
 269 data Exists_Type_and_Repr ty repr
 270  =   forall h.
 271      Exists_Type_and_Repr (ty h) (repr h)