Language/LOL/Symantic/Expr/Lambda.hs

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