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 '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_Constraint'
  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 Type_Constraint (c:: * -> Constraint) (ty:: * -> *) where
  34         type_constraint :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  35         type_constraint _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 Type_Eq 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 -- Type_Eq
  84  Type_Eq (ty (Type_Root ty)) =>
  85  Type_Eq (Type_Root ty) where
  86         type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
  87 instance -- Eq
  88  Type_Eq (Type_Root ty) =>
  89  Eq (Type_Root ty h) where
  90         x == y = isJust $ x `type_eq` y
  91 instance -- Type_Constraint c Type_Root
  92  Type_Constraint c (ty (Type_Root ty)) =>
  93  Type_Constraint c (Type_Root ty) where
  94         type_constraint c (Type_Root ty) = type_constraint c ty
  95 instance -- Type_from
  96  ( Type_Eq (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 type instance Root_of_Type (Type_Alt curr next root) = root
 125 type instance Error_of_Type ast (Type_Alt curr next root)
 126  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
 127                          (Error_of_Type ast (next root))
 128 -- ** Type family 'Error_of_Type_Alt'
 129 -- | Remove 'No_Type' type when building 'Error_of_Type'.
 130 type family Error_of_Type_Alt ast curr next where
 131         Error_of_Type_Alt ast curr          No_Error_Type = curr
 132         Error_of_Type_Alt ast No_Error_Type next          = next
 133         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
 134
 135 -- ** Type 'No_Error_Type'
 136 -- | A discarded error.
 137 data No_Error_Type
 138  =   No_Error_Type
 139  deriving (Eq, Show)
 140
 141 instance -- Type_Eq
 142  ( Type_Eq (curr root)
 143  , Type_Eq (next root)
 144  ) => Type_Eq (Type_Alt curr next root) where
 145         type_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type_eq` y
 146         type_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type_eq` y
 147         type_eq _ _ = Nothing
 148 instance -- Eq
 149  ( Type_Eq (curr root)
 150  , Type_Eq (next root)
 151  ) => Eq (Type_Alt curr next root h) where
 152         x == y = isJust $ x `type_eq` y
 153 instance -- Type_Constraint c Type_Alt
 154  ( Type_Constraint c (curr root)
 155  , Type_Constraint c (next root)
 156  ) => Type_Constraint c (Type_Alt curr next root) where
 157         type_constraint c (Type_Alt_Curr ty) = type_constraint c ty
 158         type_constraint c (Type_Alt_Next ty) = type_constraint c ty
 159 instance -- Type_from
 160  ( Type_Eq (curr root)
 161  , Type_from ast (curr root)
 162  , Type_from ast (next root)
 163  , Root_of_Type (curr root) ~ root
 164  , Root_of_Type (next root) ~ root
 165  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 166  ) => Type_from ast (Type_Alt curr next root) where
 167         type_from _ty ast k =
 168                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 169                  Right ret -> ret
 170                  Left err ->
 171                         case error_type_unlift err of
 172                          Just (Error_Type_Unsupported_here (_::ast)) ->
 173                                 type_from (Proxy::Proxy (next root)) ast k
 174                          _ -> Left err
 175 instance -- String_from_Type
 176  ( String_from_Type (curr root)
 177  , String_from_Type (next root)
 178  ) => String_from_Type (Type_Alt curr next root) where
 179         string_from_type (Type_Alt_Curr t) = string_from_type t
 180         string_from_type (Type_Alt_Next t) = string_from_type t
 181
 182 -- ** Type 'Type_Lift'
 183 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 184 type Type_Lift ty tys
 185  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 186
 187 -- *** Type 'Peano_of_Type'
 188 -- | Return a 'Peano' number derived from the location
 189 -- of a given type within a given type stack,
 190 -- which is used to avoid @OverlappingInstances@.
 191 type family Peano_of_Type
 192  (ty::  (* -> *) -> * -> *)
 193  (tys:: (* -> *) -> * -> *) :: * where
 194         Peano_of_Type ty    ty                   = Zero
 195         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 196         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 197
 198 -- *** Class 'Type_LiftN'
 199 -- | Lift a given type to the top of a given type stack including it,
 200 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 201 class Type_LiftN (p:: *) ty tys where
 202         type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 203 instance Type_LiftN Zero curr curr where
 204         type_liftN _ = id
 205 instance Type_LiftN Zero curr (Type_Alt curr next) where
 206         type_liftN _ = Type_Alt_Curr
 207 instance
 208  Type_LiftN p other next =>
 209  Type_LiftN (Succ p) other (Type_Alt curr next) where
 210         type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
 211
 212 -- | Convenient wrapper around 'type_liftN',
 213 -- passing it the 'Peano' number from 'Peano_of_Type'.
 214 type_lift
 215  :: forall ty tys (root:: * -> *) h.
 216  Type_Lift ty tys =>
 217  ty root h -> tys root h
 218 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 219
 220 -- ** Type 'Type_Unlift'
 221 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 222 type Type_Unlift ty tys
 223  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 224
 225 -- *** Class 'Type_UnliftN'
 226 -- | Try to unlift a given type out of a given type stack including it,
 227 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 228 class Type_UnliftN (p:: *) ty tys where
 229         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 230 instance Type_UnliftN Zero curr curr where
 231         type_unliftN _ = Just
 232 instance Type_UnliftN Zero curr (Type_Alt curr next) where
 233         type_unliftN _ (Type_Alt_Curr x) = Just x
 234         type_unliftN _ (Type_Alt_Next _) = Nothing
 235 instance
 236  Type_UnliftN p other next =>
 237  Type_UnliftN (Succ p) other (Type_Alt curr next) where
 238         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 239         type_unliftN _ (Type_Alt_Curr _) = Nothing
 240
 241 -- | Convenient wrapper around 'type_unliftN',
 242 -- passing it the 'Peano' number from 'Peano_of_Type'.
 243 type_unlift
 244  :: forall ty tys (root:: * -> *) h.
 245  Type_Unlift ty tys =>
 246  tys root h -> Maybe (ty root h)
 247 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 248
 249 -- ** Type family 'Is_Last_Type'
 250 -- | Return whether a given type is the last one in a given type stack.
 251 --
 252 -- NOTE: each type parser uses this type family
 253 -- when it encounters unsupported syntax:
 254 -- to know if it is the last type parser component that will be tried
 255 -- (and thus return 'Error_Type_Unsupported')
 256 -- or if some other type parser component shall be tried
 257 -- (and thus return 'Error_Type_Unsupported_here',
 258 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 259 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 260         Is_Last_Type ty ty                               = 'True
 261         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 262         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 263         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 264
 265 -- * Type 'Error_Type_Alt'
 266 -- | Error type making an alternative between two error types.
 267 data Error_Type_Alt curr next
 268  =   Error_Type_Alt_Curr curr
 269  |   Error_Type_Alt_Next next
 270  deriving (Eq, Show)
 271
 272 -- ** Type 'Error_Type_Lift'
 273 type Error_Type_Lift err errs
 274  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 275
 276 -- *** Type 'Peano_of_Error_Type'
 277 -- | Return a 'Peano' number derived from the location
 278 -- of a given error type within a given error type stack.
 279 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
 280         Peano_of_Error_Type err   err                        = Zero
 281         Peano_of_Error_Type err   (Error_Type_Alt err next)  = Zero
 282         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
 283
 284 -- *** Class 'Error_Type_LiftN'
 285 -- | Lift a given error type to the top of a given error type stack including it,
 286 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 287 class Error_Type_LiftN (p:: *) err errs where
 288         error_type_liftN :: Proxy p -> err -> errs
 289 instance Error_Type_LiftN Zero curr curr where
 290         error_type_liftN _ = id
 291 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
 292         error_type_liftN _ = Error_Type_Alt_Curr
 293 instance
 294  Error_Type_LiftN p other next =>
 295  Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
 296         error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
 297
 298 -- | Convenient wrapper around 'error_type_unliftN',
 299 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 300 error_type_lift
 301  :: forall err errs.
 302  Error_Type_Lift err errs =>
 303  err -> errs
 304 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 305
 306 -- ** Type 'Error_Type_Unlift'
 307 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 308 type Error_Type_Unlift ty tys
 309  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 310
 311 -- | Convenient wrapper around 'error_type_unliftN',
 312 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 313 error_type_unlift
 314  :: forall ty tys.
 315  Error_Type_Unlift ty tys =>
 316  tys -> Maybe ty
 317 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 318
 319 -- *** Class 'Error_Type_UnliftN'
 320 -- | Try to unlift a given type error out of a given type error stack including it,
 321 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 322 class Error_Type_UnliftN (p:: *) ty tys where
 323         error_type_unliftN :: Proxy p -> tys -> Maybe ty
 324 instance Error_Type_UnliftN Zero curr curr where
 325         error_type_unliftN _ = Just
 326 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
 327         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 328         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 329 instance
 330  Error_Type_UnliftN p other next =>
 331  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 332         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 333         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 334
 335 -- ** Type 'Error_Type_Read'
 336 -- | Common type errors.
 337 data Error_Type ast
 338  =   Error_Type_Unsupported ast
 339  -- ^ Given syntax is supported by none
 340  -- of the type parser components
 341  -- of the type stack.
 342  |   Error_Type_Unsupported_here ast
 343  -- ^ Given syntax not supported by the current type parser component.
 344  |   Error_Type_Wrong_number_of_arguments ast Int
 345  deriving (Eq, Show)
 346
 347 -- | Convenient wrapper around 'error_type_lift',
 348 -- passing the type family boilerplate.
 349 error_type
 350  :: Error_Type_Lift (Error_Type ast)
 351                     (Error_of_Type ast (Root_of_Type ty))
 352  => Proxy ty
 353  -> Error_Type ast
 354  -> Error_of_Type ast (Root_of_Type ty)
 355 error_type _ = error_type_lift
 356
 357 error_type_unsupported
 358  :: forall ast ty.
 359  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 360  , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 361  ) => Proxy ty -> ast
 362  -> Error_of_Type ast (Root_of_Type ty)
 363 error_type_unsupported ty ast =
 364         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 365          HTrue  -> error_type ty $ Error_Type_Unsupported ast
 366          HFalse -> error_type ty $ Error_Type_Unsupported_here ast
 367
 368 -- * Class 'String_from_Type'
 369 -- | Return a 'String' from a type.
 370 class String_from_Type ty where
 371         string_from_type :: ty h -> String
 372
 373 -- * Type 'Exists_Type'
 374 -- | Existential data type wrapping the index of a type.
 375 data Exists_Type ty
 376  = forall h. Exists_Type (ty h)
 377 instance -- Eq
 378  Type_Eq ty =>
 379  Eq (Exists_Type ty) where
 380         Exists_Type xh == Exists_Type yh =
 381                 isJust $ xh `type_eq` yh
 382 instance -- Show
 383  String_from_Type ty =>
 384  Show (Exists_Type ty) where
 385         show (Exists_Type ty) = string_from_type ty
 386
 387 -- * Type 'Exists_Type_and_Repr'
 388 data Exists_Type_and_Repr ty repr
 389  =   forall h.
 390      Exists_Type_and_Repr (ty h) (repr h)
 391
 392 -- * Type family 'HBool'
 393 -- | Host-type equality.
 394 type family HEq x y :: Bool where
 395         HEq x x = 'True
 396         HEq x y = 'False
 397 -- ** Type 'HBool'
 398 -- | Boolean singleton.
 399 data HBool b where
 400         HTrue  :: HBool 'True
 401         HFalse :: HBool 'False
 402 -- ** Class 'Implicit_HBool'
 403 -- | Construct a host-term boolean singleton from a host-type boolean.
 404 class    Implicit_HBool b      where hbool :: HBool b
 405 instance Implicit_HBool 'True  where hbool = HTrue
 406 instance Implicit_HBool 'False where hbool = HFalse