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