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