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