Language/Symantic/Type/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Type.Common where
  14
  15 import Data.Maybe (isJust)
  16 import Data.Proxy
  17 import Data.Type.Equality ((:~:))
  18 import Language.Symantic.Lib.Data.Peano
  19 import GHC.Prim (Constraint)
  20
  21 -- * Class 'Eq_Type'
  22
  23 -- | Test two types for equality,
  24 -- returning an Haskell type-level proof
  25 -- of the equality when it holds.
  26 class Eq_Type (ty:: * -> *) where
  27         eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  28
  29 -- * Class 'Constraint_Type'
  30 -- | Test if a type satisfies a given 'Constraint',
  31 -- returning an Haskell type-level proof
  32 -- of that satisfaction when it holds.
  33 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
  34         constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  35         constraint_type _c _ = Nothing
  36
  37 -- ** Type 'Dict'
  38 -- | 'Dict' captures the dictionary of a 'Constraint':
  39 -- pattern matching on the 'Dict' constructor
  40 -- brings the 'Constraint' into scope.
  41 data Dict :: Constraint -> * where
  42         Dict :: c => Dict c
  43
  44 -- * Type 'Exists_Dict'
  45 data Exists_Dict
  46  = forall c. Exists_Dict (Dict c)
  47
  48 -- * Class 'Type_from'
  49 -- | Parse given @ast@ into a 'Root_of_Type',
  50 -- or return an 'Error_of_Type'.
  51 class Eq_Type ty =>
  52       Type_from ast (ty:: * -> *) where
  53         type_from
  54          :: Proxy ty
  55          -> ast
  56          -> (forall h. Root_of_Type ty h
  57                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  58          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  59
  60 -- ** Type family 'Root_of_Type'
  61 -- | Return the root type of a type.
  62 type family Root_of_Type (ty:: * -> *) :: * -> *
  63
  64 -- ** Type family 'Error_of_Type'
  65 -- | Return the error type of a type.
  66 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
  67
  68 -- * Type 'No_Type'
  69 -- | A discarded type.
  70 data No_Type (root:: * -> *) h
  71  =   No_Type (root h)
  72  deriving (Eq, Show)
  73
  74 -- * Type 'Type_Root'
  75 -- | The root type, passing itself as parameter to the given type.
  76 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  77  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  78 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  79 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
  80 type instance Error_of_Type ast (Type_Root ty)
  81  = Error_Type_Alt (Error_Type ast)
  82                   (Error_of_Type ast (ty (Type_Root ty)))
  83 instance -- Eq_Type
  84  Eq_Type (ty (Type_Root ty)) =>
  85  Eq_Type (Type_Root ty) where
  86         eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
  87 instance -- Eq
  88  Eq_Type (Type_Root ty) =>
  89  Eq (Type_Root ty h) where
  90         x == y = isJust $ x `eq_type` y
  91 instance -- Constraint_Type c Type_Root
  92  Constraint_Type c (ty (Type_Root ty)) =>
  93  Constraint_Type c (Type_Root ty) where
  94         constraint_type c (Type_Root ty) = constraint_type c ty
  95 instance -- Type_from
  96  ( Eq_Type (Type_Root ty)
  97  , Type_from ast (ty (Type_Root ty))
  98  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  99  ) => Type_from ast (Type_Root ty) where
 100         type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
 101 instance -- String_from_Type
 102  String_from_Type (ty (Type_Root ty)) =>
 103  String_from_Type (Type_Root ty) where
 104         string_from_type (Type_Root ty) = string_from_type ty
 105 instance -- Show
 106  String_from_Type (Type_Root ty) =>
 107  Show (Type_Root ty h) where
 108         show = string_from_type
 109
 110 -- ** Class 'Type_Root_Lift'
 111 -- | Lift a given type to a given root type.
 112 class Type_Root_Lift ty root where
 113         type_root_lift :: forall h. ty root h -> root h
 114 instance
 115  Type_Lift ty root =>
 116  Type_Root_Lift ty (Type_Root root) where
 117         type_root_lift = Type_Root . type_lift
 118
 119 -- * Type 'Type_Alt'
 120 -- | Type making an alternative between two types.
 121 data Type_Alt curr next (root:: * -> *) h
 122  =   Type_Alt_Curr (curr root h)
 123  |   Type_Alt_Next (next root h)
 124 -- | Convenient alias. Requires @TypeOperators@.
 125 type (:|:) = Type_Alt
 126 infixr 5 :|:
 127 type instance Root_of_Type (Type_Alt curr next root) = root
 128 type instance Error_of_Type ast (Type_Alt curr next root)
 129  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
 130                          (Error_of_Type ast (next root))
 131 -- ** Type family 'Error_of_Type_Alt'
 132 -- | Remove 'No_Type' type when building 'Error_of_Type'.
 133 type family Error_of_Type_Alt ast curr next where
 134         Error_of_Type_Alt ast curr          No_Error_Type = curr
 135         Error_of_Type_Alt ast No_Error_Type next          = next
 136         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
 137
 138 -- ** Type 'No_Error_Type'
 139 -- | A discarded error.
 140 data No_Error_Type
 141  =   No_Error_Type
 142  deriving (Eq, Show)
 143
 144 instance -- Eq_Type
 145  ( Eq_Type (curr root)
 146  , Eq_Type (next root)
 147  ) => Eq_Type (Type_Alt curr next root) where
 148         eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
 149         eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
 150         eq_type _ _ = Nothing
 151 instance -- Eq
 152  ( Eq_Type (curr root)
 153  , Eq_Type (next root)
 154  ) => Eq (Type_Alt curr next root h) where
 155         x == y = isJust $ x `eq_type` y
 156 instance -- Constraint_Type c Type_Alt
 157  ( Constraint_Type c (curr root)
 158  , Constraint_Type c (next root)
 159  ) => Constraint_Type c (Type_Alt curr next root) where
 160         constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
 161         constraint_type c (Type_Alt_Next ty) = constraint_type c ty
 162 instance -- Type_from
 163  ( Eq_Type (curr root)
 164  , Type_from ast (curr root)
 165  , Type_from ast (next root)
 166  , Root_of_Type (curr root) ~ root
 167  , Root_of_Type (next root) ~ root
 168  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 169  ) => Type_from ast (Type_Alt curr next root) where
 170         type_from _ty ast k =
 171                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 172                  Right ret -> ret
 173                  Left err ->
 174                         case error_type_unlift err of
 175                          Just (Error_Type_Unsupported_here (_::ast)) ->
 176                                 type_from (Proxy::Proxy (next root)) ast k
 177                          _ -> Left err
 178 instance -- String_from_Type
 179  ( String_from_Type (curr root)
 180  , String_from_Type (next root)
 181  ) => String_from_Type (Type_Alt curr next root) where
 182         string_from_type (Type_Alt_Curr t) = string_from_type t
 183         string_from_type (Type_Alt_Next t) = string_from_type t
 184
 185 -- ** Type 'Type_Lift'
 186 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 187 type Type_Lift ty tys
 188  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 189
 190 -- *** Type 'Peano_of_Type'
 191 -- | Return a 'Peano' number derived from the location
 192 -- of a given type within a given type stack,
 193 -- which is used to avoid @OverlappingInstances@.
 194 type family Peano_of_Type
 195  (ty::  (* -> *) -> * -> *)
 196  (tys:: (* -> *) -> * -> *) :: * where
 197         Peano_of_Type ty    ty                   = Zero
 198         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 199         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 200
 201 -- *** Class 'Type_LiftN'
 202 -- | Lift a given type to the top of a given type stack including it,
 203 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 204 class Type_LiftN (p:: *) ty tys where
 205         type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 206 instance Type_LiftN Zero curr curr where
 207         type_liftN _ = id
 208 instance Type_LiftN Zero curr (Type_Alt curr next) where
 209         type_liftN _ = Type_Alt_Curr
 210 instance
 211  Type_LiftN p other next =>
 212  Type_LiftN (Succ p) other (Type_Alt curr next) where
 213         type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
 214
 215 -- | Convenient wrapper around 'type_liftN',
 216 -- passing it the 'Peano' number from 'Peano_of_Type'.
 217 type_lift
 218  :: forall ty tys (root:: * -> *) h.
 219  Type_Lift ty tys =>
 220  ty root h -> tys root h
 221 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 222
 223 -- ** Type 'Type_Unlift'
 224 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 225 type Type_Unlift ty tys
 226  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 227
 228 -- *** Class 'Type_UnliftN'
 229 -- | Try to unlift a given type out of a given type stack including it,
 230 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 231 class Type_UnliftN (p:: *) ty tys where
 232         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 233 instance Type_UnliftN Zero curr curr where
 234         type_unliftN _ = Just
 235 instance Type_UnliftN Zero curr (Type_Alt curr next) where
 236         type_unliftN _ (Type_Alt_Curr x) = Just x
 237         type_unliftN _ (Type_Alt_Next _) = Nothing
 238 instance
 239  Type_UnliftN p other next =>
 240  Type_UnliftN (Succ p) other (Type_Alt curr next) where
 241         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 242         type_unliftN _ (Type_Alt_Curr _) = Nothing
 243
 244 -- | Convenient wrapper around 'type_unliftN',
 245 -- passing it the 'Peano' number from 'Peano_of_Type'.
 246 type_unlift
 247  :: forall ty tys (root:: * -> *) h.
 248  Type_Unlift ty tys =>
 249  tys root h -> Maybe (ty root h)
 250 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 251
 252 -- ** Type family 'Is_Last_Type'
 253 -- | Return whether a given type is the last one in a given type stack.
 254 --
 255 -- NOTE: each type parser uses this type family
 256 -- when it encounters unsupported syntax:
 257 -- to know if it is the last type parser component that will be tried
 258 -- (and thus return 'Error_Type_Unsupported')
 259 -- or if some other type parser component shall be tried
 260 -- (and thus return 'Error_Type_Unsupported_here',
 261 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 262 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 263         Is_Last_Type ty ty                               = 'True
 264         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 265         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 266         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 267
 268 -- * Type 'Error_Type_Alt'
 269 -- | Error type making an alternative between two error types.
 270 data Error_Type_Alt curr next
 271  =   Error_Type_Alt_Curr curr
 272  |   Error_Type_Alt_Next next
 273  deriving (Eq, Show)
 274
 275 -- ** Type 'Error_Type_Lift'
 276 type Error_Type_Lift err errs
 277  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 278
 279 -- *** Type 'Peano_of_Error_Type'
 280 -- | Return a 'Peano' number derived from the location
 281 -- of a given error type within a given error type stack.
 282 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
 283         Peano_of_Error_Type err   err                        = Zero
 284         Peano_of_Error_Type err   (Error_Type_Alt err next)  = Zero
 285         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
 286
 287 -- *** Class 'Error_Type_LiftN'
 288 -- | Lift a given error type to the top of a given error type stack including it,
 289 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 290 class Error_Type_LiftN (p:: *) err errs where
 291         error_type_liftN :: Proxy p -> err -> errs
 292 instance Error_Type_LiftN Zero curr curr where
 293         error_type_liftN _ = id
 294 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
 295         error_type_liftN _ = Error_Type_Alt_Curr
 296 instance
 297  Error_Type_LiftN p other next =>
 298  Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
 299         error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
 300
 301 -- | Convenient wrapper around 'error_type_unliftN',
 302 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 303 error_type_lift
 304  :: forall err errs.
 305  Error_Type_Lift err errs =>
 306  err -> errs
 307 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 308
 309 -- ** Type 'Error_Type_Unlift'
 310 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 311 type Error_Type_Unlift ty tys
 312  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 313
 314 -- | Convenient wrapper around 'error_type_unliftN',
 315 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 316 error_type_unlift
 317  :: forall ty tys.
 318  Error_Type_Unlift ty tys =>
 319  tys -> Maybe ty
 320 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 321
 322 -- *** Class 'Error_Type_UnliftN'
 323 -- | Try to unlift a given type error out of a given type error stack including it,
 324 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 325 class Error_Type_UnliftN (p:: *) ty tys where
 326         error_type_unliftN :: Proxy p -> tys -> Maybe ty
 327 instance Error_Type_UnliftN Zero curr curr where
 328         error_type_unliftN _ = Just
 329 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
 330         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 331         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 332 instance
 333  Error_Type_UnliftN p other next =>
 334  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 335         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 336         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 337
 338 -- ** Type 'Error_Type_Read'
 339 -- | Common type errors.
 340 data Error_Type ast
 341  =   Error_Type_Unsupported ast
 342  -- ^ Given syntax is supported by none
 343  -- of the type parser components
 344  -- of the type stack.
 345  |   Error_Type_Unsupported_here ast
 346  -- ^ Given syntax not supported by the current type parser component.
 347  |   Error_Type_Wrong_number_of_arguments ast Int
 348  deriving (Eq, Show)
 349
 350 -- | Convenient wrapper around 'error_type_lift',
 351 -- passing the type family boilerplate.
 352 error_type
 353  :: Error_Type_Lift (Error_Type ast)
 354                     (Error_of_Type ast (Root_of_Type ty))
 355  => Proxy ty
 356  -> Error_Type ast
 357  -> Error_of_Type ast (Root_of_Type ty)
 358 error_type _ = error_type_lift
 359
 360 error_type_unsupported
 361  :: forall ast ty.
 362  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 363  , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 364  ) => Proxy ty -> ast
 365  -> Error_of_Type ast (Root_of_Type ty)
 366 error_type_unsupported ty ast =
 367         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 368          HTrue  -> error_type ty $ Error_Type_Unsupported ast
 369          HFalse -> error_type ty $ Error_Type_Unsupported_here ast
 370
 371 -- * Class 'String_from_Type'
 372 -- | Return a 'String' from a type.
 373 class String_from_Type ty where
 374         string_from_type :: ty h -> String
 375
 376 -- * Type 'Exists_Type'
 377 -- | Existential data type wrapping the index of a type.
 378 data Exists_Type ty
 379  = forall h. Exists_Type (ty h)
 380 instance -- Eq
 381  Eq_Type ty =>
 382  Eq (Exists_Type ty) where
 383         Exists_Type xh == Exists_Type yh =
 384                 isJust $ xh `eq_type` yh
 385 instance -- Show
 386  String_from_Type ty =>
 387  Show (Exists_Type ty) where
 388         show (Exists_Type ty) = string_from_type ty
 389
 390 -- * Type 'Exists_Type_and_Repr'
 391 data Exists_Type_and_Repr ty repr
 392  =   forall h.
 393      Exists_Type_and_Repr (ty h) (repr h)
 394
 395 -- * Type family 'HBool'
 396 -- | Host-type equality.
 397 type family HEq x y :: Bool where
 398         HEq x x = 'True
 399         HEq x y = 'False
 400 -- ** Type 'HBool'
 401 -- | Boolean singleton.
 402 data HBool b where
 403         HTrue  :: HBool 'True
 404         HFalse :: HBool 'False
 405 -- ** Class 'Implicit_HBool'
 406 -- | Construct a host-term boolean singleton from a host-type boolean.
 407 class    Implicit_HBool b      where hbool :: HBool b
 408 instance Implicit_HBool 'True  where hbool = HTrue
 409 instance Implicit_HBool 'False where hbool = HFalse