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 PolyKinds #-}
   9 {-# LANGUAGE MultiParamTypeClasses #-}
  10 {-# LANGUAGE Rank2Types #-}
  11 {-# LANGUAGE ScopedTypeVariables #-}
  12 {-# LANGUAGE TypeFamilies #-}
  13 {-# LANGUAGE TypeOperators #-}
  14 {-# LANGUAGE UndecidableInstances #-}
  15 module Language.LOL.Symantic.Type.Common where
  16
  17 import Data.Maybe (isJust)
  18 import Language.LOL.Symantic.Lib.Data.Peano
  19 import Data.Proxy
  20 import Data.Type.Equality ((:~:))
  21
  22 -- * Class 'Type_Eq'
  23
  24 -- | Test two types for equality,
  25 -- returning an Haskell type-level proof
  26 -- of the equality when it holds.
  27 class Type_Eq (ty:: k -> *) where
  28         type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  29
  30 -- * Class 'Type_from'
  31 -- | Parse given @ast@ into a 'Root_of_Type',
  32 -- or return an 'Error_of_Type'.
  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_Alt (Error_Type ast)
  58                   (Error_of_Type ast (ty (Type_Root ty)))
  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 $ x `type_eq` y
  67 instance -- Type_from
  68  ( Type_Eq (Type_Root ty)
  69  , Type_from ast (ty (Type_Root ty))
  70  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  71  ) => Type_from ast (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_Lift ty root =>
  88  Type_Root_Lift ty (Type_Root root) where
  89         type_root_lift = Type_Root . type_lift
  90
  91 -- * Type 'Type_Alt'
  92 -- | Type making an alternative between two types.
  93 data Type_Alt curr next (root:: * -> *) h
  94  =   Type_Alt_Curr (curr root h)
  95  |   Type_Alt_Next (next root h)
  96 type instance Root_of_Type (Type_Alt curr next root) = root
  97 type instance Error_of_Type ast (Type_Alt curr next root)
  98  = Error_Type_Alt (Error_of_Type ast (curr root))
  99                   (Error_of_Type ast (next root))
 100 instance -- Type_Eq
 101  ( Type_Eq (curr root)
 102  , Type_Eq (next root)
 103  ) => Type_Eq (Type_Alt curr next root) where
 104         type_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type_eq` y
 105         type_eq (Type_Alt_Next x) (Type_Alt_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_Alt curr next root h) where
 111         x == y = isJust $ x `type_eq` y
 112 instance -- Type_from
 113  ( Type_Eq (curr root)
 114  , Type_from ast (curr root)
 115  , Type_from ast (next root)
 116  , Root_of_Type (curr root) ~ root
 117  , Root_of_Type (next root) ~ root
 118  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 119  ) => Type_from ast (Type_Alt curr next root) where
 120         type_from _px_ty ast k =
 121                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 122                  Right ret -> ret
 123                  Left err ->
 124                         case error_type_unlift err of
 125                          Just (Error_Type_Unsupported_here (_::ast)) ->
 126                                 type_from (Proxy::Proxy (next root)) ast k
 127                          _ -> Left err
 128 instance -- String_from_Type
 129  ( String_from_Type (curr root)
 130  , String_from_Type (next root)
 131  ) => String_from_Type (Type_Alt curr next root) where
 132         string_from_type (Type_Alt_Curr t) = string_from_type t
 133         string_from_type (Type_Alt_Next t) = string_from_type t
 134
 135 -- ** Type 'Type_Lift'
 136 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 137 type Type_Lift ty tys
 138  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 139
 140 -- *** Type 'Peano_of_Type'
 141 -- | Return a 'Peano' number derived from the location
 142 -- of a given type within a given type stack,
 143 -- which is used to avoid @OverlappingInstances@.
 144 type family Peano_of_Type
 145  (ty::  (* -> *) -> * -> *)
 146  (tys:: (* -> *) -> * -> *) :: * where
 147         Peano_of_Type ty    ty                   = Zero
 148         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 149         Peano_of_Type other (Type_Alt 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_Alt_Curr' and 'Type_Alt_Next'.
 154 class Type_LiftN (p:: *) ty tys where
 155         type_liftN :: forall (root:: * -> *) h. Proxy p -> 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_Alt curr next) where
 159         type_liftN _ = Type_Alt_Curr
 160 instance
 161  Type_LiftN p other next =>
 162  Type_LiftN (Succ p) other (Type_Alt curr next) where
 163         type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
 164
 165 -- | Convenient wrapper around 'type_liftN',
 166 -- passing it the 'Peano' number from 'Peano_of_Type'.
 167 type_lift
 168  :: forall ty tys (root:: * -> *) h.
 169  Type_Lift ty tys =>
 170  ty root h -> tys root h
 171 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 172
 173 -- ** Type 'Type_Unlift'
 174 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 175 type Type_Unlift ty tys
 176  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 177
 178 -- *** Class 'Type_UnliftN'
 179 -- | Try to unlift a given type out of a given type stack including it,
 180 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 181 class Type_UnliftN (p:: *) ty tys where
 182         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 183 instance Type_UnliftN Zero curr curr where
 184         type_unliftN _ = Just
 185 instance Type_UnliftN Zero curr (Type_Alt curr next) where
 186         type_unliftN _ (Type_Alt_Curr x) = Just x
 187         type_unliftN _ (Type_Alt_Next _) = Nothing
 188 instance
 189  Type_UnliftN p other next =>
 190  Type_UnliftN (Succ p) other (Type_Alt curr next) where
 191         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 192         type_unliftN _ (Type_Alt_Curr _) = Nothing
 193
 194 -- | Convenient wrapper around 'type_unliftN',
 195 -- passing it the 'Peano' number from 'Peano_of_Type'.
 196 type_unlift
 197  :: forall ty tys (root:: * -> *) h.
 198  Type_Unlift ty tys =>
 199  tys root h -> Maybe (ty root h)
 200 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 201
 202 -- ** Type family 'Is_Last_Type'
 203 -- | Return whether a given type is the last one in a given type stack.
 204 --
 205 -- NOTE: each type parser uses this type family
 206 -- when it encounters unsupported syntax:
 207 -- to know if it is the last type parser component that will be tried
 208 -- (and thus return 'Error_Type_Unsupported')
 209 -- or if some other type parser component shall be tried
 210 -- (and thus return 'Error_Type_Unsupported_here',
 211 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 212 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 213         Is_Last_Type ty ty                               = 'True
 214         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 215         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 216         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 217
 218 -- * Type 'Error_Type_Alt'
 219 -- | Error type making an alternative between two error types.
 220 data Error_Type_Alt curr next
 221  =   Error_Type_Alt_Curr curr
 222  |   Error_Type_Alt_Next next
 223  deriving (Eq, Show)
 224
 225 -- ** Type 'Error_Type_Lift'
 226 type Error_Type_Lift err errs
 227  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 228
 229 -- *** Type 'Peano_of_Error_Type'
 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:: *) :: * where
 233         Peano_of_Error_Type err   err                        = Zero
 234         Peano_of_Error_Type err   (Error_Type_Alt err next)  = Zero
 235         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
 236
 237 -- *** Class 'Error_Type_LiftN'
 238 -- | Lift a given error type to the top of a given error type stack including it,
 239 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 240 class Error_Type_LiftN (p:: *) err errs where
 241         error_type_liftN :: Proxy p -> err -> errs
 242 instance Error_Type_LiftN Zero curr curr where
 243         error_type_liftN _ = id
 244 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
 245         error_type_liftN _ = Error_Type_Alt_Curr
 246 instance
 247  Error_Type_LiftN p other next =>
 248  Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
 249         error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
 250
 251 -- | Convenient wrapper around 'error_type_unliftN',
 252 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 253 error_type_lift
 254  :: forall err errs.
 255  Error_Type_Lift err errs =>
 256  err -> errs
 257 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 258
 259 -- ** Type 'Error_Type_Unlift'
 260 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 261 type Error_Type_Unlift ty tys
 262  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 263
 264 -- | Convenient wrapper around 'error_type_unliftN',
 265 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 266 error_type_unlift
 267  :: forall ty tys.
 268  Error_Type_Unlift ty tys =>
 269  tys -> Maybe ty
 270 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 271
 272 -- *** Class 'Error_Type_UnliftN'
 273 -- | Try to unlift a given type error out of a given type error stack including it,
 274 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 275 class Error_Type_UnliftN (p:: *) ty tys where
 276         error_type_unliftN :: Proxy p -> tys -> Maybe ty
 277 instance Error_Type_UnliftN Zero curr curr where
 278         error_type_unliftN _ = Just
 279 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
 280         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 281         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 282 instance
 283  Error_Type_UnliftN p other next =>
 284  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 285         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 286         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 287
 288 -- ** Type 'Error_Type_Read'
 289 -- | Common type errors.
 290 data Error_Type ast
 291  =   Error_Type_Unsupported ast
 292  -- ^ Given syntax is supported by none
 293  -- of the type parser components
 294  -- of the type stack.
 295  |   Error_Type_Unsupported_here ast
 296  -- ^ Given syntax not supported by the current type parser component.
 297  |   Error_Type_Wrong_number_of_arguments ast Int
 298  deriving (Eq, Show)
 299
 300 -- | Convenient wrapper around 'error_type_lift',
 301 -- passing the type family boilerplate.
 302 error_type
 303  :: Error_Type_Lift (Error_Type ast)
 304                     (Error_of_Type ast (Root_of_Type ty))
 305  => Proxy ty
 306  -> Error_Type ast
 307  -> Error_of_Type ast (Root_of_Type ty)
 308 error_type _ = error_type_lift
 309
 310 error_type_unsupported
 311  :: forall ast ty.
 312  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 313  , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 314  ) => Proxy ty -> ast
 315  -> Error_of_Type ast (Root_of_Type ty)
 316 error_type_unsupported px_ty ast =
 317         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 318          HTrue  -> error_type px_ty $ Error_Type_Unsupported ast
 319          HFalse -> error_type px_ty $ Error_Type_Unsupported_here ast
 320
 321 -- * Class 'String_from_Type'
 322 -- | Return a 'String' from a type.
 323 class String_from_Type ty where
 324         string_from_type :: ty h -> String
 325
 326 -- * Type 'Exists_Type'
 327
 328 -- | Existential data type to wrap an indexed type.
 329 data Exists_Type ty
 330  = forall h. Exists_Type (ty h)
 331 instance -- Eq
 332  Type_Eq ty =>
 333  Eq (Exists_Type ty) where
 334         Exists_Type xh == Exists_Type yh =
 335                 isJust $ xh `type_eq` yh
 336 instance -- Show
 337  String_from_Type ty =>
 338  Show (Exists_Type ty) where
 339         show (Exists_Type ty) = string_from_type ty
 340
 341 -- * Type 'Exists_Type_and_Repr'
 342 data Exists_Type_and_Repr ty repr
 343  =   forall h.
 344      Exists_Type_and_Repr (ty h) (repr h)
 345
 346 -- * Type family 'HBool'
 347 -- | Host-type equality.
 348 type family HEq x y :: Bool where
 349         HEq x x = 'True
 350         HEq x y = 'False
 351 -- ** Type 'HBool'
 352 -- | Boolean singleton.
 353 data HBool b where
 354         HTrue  :: HBool 'True
 355         HFalse :: HBool 'False
 356 -- ** Class 'Implicit_HBool'
 357 -- | Construct a host-term boolean singleton from a host-type boolean.
 358 class    Implicit_HBool b      where hbool :: HBool b
 359 instance Implicit_HBool 'True  where hbool = HTrue
 360 instance Implicit_HBool 'False where hbool = HFalse