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 @ast@ data into a 'Root_of_Type',
  31 -- or return 'Nothing' if the @ast@ value is not supported
  32 -- or an 'Error_Type' if it is not well-formed.
  33 class Type_Eq ty =>
  34       Type_from ast (ty:: * -> *) where
  35         type_from
  36          :: Proxy ty
  37          -> ast
  38          -> (forall h. Root_of_Type ty h
  39                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  40          ->            Either (Error_of_Type ast (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 (ast:: *) (ty:: * -> *) :: *
  49
  50 -- * Type 'Type_Root'
  51 -- | The root type, passing itself as parameter to the given type.
  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 ast (Type_Root ty)
  57  = Error_Type_Cons (Error_Type ast)
  58                    (Error_of_Type ast (ty (Type_Root ty)))
  59  -- NOTE: require UndecidableInstances.
  60 instance -- Type_Eq
  61  Type_Eq (ty (Type_Root ty)) =>
  62  Type_Eq (Type_Root ty) where
  63         type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
  64 instance -- Eq
  65  Type_Eq (Type_Root ty) =>
  66  Eq (Type_Root ty h) where
  67         x == y = isJust $ type_eq x y
  68 instance -- Type_from
  69  ( Type_Eq (Type_Root ty)
  70  , Type_from ast (ty (Type_Root ty))
  71  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  72  ) => Type_from ast (Type_Root ty) where
  73         type_from _px_ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
  74 instance -- String_from_Type
  75  String_from_Type (ty (Type_Root ty)) =>
  76  String_from_Type (Type_Root ty) where
  77         string_from_type (Type_Root ty) = string_from_type ty
  78 instance -- Show
  79  String_from_Type (Type_Root ty) =>
  80  Show (Type_Root ty h) where
  81         show = string_from_type
  82
  83 -- ** Class 'Type_Root_Lift'
  84 -- | Lift a given type to a given root type.
  85 class Type_Root_Lift ty root where
  86         type_root_lift :: forall h. ty root h -> root h
  87 instance
  88  Type_Lift ty root =>
  89  Type_Root_Lift ty (Type_Root root) where
  90         type_root_lift = Type_Root . type_lift
  91
  92 -- * Type 'Type_Cons'
  93 -- | Combine two types into one.
  94 data Type_Cons curr next (root:: * -> *) h
  95  =   Type_Curr (curr root h)
  96  |   Type_Next (next root h)
  97 type instance Root_of_Type (Type_Cons curr next root) = root
  98 type instance Error_of_Type ast (Type_Cons curr next root)
  99  = Error_Type_Cons (Error_of_Type ast (curr root))
 100                    (Error_of_Type ast (next root))
 101 instance -- Type_Eq
 102  ( Type_Eq (curr root)
 103  , Type_Eq (next root)
 104  ) => Type_Eq (Type_Cons curr next root) where
 105         type_eq (Type_Curr x) (Type_Curr y) = x `type_eq` y
 106         type_eq (Type_Next x) (Type_Next y) = x `type_eq` y
 107         type_eq _ _ = Nothing
 108 instance -- Eq
 109  ( Type_Eq (curr root)
 110  , Type_Eq (next root)
 111  ) => Eq (Type_Cons curr next root h) where
 112         x == y = isJust $ type_eq x y
 113 instance -- Type_from
 114  ( Type_Eq (curr root)
 115  , Type_from ast (curr root)
 116  , Type_from ast (next root)
 117  , Root_of_Type (curr root) ~ root
 118  , Root_of_Type (next root) ~ root
 119  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 120  ) => Type_from ast (Type_Cons curr next root) where
 121         type_from _px_ty ast k =
 122                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 123                  Right ret -> ret
 124                  Left err ->
 125                         case error_type_unlift err of
 126                          Just (Error_Type_Unsupported (_::ast)) ->
 127                                 type_from (Proxy::Proxy (next root)) ast k
 128                          _ -> Left err
 129 instance -- String_from_Type
 130  ( String_from_Type (curr root)
 131  , String_from_Type (next root)
 132  ) => String_from_Type (Type_Cons curr next root) where
 133         string_from_type (Type_Curr t) = string_from_type t
 134         string_from_type (Type_Next t) = string_from_type t
 135
 136 -- ** Type 'Type_Lift'
 137 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 138 type Type_Lift ty tys
 139  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 140
 141 -- *** Type 'Peano_of_Type'
 142 -- | Return a 'Peano' number derived from the location
 143 -- of a given type within a given type stack.
 144 type family Peano_of_Type
 145  (ty::  (* -> *) -> * -> *)
 146  (tys:: (* -> *) -> * -> *) :: Peano where
 147         Peano_of_Type ty ty                       = 'Zero
 148         Peano_of_Type ty (Type_Cons ty next)      = 'Zero
 149         Peano_of_Type other (Type_Cons curr next) = 'Succ (Peano_of_Type other next)
 150
 151 -- *** Class 'Type_LiftN'
 152 -- | Lift a given type to the top of a given type stack including it,
 153 -- by constructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 154 class Type_LiftN (n::Peano) ty tys where
 155         type_liftN :: forall (root:: * -> *) h. Proxy n -> ty root h -> tys root h
 156 instance Type_LiftN 'Zero curr curr where
 157         type_liftN _ = id
 158 instance Type_LiftN 'Zero curr (Type_Cons curr next) where
 159         type_liftN _ = Type_Curr
 160 instance
 161  Type_LiftN n other next =>
 162  Type_LiftN ('Succ n) other (Type_Cons curr next) where
 163         type_liftN _ = Type_Next . type_liftN (Proxy::Proxy n)
 164
 165 -- | Convenient wrapper around 'type_liftN',
 166 -- passing it the 'Peano' number from 'Peano_of_Type',
 167 -- used to avoid @OverlappingInstances@.
 168 type_lift
 169  :: forall ty tys (root:: * -> *) h.
 170  Type_Lift ty tys =>
 171  ty root h -> tys root h
 172 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 173
 174 -- ** Type 'Type_Unlift'
 175 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 176 type Type_Unlift ty tys
 177  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 178
 179 -- *** Class 'Type_UnliftN'
 180 -- | Try to unlift a given type out of a given type stack including it,
 181 -- by deconstructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 182 class Type_UnliftN (n::Peano) ty tys where
 183         type_unliftN :: forall (root:: * -> *) h. Proxy n -> tys root h -> Maybe (ty root h)
 184 instance Type_UnliftN 'Zero curr curr where
 185         type_unliftN _ = Just
 186 instance Type_UnliftN 'Zero curr (Type_Cons curr next) where
 187         type_unliftN _ (Type_Curr x) = Just x
 188         type_unliftN _ (Type_Next _) = Nothing
 189 instance
 190  Type_UnliftN n other next =>
 191  Type_UnliftN ('Succ n) other (Type_Cons curr next) where
 192         type_unliftN _ (Type_Next x) = type_unliftN (Proxy::Proxy n) x
 193         type_unliftN _ (Type_Curr _) = Nothing
 194
 195 -- | Convenient wrapper around 'type_unliftN',
 196 -- passing it the 'Peano' number from 'Peano_of_Type',
 197 -- used to avoid @OverlappingInstances@.
 198 type_unlift
 199  :: forall ty tys (root:: * -> *) h.
 200  Type_Unlift ty tys =>
 201  tys root h -> Maybe (ty root h)
 202 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 203
 204 -- * Type family 'Is_Last_Type'
 205 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 206         Is_Last_Type ty ty                                = 'True
 207         Is_Last_Type ty        (Type_Root tys)            = Is_Last_Type ty (tys (Type_Root tys))
 208         Is_Last_Type (ty root) (Type_Cons ty   next root) = 'False
 209         Is_Last_Type other     (Type_Cons curr next root) = Is_Last_Type other (next root)
 210
 211 -- * Type 'Error_Type_Cons'
 212 -- | Combine two error types into one.
 213 data Error_Type_Cons curr next
 214  =   Error_Type_Curr curr
 215  |   Error_Type_Next next
 216  deriving (Eq, Show)
 217
 218 -- ** Type 'Error_Type_Lift'
 219 type Error_Type_Lift err errs
 220  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 221
 222 -- *** Type 'Peano_of_Error_Type'
 223 -- | Return a 'Peano' number derived from the location
 224 -- of a given error type within a given error type stack.
 225 type family Peano_of_Error_Type (err:: *) (errs:: *) :: Peano where
 226         Peano_of_Error_Type err err                           = 'Zero
 227         Peano_of_Error_Type err (Error_Type_Cons err next)    = 'Zero
 228         Peano_of_Error_Type other (Error_Type_Cons curr next) = 'Succ (Peano_of_Error_Type other next)
 229
 230 -- *** Class 'Error_Type_LiftN'
 231 -- | Lift a given error type to the top of a given error type stack including it,
 232 -- by constructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
 233 class Error_Type_LiftN (n::Peano) err errs where
 234         error_type_liftN :: Proxy n -> err -> errs
 235 instance Error_Type_LiftN 'Zero curr curr where
 236         error_type_liftN _ = id
 237 instance Error_Type_LiftN 'Zero curr (Error_Type_Cons curr next) where
 238         error_type_liftN _ = Error_Type_Curr
 239 instance
 240  Error_Type_LiftN n other next =>
 241  Error_Type_LiftN ('Succ n) other (Error_Type_Cons curr next) where
 242         error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)
 243
 244 -- | Convenient wrapper around 'error_type_unliftN',
 245 -- passing it the 'Peano' number from 'Peano_of_Type',
 246 -- used to avoid @OverlappingInstances@.
 247 error_type_lift
 248  :: forall err errs.
 249  Error_Type_Lift err errs =>
 250  err -> errs
 251 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 252
 253 -- ** Type 'Error_Type_Unlift'
 254 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 255 type Error_Type_Unlift ty tys
 256  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 257
 258 -- | Convenient wrapper around 'error_type_unliftN',
 259 -- passing it the 'Peano' number from 'Peano_of_Error_Type',
 260 -- used to avoid @OverlappingInstances@.
 261 error_type_unlift
 262  :: forall ty tys.
 263  Error_Type_Unlift ty tys =>
 264  tys -> Maybe ty
 265 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 266
 267 -- *** Class 'Error_Type_UnliftN'
 268 -- | Try to unlift a given type error out of a given type error stack including it,
 269 -- by deconstructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
 270 class Error_Type_UnliftN (n::Peano) ty tys where
 271         error_type_unliftN :: Proxy n -> tys -> Maybe ty
 272 instance Error_Type_UnliftN 'Zero curr curr where
 273         error_type_unliftN _ = Just
 274 instance Error_Type_UnliftN 'Zero curr (Error_Type_Cons curr next) where
 275         error_type_unliftN _ (Error_Type_Curr x) = Just x
 276         error_type_unliftN _ (Error_Type_Next _) = Nothing
 277 instance
 278  Error_Type_UnliftN n other next =>
 279  Error_Type_UnliftN ('Succ n) other (Error_Type_Cons curr next) where
 280         error_type_unliftN _ (Error_Type_Next x) = error_type_unliftN (Proxy::Proxy n) x
 281         error_type_unliftN _ (Error_Type_Curr _) = Nothing
 282
 283 -- ** Type 'Error_Type_Read'
 284 -- | Common type errors.
 285 data Error_Type ast
 286  =   Error_Type_Unsupported ast
 287  |   Error_Type_Unsupported_from_root ast
 288  deriving (Eq, Show)
 289
 290 -- * Class 'String_from_Type'
 291 -- | Return a 'String' from a type.
 292 class String_from_Type ty where
 293         string_from_type :: ty h -> String
 294
 295 -- * Type 'Exists_Type'
 296
 297 -- | Existential data type to wrap an indexed type.
 298 data Exists_Type ty
 299  = forall h. Exists_Type (ty h)
 300 instance -- Eq
 301  Type_Eq ty =>
 302  Eq (Exists_Type ty) where
 303         Exists_Type xh == Exists_Type yh =
 304                 isJust $ type_eq xh yh
 305 instance -- Show
 306  String_from_Type ty =>
 307  Show (Exists_Type ty) where
 308         show (Exists_Type ty) = string_from_type ty
 309
 310 -- * Type 'Exists_Type_and_Repr'
 311 data Exists_Type_and_Repr ty repr
 312  =   forall h.
 313      Exists_Type_and_Repr (ty h) (repr h)
 314
 315 -- * Type family 'HBool'
 316 type family HEq x y :: Bool where
 317         HEq x x = 'True
 318         HEq x y = 'False
 319 -- ** Type 'HBool'
 320 data HBool b where
 321         HTrue  :: HBool 'True
 322         HFalse :: HBool 'False
 323 -- ** Class family 'Implicit_HBool'
 324 class    Implicit_HBool b      where hbool :: HBool b
 325 instance Implicit_HBool 'True  where hbool = HTrue
 326 instance Implicit_HBool 'False where hbool = HFalse