Language/LOL/Symantic/Type/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE KindSignatures #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.LOL.Symantic.Type.Common where
  14
  15 import Data.Maybe (isJust)
  16 import Data.Peano
  17 import Data.Proxy
  18 import Data.Type.Equality ((:~:))
  19
  20 -- * Class 'Type_Eq'
  21
  22 -- | Test two types for equality,
  23 -- returning an Haskell type-level proof
  24 -- of the equality when it holds.
  25 class Type_Eq ty where
  26         type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  27
  28 -- * Class 'Type_from'
  29 -- | Parse some @ast@ data into a 'Root_of_Type',
  30 -- or return 'Nothing' if the @ast@ value is not supported
  31 -- or an 'Error_Type' if it is not well-formed.
  32 class Type_Eq ty =>
  33       Type_from ast (ty:: * -> *) where
  34         type_from
  35          :: Proxy ty
  36          -> ast
  37          -> (forall h. Root_of_Type ty h
  38                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  39          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  40
  41 -- ** Type family 'Root_of_Type'
  42 -- | Return the root type of a type.
  43 type family Root_of_Type (ty:: * -> *) :: * -> *
  44
  45 -- ** Type family 'Error_of_Type'
  46 -- | Return the error type of a type.
  47 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
  48
  49 -- * Type 'Type_Root'
  50 -- | The root type, passing itself as parameter to the given type.
  51 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  52  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  53 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  54 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
  55 type instance Error_of_Type ast (Type_Root ty)
  56  = Error_Type_Cons (Error_Type ast)
  57                    (Error_of_Type ast (ty (Type_Root ty)))
  58  -- NOTE: require UndecidableInstances.
  59 instance -- Type_Eq
  60  Type_Eq (ty (Type_Root ty)) =>
  61  Type_Eq (Type_Root ty) where
  62         type_eq (Type_Root x) (Type_Root y) = x `type_eq` y
  63 instance -- Eq
  64  Type_Eq (Type_Root ty) =>
  65  Eq (Type_Root ty h) where
  66         x == y = isJust $ type_eq x y
  67 instance -- Type_from
  68  ( Type_Eq (Type_Root ty)
  69  , Type_from ast (ty (Type_Root ty))
  70  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  71  ) => Type_from ast (Type_Root ty) where
  72         type_from _px_ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
  73 instance -- String_from_Type
  74  String_from_Type (ty (Type_Root ty)) =>
  75  String_from_Type (Type_Root ty) where
  76         string_from_type (Type_Root ty) = string_from_type ty
  77 instance -- Show
  78  String_from_Type (Type_Root ty) =>
  79  Show (Type_Root ty h) where
  80         show = string_from_type
  81
  82 -- ** Class 'Type_Root_Lift'
  83 -- | Lift a given type to a given root type.
  84 class Type_Root_Lift ty root where
  85         type_root_lift :: forall h. ty root h -> root h
  86 instance
  87  Type_Lift ty root =>
  88  Type_Root_Lift ty (Type_Root root) where
  89         type_root_lift = Type_Root . type_lift
  90
  91 -- * Type 'Type_Cons'
  92 -- | Combine two types into one.
  93 data Type_Cons curr next (root:: * -> *) h
  94  =   Type_Curr (curr root h)
  95  |   Type_Next (next root h)
  96 type instance Root_of_Type (Type_Cons curr next root) = root
  97 type instance Error_of_Type ast (Type_Cons curr next root)
  98  = Error_Type_Cons (Error_of_Type ast (curr root))
  99                    (Error_of_Type ast (next root))
 100 instance -- Type_Eq
 101  ( Type_Eq (curr root)
 102  , Type_Eq (next root)
 103  ) => Type_Eq (Type_Cons curr next root) where
 104         type_eq (Type_Curr x) (Type_Curr y) = x `type_eq` y
 105         type_eq (Type_Next x) (Type_Next y) = x `type_eq` y
 106         type_eq _ _ = Nothing
 107 instance -- Eq
 108  ( Type_Eq (curr root)
 109  , Type_Eq (next root)
 110  ) => Eq (Type_Cons curr next root h) where
 111         x == y = isJust $ type_eq x y
 112 instance -- Type_from
 113  ( Type_Eq (curr root)
 114  , Type_from ast (curr root)
 115  , Type_from ast (next root)
 116  , Root_of_Type (curr root) ~ root
 117  , Root_of_Type (next root) ~ root
 118  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 119  ) => Type_from ast (Type_Cons curr next root) where
 120         type_from _px_ty ast k =
 121                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 122                  Right ret -> ret
 123                  Left err ->
 124                         case error_type_unlift err of
 125                          Just (Error_Type_Unsupported (_::ast)) -> type_from (Proxy::Proxy (next root)) ast k
 126                          _ -> Left err
 127 instance -- String_from_Type
 128  ( String_from_Type (curr root)
 129  , String_from_Type (next root)
 130  ) => String_from_Type (Type_Cons curr next root) where
 131         string_from_type (Type_Curr t) = string_from_type t
 132         string_from_type (Type_Next t) = string_from_type t
 133
 134 -- ** Type 'Type_Lift'
 135 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 136 type Type_Lift ty tys
 137  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 138
 139 -- *** Type 'Peano_of_Type'
 140 -- | Return a 'Peano' number derived from the location
 141 -- of a given type within a given type stack.
 142 type family Peano_of_Type
 143  (ty::  (* -> *) -> * -> *)
 144  (tys:: (* -> *) -> * -> *) :: Peano where
 145         Peano_of_Type ty ty                       = 'Zero
 146         Peano_of_Type ty (Type_Cons ty next)      = 'Zero
 147         Peano_of_Type other (Type_Cons curr next) = 'Succ (Peano_of_Type other next)
 148
 149 -- *** Class 'Type_LiftN'
 150 -- | Lift a given type to the top of a given type stack including it,
 151 -- by constructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 152 class Type_LiftN (n::Peano) ty tys where
 153         type_liftN :: forall (root:: * -> *) h. Proxy n -> ty root h -> tys root h
 154 instance Type_LiftN 'Zero curr curr where
 155         type_liftN _ = id
 156 instance Type_LiftN 'Zero curr (Type_Cons curr next) where
 157         type_liftN _ = Type_Curr
 158 instance
 159  Type_LiftN n other next =>
 160  Type_LiftN ('Succ n) other (Type_Cons curr next) where
 161         type_liftN _ = Type_Next . type_liftN (Proxy::Proxy n)
 162
 163 -- | Convenient wrapper around 'type_liftN',
 164 -- passing it the 'Peano' number from 'Peano_of_Type',
 165 -- used to avoid @OverlappingInstances@.
 166 type_lift
 167  :: forall ty tys (root:: * -> *) h.
 168  Type_Lift ty tys =>
 169  ty root h -> tys root h
 170 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 171
 172 -- ** Type 'Type_Unlift'
 173 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 174 type Type_Unlift ty tys
 175  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 176
 177 -- *** Class 'Type_UnliftN'
 178 -- | Try to unlift a given type out of a given type stack including it,
 179 -- by deconstructing the appropriate sequence of 'Type_Curr' and 'Type_Next'.
 180 class Type_UnliftN (n::Peano) ty tys where
 181         type_unliftN :: forall (root:: * -> *) h. Proxy n -> tys root h -> Maybe (ty root h)
 182 instance Type_UnliftN 'Zero curr curr where
 183         type_unliftN _ = Just
 184 instance Type_UnliftN 'Zero curr (Type_Cons curr next) where
 185         type_unliftN _ (Type_Curr x) = Just x
 186         type_unliftN _ (Type_Next _) = Nothing
 187 instance
 188  Type_UnliftN n other next =>
 189  Type_UnliftN ('Succ n) other (Type_Cons curr next) where
 190         type_unliftN _ (Type_Next x) = type_unliftN (Proxy::Proxy n) x
 191         type_unliftN _ (Type_Curr _) = Nothing
 192
 193 -- | Convenient wrapper around 'type_unliftN',
 194 -- passing it the 'Peano' number from 'Peano_of_Type',
 195 -- used to avoid @OverlappingInstances@.
 196 type_unlift
 197  :: forall ty tys (root:: * -> *) h.
 198  Type_Unlift ty tys =>
 199  tys root h -> Maybe (ty root h)
 200 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 201
 202 -- * Type 'Error_Type_Cons'
 203 -- | Combine two error types into one.
 204 data Error_Type_Cons curr next
 205  =   Error_Type_Curr curr
 206  |   Error_Type_Next next
 207  deriving (Eq, Show)
 208
 209 -- ** Type 'Error_Type_Lift'
 210 type Error_Type_Lift err errs
 211  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 212
 213 -- *** Type 'Peano_of_Error_Type'
 214 -- | Return a 'Peano' number derived from the location
 215 -- of a given error type within a given error type stack.
 216 type family Peano_of_Error_Type (err:: *) (errs:: *) :: Peano where
 217         Peano_of_Error_Type err err                           = 'Zero
 218         Peano_of_Error_Type err (Error_Type_Cons err next)    = 'Zero
 219         Peano_of_Error_Type other (Error_Type_Cons curr next) = 'Succ (Peano_of_Error_Type other next)
 220
 221 -- *** Class 'Error_Type_LiftN'
 222 -- | Lift a given error type to the top of a given error type stack including it,
 223 -- by constructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
 224 class Error_Type_LiftN (n::Peano) err errs where
 225         error_type_liftN :: Proxy n -> err -> errs
 226 instance Error_Type_LiftN 'Zero curr curr where
 227         error_type_liftN _ = id
 228 instance Error_Type_LiftN 'Zero curr (Error_Type_Cons curr next) where
 229         error_type_liftN _ = Error_Type_Curr
 230 instance
 231  Error_Type_LiftN n other next =>
 232  Error_Type_LiftN ('Succ n) other (Error_Type_Cons curr next) where
 233         error_type_liftN _ = Error_Type_Next . error_type_liftN (Proxy::Proxy n)
 234
 235 -- | Convenient wrapper around 'error_type_unliftN',
 236 -- passing it the 'Peano' number from 'Peano_of_Type',
 237 -- used to avoid @OverlappingInstances@.
 238 error_type_lift
 239  :: forall err errs.
 240  Error_Type_Lift err errs =>
 241  err -> errs
 242 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 243
 244 -- ** Type 'Error_Type_Unlift'
 245 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 246 type Error_Type_Unlift ty tys
 247  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 248
 249 -- | Convenient wrapper around 'error_type_unliftN',
 250 -- passing it the 'Peano' number from 'Peano_of_Error_Type',
 251 -- used to avoid @OverlappingInstances@.
 252 error_type_unlift
 253  :: forall ty tys.
 254  Error_Type_Unlift ty tys =>
 255  tys -> Maybe ty
 256 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 257
 258 -- *** Class 'Error_Type_UnliftN'
 259 -- | Try to unlift a given type error out of a given type error stack including it,
 260 -- by deconstructing the appropriate sequence of 'Error_Type_Curr' and 'Error_Type_Next'.
 261 class Error_Type_UnliftN (n::Peano) ty tys where
 262         error_type_unliftN :: Proxy n -> tys -> Maybe ty
 263 instance Error_Type_UnliftN 'Zero curr curr where
 264         error_type_unliftN _ = Just
 265 instance Error_Type_UnliftN 'Zero curr (Error_Type_Cons curr next) where
 266         error_type_unliftN _ (Error_Type_Curr x) = Just x
 267         error_type_unliftN _ (Error_Type_Next _) = Nothing
 268 instance
 269  Error_Type_UnliftN n other next =>
 270  Error_Type_UnliftN ('Succ n) other (Error_Type_Cons curr next) where
 271         error_type_unliftN _ (Error_Type_Next x) = error_type_unliftN (Proxy::Proxy n) x
 272         error_type_unliftN _ (Error_Type_Curr _) = Nothing
 273
 274 -- ** Type 'Error_Type_Read'
 275 -- | Common type errors.
 276 data Error_Type ast
 277  =   Error_Type_Unsupported ast
 278  deriving (Eq, Show)
 279
 280 -- * Class 'String_from_Type'
 281 -- | Return a 'String' from a type.
 282 class String_from_Type ty where
 283         string_from_type :: ty h -> String
 284
 285 -- * Type 'Exists_Type'
 286
 287 -- | Existential data type to wrap an indexed type.
 288 data Exists_Type ty
 289  = forall h. Exists_Type (ty h)
 290 instance -- Eq
 291  Type_Eq ty =>
 292  Eq (Exists_Type ty) where
 293         Exists_Type xh == Exists_Type yh =
 294                 isJust $ type_eq xh yh
 295 instance -- Show
 296  String_from_Type ty =>
 297  Show (Exists_Type ty) where
 298         show (Exists_Type ty) = string_from_type ty
 299
 300 -- * Type 'Exists_Type_and_Repr'
 301 data Exists_Type_and_Repr ty repr
 302  =   forall h.
 303      Exists_Type_and_Repr (ty h) (repr h)