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 -- | Lift a given type to the top of a given type stack including it,
 147 -- by constructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 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 -- | Convenient wrapper around 'type_liftN',
 160 -- passing it the 'Peano' number from 'Peano_of_Type'.
 161 type_lift
 162  :: forall ty tys (root:: * -> *) h.
 163  Type_Lift ty tys =>
 164  ty root h -> tys root h
 165 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 166
 167 -- ** Type 'Type_Unlift'
 168 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 169 type Type_Unlift ty tys
 170  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 171
 172 -- *** Class 'Type_UnliftN'
 173 -- | Try to unlift a given type out of a given type stack including it,
 174 -- by deconstructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 175 class Type_UnliftN (n::Peano) ty tys where
 176         type_unliftN :: forall (root:: * -> *) h. Proxy n -> tys root h -> Maybe (ty root h)
 177 instance Type_UnliftN 'Zero curr curr where
 178         type_unliftN _ = Just
 179 instance Type_UnliftN 'Zero curr (Type_Cons curr next) where
 180         type_unliftN _ (Type_Curr x) = Just x
 181         type_unliftN _ (Type_Next _) = Nothing
 182 instance
 183  Type_UnliftN n other next =>
 184  Type_UnliftN ('Succ n) other (Type_Cons curr next) where
 185         type_unliftN _ (Type_Next x) = type_unliftN (Proxy::Proxy n) x
 186         type_unliftN _ (Type_Curr _) = Nothing
 187
 188 -- | Convenient wrapper around 'type_unliftN',
 189 -- passing it the 'Peano' number from 'Peano_of_Type'.
 190 type_unlift
 191  :: forall ty tys (root:: * -> *) h.
 192  Type_Unlift ty tys =>
 193  tys root h -> Maybe (ty root h)
 194 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 195
 196 -- * Type 'Error_Type_Cons'
 197 -- | Combine two error types into one.
 198 data Error_Type_Cons curr next
 199  =   Error_Type_Curr curr
 200  |   Error_Type_Next next
 201  deriving (Eq, Show)
 202
 203 -- ** Type 'Error_Type_Lift'
 204 type Error_Type_Lift err errs
 205  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 206
 207 -- *** Type 'Peano_of_Error_Type'
 208 -- | Return a 'Peano' number derived from the location
 209 -- of a given error type within a given error type stack.
 210 type family Peano_of_Error_Type (err:: *) (errs:: *) :: Peano where
 211         Peano_of_Error_Type err err                           = 'Zero
 212         Peano_of_Error_Type err (Error_Type_Cons err next)    = 'Zero
 213         Peano_of_Error_Type other (Error_Type_Cons curr next) = 'Succ (Peano_of_Error_Type other next)
 214
 215 -- *** Class 'Error_Type_LiftN'
 216 -- | Lift a given error type to the top of a given error type stack including it,
 217 -- by constructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
 218 class Error_Type_LiftN (n::Peano) err errs where
 219         error_type_liftN :: Proxy n -> err -> errs
 220 instance Error_Type_LiftN 'Zero curr curr where
 221         error_type_liftN _ = id
 222 instance Error_Type_LiftN 'Zero curr (Error_Type_Cons curr next) where
 223         error_type_liftN _ = Error_Type_Curr
 224 instance
 225  Error_Type_LiftN n other next =>
 226  Error_Type_LiftN ('Succ n) other (Error_Type_Cons curr next) where
 227         error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)
 228
 229 -- | Convenient wrapper around 'error_type_unliftN',
 230 -- passing it the 'Peano' number from 'Peano_of_Type'.
 231 error_type_lift
 232  :: forall err errs.
 233  Error_Type_Lift err errs =>
 234  err -> errs
 235 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 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 'Exists_Type'
 243
 244 -- | Existential data type to wrap an indexed type.
 245 data Exists_Type ty
 246  = forall h. Exists_Type (ty h)
 247 instance -- Eq
 248  Type_Eq ty =>
 249  Eq (Exists_Type ty) where
 250         Exists_Type xh == Exists_Type yh =
 251                 isJust $ type_eq xh yh
 252 instance -- Show
 253  String_from_Type ty =>
 254  Show (Exists_Type ty) where
 255         show (Exists_Type ty) = string_from_type ty
 256
 257 -- * Type 'Exists_Type_and_Repr'
 258 data Exists_Type_and_Repr ty repr
 259  =   forall h.
 260      Exists_Type_and_Repr (ty h) (repr h)