Language/Symantic/Expr/Lambda.hs

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