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_Alt (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_Alt'
  93 -- | Type making an alternative between two types.
  94 data Type_Alt curr next (root:: * -> *) h
  95  =   Type_Alt_Curr (curr root h)
  96  |   Type_Alt_Next (next root h)
  97 type instance Root_of_Type (Type_Alt curr next root) = root
  98 type instance Error_of_Type ast (Type_Alt curr next root)
  99  = Error_Type_Alt (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_Alt curr next root) where
 105         type_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type_eq` y
 106         type_eq (Type_Alt_Next x) (Type_Alt_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_Alt 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_Alt 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_Alt curr next root) where
 133         string_from_type (Type_Alt_Curr t) = string_from_type t
 134         string_from_type (Type_Alt_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 -- which is used to avoid @OverlappingInstances@.
 145 type family Peano_of_Type
 146  (ty::  (* -> *) -> * -> *)
 147  (tys:: (* -> *) -> * -> *) :: Peano where
 148         Peano_of_Type ty ty                       = 'Zero
 149         Peano_of_Type ty (Type_Alt ty next)      = 'Zero
 150         Peano_of_Type other (Type_Alt curr next) = 'Succ (Peano_of_Type other next)
 151
 152 -- *** Class 'Type_LiftN'
 153 -- | Lift a given type to the top of a given type stack including it,
 154 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 155 class Type_LiftN (n::Peano) ty tys where
 156         type_liftN :: forall (root:: * -> *) h. Proxy n -> ty root h -> tys root h
 157 instance Type_LiftN 'Zero curr curr where
 158         type_liftN _ = id
 159 instance Type_LiftN 'Zero curr (Type_Alt curr next) where
 160         type_liftN _ = Type_Alt_Curr
 161 instance
 162  Type_LiftN n other next =>
 163  Type_LiftN ('Succ n) other (Type_Alt curr next) where
 164         type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy n)
 165
 166 -- | Convenient wrapper around 'type_liftN',
 167 -- passing it the 'Peano' number from 'Peano_of_Type'.
 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_Alt_Curr' and 'Type_Alt_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_Alt curr next) where
 187         type_unliftN _ (Type_Alt_Curr x) = Just x
 188         type_unliftN _ (Type_Alt_Next _) = Nothing
 189 instance
 190  Type_UnliftN n other next =>
 191  Type_UnliftN ('Succ n) other (Type_Alt curr next) where
 192         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy n) x
 193         type_unliftN _ (Type_Alt_Curr _) = Nothing
 194
 195 -- | Convenient wrapper around 'type_unliftN',
 196 -- passing it the 'Peano' number from 'Peano_of_Type'.
 197 type_unlift
 198  :: forall ty tys (root:: * -> *) h.
 199  Type_Unlift ty tys =>
 200  tys root h -> Maybe (ty root h)
 201 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 202
 203 -- * Type family 'Is_Last_Type'
 204 -- | Return whether a given type is the last one in a given type stack.
 205 --
 206 -- NOTE: each type parser uses this type family
 207 -- when it encounters unsupported syntax:
 208 -- to know if it is the last type parser component that will be tried
 209 -- (and thus return 'Error_Type_Unsupported')
 210 -- or if some other type parser component shall be tried
 211 -- (and thus return 'Error_Type_Unsupported_here',
 212 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 213 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 214         Is_Last_Type ty ty                               = 'True
 215         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 216         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 217         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 218
 219 -- * Type 'Error_Type_Alt'
 220 -- | Error type making an alternative between two error types.
 221 data Error_Type_Alt curr next
 222  =   Error_Type_Alt_Curr curr
 223  |   Error_Type_Alt_Next next
 224  deriving (Eq, Show)
 225
 226 -- ** Type 'Error_Type_Lift'
 227 type Error_Type_Lift err errs
 228  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 229
 230 -- *** Type 'Peano_of_Error_Type'
 231 -- | Return a 'Peano' number derived from the location
 232 -- of a given error type within a given error type stack.
 233 type family Peano_of_Error_Type (err:: *) (errs:: *) :: Peano where
 234         Peano_of_Error_Type err err                           = 'Zero
 235         Peano_of_Error_Type err (Error_Type_Alt err next)    = 'Zero
 236         Peano_of_Error_Type other (Error_Type_Alt curr next) = 'Succ (Peano_of_Error_Type other next)
 237
 238 -- *** Class 'Error_Type_LiftN'
 239 -- | Lift a given error type to the top of a given error type stack including it,
 240 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 241 class Error_Type_LiftN (n::Peano) err errs where
 242         error_type_liftN :: Proxy n -> err -> errs
 243 instance Error_Type_LiftN 'Zero curr curr where
 244         error_type_liftN _ = id
 245 instance Error_Type_LiftN 'Zero curr (Error_Type_Alt curr next) where
 246         error_type_liftN _ = Error_Type_Alt_Curr
 247 instance
 248  Error_Type_LiftN n other next =>
 249  Error_Type_LiftN ('Succ n) other (Error_Type_Alt curr next) where
 250         error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy n)
 251
 252 -- | Convenient wrapper around 'error_type_unliftN',
 253 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 254 error_type_lift
 255  :: forall err errs.
 256  Error_Type_Lift err errs =>
 257  err -> errs
 258 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 259
 260 -- ** Type 'Error_Type_Unlift'
 261 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 262 type Error_Type_Unlift ty tys
 263  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 264
 265 -- | Convenient wrapper around 'error_type_unliftN',
 266 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 267 error_type_unlift
 268  :: forall ty tys.
 269  Error_Type_Unlift ty tys =>
 270  tys -> Maybe ty
 271 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 272
 273 -- *** Class 'Error_Type_UnliftN'
 274 -- | Try to unlift a given type error out of a given type error stack including it,
 275 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 276 class Error_Type_UnliftN (n::Peano) ty tys where
 277         error_type_unliftN :: Proxy n -> tys -> Maybe ty
 278 instance Error_Type_UnliftN 'Zero curr curr where
 279         error_type_unliftN _ = Just
 280 instance Error_Type_UnliftN 'Zero curr (Error_Type_Alt curr next) where
 281         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 282         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 283 instance
 284  Error_Type_UnliftN n other next =>
 285  Error_Type_UnliftN ('Succ n) other (Error_Type_Alt curr next) where
 286         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy n) x
 287         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 288
 289 -- ** Type 'Error_Type_Read'
 290 -- | Common type errors.
 291 data Error_Type ast
 292  =   Error_Type_Unsupported ast
 293  -- ^ Given syntax is supported by none
 294  -- of the type parser components
 295  -- of the type stack.
 296  |   Error_Type_Unsupported_here ast
 297  -- ^ Given syntax not supported by the current type parser component.
 298  deriving (Eq, Show)
 299
 300 -- * Class 'String_from_Type'
 301 -- | Return a 'String' from a type.
 302 class String_from_Type ty where
 303         string_from_type :: ty h -> String
 304
 305 -- * Type 'Exists_Type'
 306
 307 -- | Existential data type to wrap an indexed type.
 308 data Exists_Type ty
 309  = forall h. Exists_Type (ty h)
 310 instance -- Eq
 311  Type_Eq ty =>
 312  Eq (Exists_Type ty) where
 313         Exists_Type xh == Exists_Type yh =
 314                 isJust $ type_eq xh yh
 315 instance -- Show
 316  String_from_Type ty =>
 317  Show (Exists_Type ty) where
 318         show (Exists_Type ty) = string_from_type ty
 319
 320 -- * Type 'Exists_Type_and_Repr'
 321 data Exists_Type_and_Repr ty repr
 322  =   forall h.
 323      Exists_Type_and_Repr (ty h) (repr h)
 324
 325 -- * Type family 'HBool'
 326 -- | Host-type equality.
 327 type family HEq x y :: Bool where
 328         HEq x x = 'True
 329         HEq x y = 'False
 330 -- ** Type 'HBool'
 331 -- | Boolean singleton.
 332 data HBool b where
 333         HTrue  :: HBool 'True
 334         HFalse :: HBool 'False
 335 -- ** Class 'Implicit_HBool'
 336 -- | Construct a host-term boolean singleton from a host-type boolean.
 337 class    Implicit_HBool b      where hbool :: HBool b
 338 instance Implicit_HBool 'True  where hbool = HTrue
 339 instance Implicit_HBool 'False where hbool = HFalse