Language/LOL/Symantic/Type/Common.hs

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