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