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