Language/LOL/Symantic/Expr/Lambda.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 -- | Expression for /lambda abstraction/s.
  12 module Language.LOL.Symantic.Expr.Lambda where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16
  17 import Language.LOL.Symantic.AST
  18 import Language.LOL.Symantic.Type
  19 import Language.LOL.Symantic.Expr.Common
  20 import Language.LOL.Symantic.Repr.Dup
  21 import Language.LOL.Symantic.Trans.Common
  22
  23 -- * Class 'Sym_Lambda'
  24
  25 -- | Symantic for /lambda abstraction/
  26 -- in /higher-order abstract syntax/ (HOAS),
  27 -- and with argument @arg@ and result @res@ of 'Lambda'
  28 -- wrapped inside 'lam': to control the calling
  29 -- in the 'Repr_Host' instance.
  30 --
  31 -- NOTE: the default definitions supplied for:
  32 -- 'app', 'inline', 'val' and 'lazy'
  33 -- are there to avoid boilerplate code
  34 -- when writting 'Trans' instances which
  35 -- do not need to alterate those methods.
  36 class (lam ~ Lambda_from_Repr repr) => Sym_Lambda lam repr where
  37         -- | This type constructor is used like
  38         -- the functional dependency: @repr -> lam@
  39         -- (ie. knowing @repr@ one can determine @lam@)
  40         -- in order to avoid to introduce a 'Proxy' @lam@
  41         -- in 'let_inline', 'let_val' and 'let_lazy'.
  42         --
  43         -- Distinguishing between @lam@ and @repr@ is used to maintain
  44         -- the universal polymorphism of @repr@ in 'Expr_from',
  45         -- the downside with this however is that
  46         -- to be an instance of 'Sym_Lambda' for all @lam@,
  47         -- the @repr@ type of an interpreter
  48         -- has to be parameterized by @lam@,
  49         -- even though it does not actually need @lam@ to do its work.
  50         --
  51         -- Basically this means having sometimes to add a type annotation
  52         -- to the interpreter call to specify @lam@.
  53         type Lambda_from_Repr repr :: {-lam-}(* -> *)
  54
  55         -- | Lambda application.
  56         app :: repr (Lambda lam arg res) -> repr arg -> repr res
  57
  58         -- | /Call-by-name/ lambda.
  59         inline :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  60         -- | /Call-by-value/ lambda.
  61         val    :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  62         -- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what.
  63         lazy   :: (repr arg -> repr res) -> repr (Lambda lam arg res)
  64
  65         default app :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
  66         default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  67         default val    :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  68         default lazy   :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
  69         app  f x = trans_lift $ trans_apply f `app` trans_apply x
  70         inline f = trans_lift $ inline $ trans_apply . f . trans_lift
  71         val    f = trans_lift $ val    $ trans_apply . f . trans_lift
  72         lazy   f = trans_lift $ lazy   $ trans_apply . f . trans_lift
  73
  74         -- | Convenient 'inline' wrapper.
  75         let_inline
  76          :: Sym_Lambda lam repr
  77          => repr arg -> (repr arg -> repr res) -> repr res
  78         let_inline x y = inline y `app` x
  79         -- | Convenient 'val' wrapper.
  80         let_val
  81          :: Sym_Lambda lam repr
  82          => repr arg -> (repr arg -> repr res) -> repr res
  83         let_val x y = val y `app` x
  84         -- | Convenient 'lazy' wrapper.
  85         let_lazy
  86          :: Sym_Lambda lam repr
  87          => repr arg -> (repr arg -> repr res) -> repr res
  88         let_lazy x y = lazy y `app` x
  89
  90 infixl 5 `app`
  91
  92 instance -- Sym_Lambda Dup
  93  ( Sym_Lambda lam r1
  94  , Sym_Lambda lam r2
  95  ) => Sym_Lambda lam (Dup r1 r2) where
  96         type Lambda_from_Repr (Dup r1 r2) = Lambda_from_Repr r1
  97         app (f1 `Dup` f2) (x1 `Dup` x2) = app f1 x1 `Dup` app f2 x2
  98         inline f = dup1 (inline f) `Dup` dup2 (inline f)
  99         val    f = dup1 (val f)    `Dup` dup2 (val f)
 100         lazy   f = dup1 (lazy f)   `Dup` dup2 (lazy f)
 101
 102 -- * Type 'Expr_Lambda'
 103 -- | Expression's extension.
 104 data Expr_Lambda (lam:: * -> *) (root:: *)
 105 type instance Root_of_Expr (Expr_Lambda lam root) = root
 106 type instance Type_of_Expr (Expr_Lambda lam root) = Type_Fun lam
 107 type instance Sym_of_Expr (Expr_Lambda lam root) repr = Sym_Lambda lam repr
 108 type instance Error_of_Expr ast (Expr_Lambda lam root)
 109  = Error_Expr_Lambda (Error_of_Type ast (Type_Root_of_Expr root))
 110                      (Type_Root_of_Expr root)
 111                      ast
 112  -- NOTE: require UndecidableInstances.
 113
 114 instance -- Expr_from AST Expr_Lambda
 115  ( Type_from AST (Type_Root_of_Expr root)
 116  , Expr_from AST root
 117
 118  , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
 119  , Error_Type_Lift (Error_Type_Fun AST)
 120                    (Error_of_Type AST (Type_Root_of_Expr root))
 121  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
 122                                       (                   Type_Root_of_Expr root)
 123                                       AST)
 124                    (Error_of_Expr AST root)
 125
 126  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 127
 128  , Root_of_Expr root ~ root
 129  ) => Expr_from AST (Expr_Lambda lam root) where
 130         expr_from _px_ex ctx ast k =
 131                 case ast of
 132                  AST "var" asts ->
 133                         case asts of
 134                          [AST name []] -> go ctx k
 135                                 where
 136                                 go
 137                                  :: forall hs ret
 138                                  . Context (Var root) hs
 139                                  -> ( forall h
 140                                     .  Type_Root_of_Expr root h
 141                                     -> Forall_Repr_with_Context (Expr_Lambda lam root) hs h
 142                                     -> Either (Maybe (Error_of_Expr AST root)) ret )
 143                                  -> Either (Maybe (Error_of_Expr AST root)) ret
 144                                 go c k' =
 145                                         case c of
 146                                          Context_Empty -> Left $ Just $ error_lambda_lift $
 147                                                 Error_Expr_Lambda_Var_unbound name ast
 148                                          Var n ty `Context_Next` _ | n == name ->
 149                                                 k' ty $ Forall_Repr_with_Context $
 150                                                  \(repr `Context_Next` _) -> repr
 151                                          _ `Context_Next` ctx' ->
 152                                                 go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 153                                                         k' ty $ Forall_Repr_with_Context $
 154                                                          \(_ `Context_Next` c') -> repr c'
 155                          _ -> Left $ Just $ error_lambda_lift $
 156                                 Error_Expr_Fun_Wrong_number_of_arguments 1 ast
 157                  AST "app" asts ->
 158                         case asts of
 159                          [ast_lam, ast_arg_actual] ->
 160                                 expr_from (Proxy::Proxy root) ctx ast_lam $
 161                                  \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) ->
 162                                 expr_from (Proxy::Proxy root) ctx ast_arg_actual $
 163                                  \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual)
 164                                   (Forall_Repr_with_Context arg_actual) ->
 165                                         case type_unlift $ unType_Root ty_lam of
 166                                          Just (ty_arg_expected `Type_Fun` ty_res
 167                                           :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
 168                                                 case ty_arg_expected `type_eq` ty_arg_actual of
 169                                                  Just Refl ->
 170                                                         k ty_res $ Forall_Repr_with_Context $
 171                                                          \c -> lam c `app` arg_actual c
 172                                                  Nothing -> Left $ Just $ error_lambda_lift $
 173                                                         Error_Expr_Fun_Argument_mismatch
 174                                                          (Exists_Type ty_arg_expected)
 175                                                          (Exists_Type ty_arg_actual) ast
 176                                          Nothing -> Left $ Just $ error_lambda_lift $
 177                                                 Error_Expr_Lambda_Not_a_lambda ast
 178                          _ -> Left $ Just $ error_lambda_lift $
 179                                 Error_Expr_Type
 180                                  (error_type_lift $
 181                                         Error_Type_Fun_Wrong_number_of_arguments 2 ast
 182                                  ) ast
 183                  AST "inline" asts -> lambda_from asts inline
 184                  AST "val"    asts -> lambda_from asts val
 185                  AST "lazy"   asts -> lambda_from asts lazy
 186                  _ -> Left Nothing
 187                 where
 188                 lambda_from asts
 189                  (lam::forall repr arg res. Sym_Lambda lam repr
 190                      => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
 191                         case asts of
 192                          [AST name [], ast_ty_arg, ast_body] ->
 193                                 case type_from (Proxy::Proxy (Type_Root_of_Expr root)) ast_ty_arg
 194                                  (Right . Exists_Type) of
 195                                  Left Nothing -> Left Nothing
 196                                  Left (Just err) -> Left $ Just $ error_lambda_lift $ Error_Expr_Type err ast
 197                                  Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
 198                                         expr_from (Proxy::Proxy root)
 199                                          (Var name ty_arg `Context_Next` ctx) ast_body $
 200                                          \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
 201                                                 k (ty_arg `type_fun` ty_res
 202                                                  :: Root_of_Type (Type_Root_of_Expr root)
 203                                                                  (Lambda lam h_arg h_res)) $
 204                                                 Forall_Repr_with_Context $
 205                                                  \c -> lam $ \arg -> res (arg `Context_Next` c)
 206                          _ -> Left $ Just $ error_lambda_lift $
 207                                 Error_Expr_Fun_Wrong_number_of_arguments 3 ast
 208                 error_lambda_lift
 209                  :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
 210                  -> Error_of_Expr AST root
 211                 error_lambda_lift = error_expr_lift
 212
 213 -- * Type 'Error_Expr_Lambda'
 214 data Error_Expr_Lambda err_ty ty ast
 215  =   Error_Expr_Lambda_Not_a_lambda ast
 216  |   Error_Expr_Lambda_Var_unbound Var_Name ast
 217  |   Error_Expr_Fun_Wrong_number_of_arguments Int ast
 218  |   Error_Expr_Fun_Argument_mismatch (Exists_Type ty) (Exists_Type ty) ast
 219  |   Error_Expr_Type err_ty ast
 220  deriving (Eq, Show)