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