Language/Symantic/Expr/Lambda.hs

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