{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -- | Expression for /lambda abstraction/s -- in /Higher-Order Abstract Syntax/ (HOAS). module Language.LOL.Symantic.Expr.Lambda where import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Data.Text (Text) import Language.LOL.Symantic.Type import Language.LOL.Symantic.Expr.Common import Language.LOL.Symantic.Repr.Dup import Language.LOL.Symantic.Trans.Common -- * Class 'Sym_Lambda' -- | Symantic. -- -- NOTE: argument @arg@ and result @res@ of 'Lambda' -- wrapped inside 'lam': to control the calling -- in the 'Repr_Host' instance. -- -- NOTE: the default definitions supplied for: -- 'app', 'inline', 'val' and 'lazy' -- are there to avoid boilerplate code -- when writting 'Trans' instances which -- do not need to alterate those methods. class (lam ~ Lambda_from_Repr repr) => Sym_Lambda lam repr where -- | This type constructor is used like -- the functional dependency: @repr -> lam@ -- (ie. knowing @repr@ one can determine @lam@) -- in order to avoid to introduce a 'Proxy' @lam@ -- in 'let_inline', 'let_val' and 'let_lazy'. -- -- Distinguishing between @lam@ and @repr@ is used to maintain -- the universal polymorphism of @repr@ in 'Expr_from', -- the downside with this however is that -- to be an instance of 'Sym_Lambda' for all @lam@, -- the @repr@ type of an interpreter -- has to be parameterized by @lam@, -- even though it does not actually need @lam@ to do its work. -- -- Basically this means having sometimes to add a type annotation -- to the interpreter call to specify @lam@. type Lambda_from_Repr repr :: {-lam-}(* -> *) -- | Lambda application. app :: repr (Lambda lam arg res) -> repr arg -> repr res -- | /Call-by-name/ lambda. inline :: (repr arg -> repr res) -> repr (Lambda lam arg res) -- | /Call-by-value/ lambda. val :: (repr arg -> repr res) -> repr (Lambda lam arg res) -- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what. lazy :: (repr arg -> repr res) -> repr (Lambda lam arg res) default app :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res) default val :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res) default lazy :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res) app f x = trans_lift $ trans_apply f `app` trans_apply x inline f = trans_lift $ inline $ trans_apply . f . trans_lift val f = trans_lift $ val $ trans_apply . f . trans_lift lazy f = trans_lift $ lazy $ trans_apply . f . trans_lift -- | Convenient 'inline' wrapper. let_inline :: Sym_Lambda lam repr => repr var -> (repr var -> repr res) -> repr res let_inline x y = inline y `app` x -- | Convenient 'val' wrapper. let_val :: Sym_Lambda lam repr => repr var -> (repr var -> repr res) -> repr res let_val x y = val y `app` x -- | Convenient 'lazy' wrapper. let_lazy :: Sym_Lambda lam repr => repr var -> (repr var -> repr res) -> repr res let_lazy x y = lazy y `app` x infixl 5 `app` instance -- Sym_Lambda Dup ( Sym_Lambda lam r1 , Sym_Lambda lam r2 ) => Sym_Lambda lam (Dup r1 r2) where type Lambda_from_Repr (Dup r1 r2) = Lambda_from_Repr r1 app (f1 `Dup` f2) (x1 `Dup` x2) = app f1 x1 `Dup` app f2 x2 inline f = dup1 (inline f) `Dup` dup2 (inline f) val f = dup1 (val f) `Dup` dup2 (val f) lazy f = dup1 (lazy f) `Dup` dup2 (lazy f) -- * Type 'Expr_Lambda' -- | Expression. data Expr_Lambda (lam:: * -> *) (root:: *) type instance Root_of_Expr (Expr_Lambda lam root) = root type instance Type_of_Expr (Expr_Lambda lam root) = Type_Fun lam type instance Sym_of_Expr (Expr_Lambda lam root) repr = Sym_Lambda lam repr type instance Error_of_Expr ast (Expr_Lambda lam root) = Error_Expr_Lambda ast var_from :: forall ast lam root hs ret. ( Type_from ast (Type_Root_of_Expr root) , Error_Expr_Lift (Error_Expr_Lambda ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => Text -> Expr_From ast (Expr_Lambda lam root) hs ret var_from name _px_ex ast = go where go :: forall ex hs'. (ex ~ (Expr_Lambda lam root)) => Context (Lambda_Var (Type_Root_of_Expr ex)) hs' -> ( forall h. Type_Root_of_Expr ex h -> Forall_Repr_with_Context ex hs' h -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret ) -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret go c k' = case c of Context_Empty -> Left $ error_expr_lift $ Error_Expr_Lambda_Var_unbound name ast Lambda_Var n ty `Context_Next` _ | n == name -> k' ty $ Forall_Repr_with_Context $ \(repr `Context_Next` _) -> repr _ `Context_Next` ctx' -> go ctx' $ \ty (Forall_Repr_with_Context repr) -> k' ty $ Forall_Repr_with_Context $ \(_ `Context_Next` c') -> repr c' app_from :: forall ty ast lam root hs ret. ( ty ~ Type_Root_of_Expr root , Type_from ast ty , Expr_from ast root , Type_Root_Lift (Type_Fun lam) ty , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Type_Unlift (Type_Fun lam) (Type_of_Expr root) , Root_of_Expr root ~ root ) => ast -> ast -> Expr_From ast (Expr_Lambda lam root) hs ret app_from ast_lam ast_arg_actual px_ex ast ctx k = expr_from (Proxy::Proxy root) ast_lam ctx $ \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) -> expr_from (Proxy::Proxy root) ast_arg_actual ctx $ \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual) (Forall_Repr_with_Context arg_actual) -> case type_unlift $ unType_Root ty_lam of Nothing -> Left $ error_expr px_ex $ Error_Expr_Type_mismatch ast (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero) :: Type_Root_of_Expr (Expr_Lambda lam root) (lam Zero -> lam (Succ Zero)))) (Exists_Type ty_lam) Just (ty_arg_expected `Type_Fun` ty_res :: Type_Fun lam (Type_Root_of_Expr root) h_lam) -> when_type_eq px_ex ast ty_arg_expected ty_arg_actual $ \Refl -> k ty_res $ Forall_Repr_with_Context $ \c -> lam c `app` arg_actual c lam_from :: forall ty ast lam root hs ret. ( ty ~ Type_Root_of_Expr root , Type_from ast ty , Expr_from ast root , Type_Root_Lift (Type_Fun lam) ty , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => (forall repr arg res . Sym_Lambda lam repr => (repr arg -> repr res) -> repr (Lambda lam arg res)) -> Text -> ast -> ast -> Expr_From ast (Expr_Lambda lam root) hs ret lam_from lam name ast_ty_arg ast_body px_ex ast ctx k = case type_from (Proxy::Proxy (Type_Root_of_Expr root)) ast_ty_arg (Right . Exists_Type) of Left err -> Left $ error_expr px_ex $ Error_Expr_Type err ast Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) -> expr_from (Proxy::Proxy root) ast_body (Lambda_Var name ty_arg `Context_Next` ctx) $ \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) -> k (ty_arg `type_fun` ty_res :: Root_of_Type (Type_Root_of_Expr root) (Lambda lam h_arg h_res)) $ Forall_Repr_with_Context $ \c -> lam $ \arg -> res (arg `Context_Next` c) let_from :: forall ty ast lam root hs ret. ( ty ~ Type_Root_of_Expr root , Type_from ast ty , Expr_from ast root , Type_Root_Lift (Type_Fun lam) ty , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => (forall repr var res. Sym_Lambda lam repr => repr var -> (repr var -> repr res) -> repr res) -> Text -> ast -> ast -> Expr_From ast (Expr_Lambda lam root) hs ret let_from let_ name ast_var ast_body _px_ex _ast ctx k = expr_from (Proxy::Proxy root) ast_var ctx $ \(ty_var::Type_Root_of_Expr root h_var) (Forall_Repr_with_Context var) -> expr_from (Proxy::Proxy root) ast_body (Lambda_Var name ty_var `Context_Next` ctx) $ \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) -> k ty_res $ Forall_Repr_with_Context $ \c -> let_ (var c) $ \arg -> res (arg `Context_Next` c) -- * Type 'Error_Expr_Lambda' data Error_Expr_Lambda ast = Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast deriving (Eq, Show)