Language/Symantic/Expr/Lambda.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 -- | Expression for /lambda abstraction/s
  11 -- in /Higher-Order Abstract Syntax/ (HOAS).
  12 module Language.Symantic.Expr.Lambda where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Data.Text (Text)
  17
  18 import Language.Symantic.Type
  19 import Language.Symantic.Expr.Root
  20 import Language.Symantic.Expr.Error
  21 import Language.Symantic.Expr.From
  22 import Language.Symantic.Trans.Common
  23
  24 -- * Class 'Lambda_from_Repr'
  25 -- | This type constructor is used like
  26 -- the functional dependency: @repr -> lam@
  27 -- (ie. knowing @repr@ one can determine @lam@)
  28 -- in order to avoid to introduce a 'Proxy' @lam@
  29 -- in 'let_inline', 'let_val' and 'let_lazy'.
  30 --
  31 -- Distinguishing between @lam@ and @repr@ is used to maintain
  32 -- the universal polymorphism of @repr@ in 'Expr_from';
  33 -- a downside of this approach is
  34 -- that to be an instance of 'Sym_Lambda' for all @lam@,
  35 -- the @repr@ type of an interpreter
  36 -- has to be parameterized by @lam@,
  37 -- even when it does not actually need @lam@ to do its work
  38 -- (eg. 'Repr_Text').
  39 --
  40 -- Basically this means having sometimes to add a type annotation
  41 -- to the interpreter call to specify @lam@.
  42 --
  43 -- FIXME: 'lazy' requires @lam@ to contain 'IO',
  44 -- which is not escapable (there is no safe function: @IO a -> a@),
  45 -- this is problematic when writing 'Repr_Host' instances
  46 -- where 'app'lying an object-function on the elements of a 'Functor'
  47 -- return a value wrapped inside @lam@, which is then not unwrappable
  48 -- as needed to write the instance.
  49 -- I think the way to solve this is to require all object-values
  50 -- to be wrapped inside @lam@.
  51 type family Lambda_from_Repr (repr:: * -> *) :: {-lam-}(* -> *)
  52
  53 -- * Class 'Sym_Lambda_App'
  54 -- | Symantic.
  55 class (lam ~ Lambda_from_Repr repr) => Sym_Lambda_App lam repr where
  56         -- | /Lambda application/.
  57         app :: repr (Lambda lam arg res) -> repr arg -> repr res
  58         default app    :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
  59         app  f x = trans_lift $ trans_apply f `app` trans_apply x
  60 infixl 5 `app`
  61 -- * Class 'Sym_Lambda_Inline'
  62 -- | Symantic.
  63 class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Inline lam repr where
  64         -- | /Call-by-name/ /lambda abstraction/.
  65         inline :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  66         default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  67         inline f = trans_lift $ inline $ trans_apply . f . trans_lift
  68
  69         -- | Convenient 'inline' wrapper.
  70         let_inline
  71          :: Sym_Lambda_Inline lam repr
  72          => repr var -> (repr var -> repr res) -> repr res
  73         let_inline x y = inline y `app` x
  74 -- * Class 'Sym_Lambda_Val'
  75 -- | Symantic.
  76 class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Val lam repr where
  77         -- | /Call-by-value/ /lambda abstraction/.
  78         val :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  79         default val :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  80         val f = trans_lift $ val $ trans_apply . f . trans_lift
  81
  82         -- | Convenient 'val' wrapper.
  83         let_val
  84          :: Sym_Lambda_Val lam repr
  85          => repr var -> (repr var -> repr res) -> repr res
  86         let_val x y = val y `app` x
  87 -- * Class 'Sym_Lambda_Lazy'
  88 -- | Symantic.
  89 class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Lazy lam repr where
  90         -- | /Call-by-need/ /lambda abstraction/ (aka. /lazyness/): lazy shares its argument, no matter what.
  91         lazy :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  92         default lazy :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  93         lazy f = trans_lift $ lazy $ trans_apply . f . trans_lift
  94
  95         -- | Convenient 'lazy' wrapper.
  96         let_lazy
  97          :: Sym_Lambda_Lazy lam repr
  98          => repr var -> (repr var -> repr res) -> repr res
  99         let_lazy x y = lazy y `app` x
 100
 101 -- * Type 'Expr_Lambda_App'
 102 -- | Expression.
 103 data Expr_Lambda_App (lam:: * -> *) (root:: *)
 104 type instance Root_of_Expr      (Expr_Lambda_App lam root)      = root
 105 type instance Type_of_Expr      (Expr_Lambda_App lam root)      = Type_Fun lam
 106 type instance Sym_of_Expr       (Expr_Lambda_App lam root) repr = Sym_Lambda_App lam repr
 107 type instance Error_of_Expr ast (Expr_Lambda_App lam root)      = Error_Expr_Lambda ast
 108
 109 -- * Type 'Expr_Lambda_Inline'
 110 -- | Expression.
 111 data Expr_Lambda_Inline (lam:: * -> *) (root:: *)
 112 type instance Root_of_Expr      (Expr_Lambda_Inline lam root)      = root
 113 type instance Type_of_Expr      (Expr_Lambda_Inline lam root)      = No_Type
 114 type instance Sym_of_Expr       (Expr_Lambda_Inline lam root) repr = Sym_Lambda_Inline lam repr
 115 type instance Error_of_Expr ast (Expr_Lambda_Inline lam root)      = No_Error_Expr
 116
 117 -- * Type 'Expr_Lambda_Val'
 118 -- | Expression.
 119 data Expr_Lambda_Val (lam:: * -> *) (root:: *)
 120 type instance Root_of_Expr      (Expr_Lambda_Val lam root)      = root
 121 type instance Type_of_Expr      (Expr_Lambda_Val lam root)      = No_Type
 122 type instance Sym_of_Expr       (Expr_Lambda_Val lam root) repr = Sym_Lambda_Val lam repr
 123 type instance Error_of_Expr ast (Expr_Lambda_Val lam root)      = No_Error_Expr
 124
 125 -- * Type 'Expr_Lambda_Lazy'
 126 -- | Expression.
 127 data Expr_Lambda_Lazy (lam:: * -> *) (root:: *)
 128 type instance Root_of_Expr      (Expr_Lambda_Lazy lam root)      = root
 129 type instance Type_of_Expr      (Expr_Lambda_Lazy lam root)      = No_Type
 130 type instance Sym_of_Expr       (Expr_Lambda_Lazy lam root) repr = Sym_Lambda_Lazy lam repr
 131 type instance Error_of_Expr ast (Expr_Lambda_Lazy lam root)      = No_Error_Expr
 132
 133 -- | Parsing utility to check that the given type is a 'Type_Fun'
 134 -- or raise 'Error_Expr_Type_mismatch'.
 135 check_type_fun
 136  :: forall ast ex root lam ty h ret.
 137  ( root ~ Root_of_Expr ex
 138  , ty ~ Type_Root_of_Expr ex
 139  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 140  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 141  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 142                    (Error_of_Expr ast root)
 143  )
 144  => Proxy ex -> ast -> ty h
 145  -> (Type_Fun lam ty h -> Either (Error_of_Expr ast root) ret)
 146  -> Either (Error_of_Expr ast root) ret
 147 check_type_fun ex ast ty k =
 148         case unlift_type $ unType_Root ty of
 149          Just ty_f -> k ty_f
 150          Nothing -> Left $
 151                 error_expr ex $
 152                 Error_Expr_Type_mismatch ast
 153                  (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 154                  :: Type_Root_of_Expr ex (Lambda lam Var0 Var0)))
 155                  (Exists_Type ty)
 156
 157 -- | Parse a /lambda variable/.
 158 var_from
 159  :: forall ast lam root hs ret.
 160  ( Type_from ast (Type_Root_of_Expr root)
 161  , Lift_Error_Expr (Error_Expr_Lambda ast)
 162                    (Error_of_Expr ast root)
 163  , Root_of_Expr root ~ root
 164  ) => Text -> Expr_From ast (Expr_Lambda_App lam root) hs ret
 165 var_from name _ex ast = go
 166         where
 167         go :: forall ex hs'. (ex ~ (Expr_Lambda_App lam root))
 168          => Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
 169          -> ( forall h. Type_Root_of_Expr ex h
 170             -> Forall_Repr_with_Context ex hs' h
 171             -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 172          ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
 173         go c k' =
 174                 case c of
 175                  Context_Empty -> Left $ lift_error_expr $
 176                         Error_Expr_Lambda_Var_unbound name ast
 177                  Lambda_Var n ty `Context_Next` _ | n == name ->
 178                         k' ty $ Forall_Repr_with_Context $
 179                          \(repr `Context_Next` _) -> repr
 180                  _ `Context_Next` ctx' ->
 181                         go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 182                                 k' ty $ Forall_Repr_with_Context $
 183                                  \(_ `Context_Next` c') -> repr c'
 184
 185 -- | Parse 'app'.
 186 app_from
 187  :: forall ty ast lam root hs ret.
 188  ( ty ~ Type_Root_of_Expr root
 189  , Type_from ast ty
 190  , Eq_Type ty
 191  , Expr_from ast root
 192  , Lift_Type_Root (Type_Fun lam) ty
 193  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 194                    (Error_of_Expr ast root)
 195  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 196  , Root_of_Expr root ~ root
 197  ) => ast -> ast
 198  -> Expr_From ast (Expr_Lambda_App lam root) hs ret
 199 app_from ast_lam ast_arg_actual ex ast ctx k =
 200         expr_from (Proxy::Proxy root) ast_lam ctx $
 201          \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) ->
 202         expr_from (Proxy::Proxy root) ast_arg_actual ctx $
 203          \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual)
 204           (Forall_Repr_with_Context arg_actual) ->
 205                 case unlift_type $ unType_Root ty_lam of
 206                  Nothing -> Left $
 207                         error_expr ex $
 208                         Error_Expr_Type_mismatch ast
 209                          (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 210                          :: Type_Root_of_Expr (Expr_Lambda_App lam root) (Lambda lam Var0 Var0)))
 211                          (Exists_Type ty_lam)
 212                  Just (Type_Type2 Proxy ty_arg_expected ty_res
 213                   :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
 214                         check_eq_type ex ast
 215                          ty_arg_expected ty_arg_actual $ \Refl ->
 216                                 k ty_res $ Forall_Repr_with_Context $
 217                                  \c -> lam c `app` arg_actual c
 218
 219 -- | Parse given /lambda abstraction/.
 220 lam_from
 221  :: forall ty ast (lam:: * -> *) root hs ret ex.
 222  ( ty ~ Type_Root_of_Expr root
 223  , root ~ Root_of_Expr ex
 224  , root ~ Root_of_Expr root
 225  , Type_from ast ty
 226  , Expr_from ast root
 227  , Lift_Type_Root (Type_Fun lam) ty
 228  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 229                    (Error_of_Expr ast root)
 230  ) => Proxy lam
 231  -> (forall repr arg res
 232       . Sym_of_Expr ex repr
 233       => (repr arg -> repr res)
 234       -> repr (Lambda lam arg res))
 235  -> Text -> ast -> ast
 236  -> Expr_From ast ex hs ret
 237 lam_from _ lam name ast_ty_arg ast_body ex ast ctx k =
 238         case type_from
 239          (Proxy::Proxy (Type_Root_of_Expr root))
 240          ast_ty_arg (Right . Exists_Type) of
 241          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 242          Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
 243                 expr_from (Proxy::Proxy root) ast_body
 244                  (Lambda_Var name ty_arg `Context_Next` ctx) $
 245                  \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
 246                         k (ty_arg `type_fun` ty_res
 247                          :: Root_of_Type (Type_Root_of_Expr root)
 248                                          (Lambda lam h_arg h_res)) $
 249                         Forall_Repr_with_Context $
 250                          \c -> lam $
 251                                  \arg -> res (arg `Context_Next` c)
 252
 253 -- | Parse given /let/.
 254 let_from
 255  :: forall ty ast root hs ret ex.
 256  ( ty ~ Type_Root_of_Expr root
 257  , root ~ Root_of_Expr ex
 258  , root ~ Root_of_Expr root
 259  , Type_from ast ty
 260  , Expr_from ast root
 261  -- , Lift_Type_Root (Type_Fun lam) ty
 262  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 263                    (Error_of_Expr ast root)
 264  ) => (forall repr var res. Sym_of_Expr ex repr
 265       => repr var -> (repr var -> repr res) -> repr res)
 266  -> Text -> ast -> ast
 267  -> Expr_From ast ex hs ret
 268 let_from let_ name ast_var ast_body _ex _ast ctx k =
 269         expr_from (Proxy::Proxy root) ast_var ctx $
 270          \(ty_var::Type_Root_of_Expr root h_var) (Forall_Repr_with_Context var) ->
 271                 expr_from (Proxy::Proxy root) ast_body
 272                  (Lambda_Var name ty_var `Context_Next` ctx) $
 273                  \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
 274                         k ty_res $ Forall_Repr_with_Context $
 275                          \c -> let_ (var c) $
 276                                  \arg -> res (arg `Context_Next` c)
 277
 278 -- * Type 'Error_Expr_Lambda'
 279 data Error_Expr_Lambda ast
 280  =   Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast
 281  deriving (Eq, Show)