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 qualified Data.Function as Fun
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import Data.Text (Text)
  18 import Prelude hiding (const, id)
  19
  20 import Language.Symantic.Type
  21 import Language.Symantic.Expr.Root
  22 import Language.Symantic.Expr.Error
  23 import Language.Symantic.Expr.From
  24 import Language.Symantic.Trans.Common
  25
  26 -- * Class 'Sym_Lambda'
  27 -- | Symantic.
  28 class Sym_Lambda repr where
  29         -- | /Lambda application/.
  30         ($$) :: repr ((->) arg res) -> repr arg -> repr res
  31         default ($$) :: Trans t repr
  32          => t repr ((->) arg res) -> t repr arg -> t repr res
  33         ($$) f x = trans_lift (trans_apply f $$ trans_apply x)
  34
  35         -- | /Lambda abstraction/.
  36         lam :: (repr arg -> repr res) -> repr ((->) arg res)
  37         default lam :: Trans t repr
  38          => (t repr arg -> t repr res) -> t repr ((->) arg res)
  39         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
  40
  41         -- | Convenient 'lam' and '$$' wrapper.
  42         let_ :: repr var -> (repr var -> repr res) -> repr res
  43         let_ x y = lam y $$ x
  44
  45         id :: repr a -> repr a
  46         id a = (lam Fun.id) $$ a
  47
  48         const :: repr a -> repr b -> repr a
  49         const a b = lam (lam . Fun.const) $$ a $$ b
  50
  51         (#) :: repr (b -> c) -> repr (a -> b) -> repr a -> repr c
  52         (#) f g a = f $$ (g $$ a)
  53
  54         flip :: repr (a -> b -> c) -> repr b -> repr a -> repr c
  55         flip f b a = f $$ a $$ b
  56 infixl 0 $$
  57 infixr 9 #
  58
  59 -- * Type 'Expr_Lambda'
  60 -- | Expression.
  61 data Expr_Lambda (root:: *)
  62 type instance Root_of_Expr      (Expr_Lambda root)      = root
  63 type instance Type_of_Expr      (Expr_Lambda root)      = Type_Fun
  64 type instance Sym_of_Expr       (Expr_Lambda root) repr = Sym_Lambda repr
  65 type instance Error_of_Expr ast (Expr_Lambda root)      = Error_Expr_Lambda ast
  66
  67 -- | Parsing utility to check that the given type is a 'Type_Fun'
  68 -- or raise 'Error_Expr_Type_mismatch'.
  69 check_type_fun
  70  :: forall ast ex root ty h ret.
  71  ( root ~ Root_of_Expr ex
  72  , ty ~ Type_Root_of_Expr ex
  73  , Lift_Type   Type_Fun (Type_of_Expr root)
  74  , Unlift_Type Type_Fun (Type_of_Expr root)
  75  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  76                    (Error_of_Expr ast root)
  77  )
  78  => Proxy ex -> ast -> ty h
  79  -> (Type_Fun ty h -> Either (Error_of_Expr ast root) ret)
  80  -> Either (Error_of_Expr ast root) ret
  81 check_type_fun ex ast ty k =
  82         case unlift_type $ unType_Root ty of
  83          Just ty_f -> k ty_f
  84          Nothing -> Left $
  85                 error_expr ex $
  86                 Error_Expr_Type_mismatch ast
  87                  (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
  88                  :: ty ((->) Var0 Var0)))
  89                  (Exists_Type ty)
  90
  91 -- | Parse a /lambda variable/.
  92 var_from
  93  :: forall ast root hs ret.
  94  ( Type_from ast (Type_Root_of_Expr root)
  95  , Lift_Error_Expr (Error_Expr_Lambda ast)
  96                    (Error_of_Expr ast root)
  97  , Root_of_Expr root ~ root
  98  ) => Text -> Expr_From ast (Expr_Lambda root) hs ret
  99 var_from name _ex ast = go
 100         where
 101         go :: forall ex hs'. (ex ~ (Expr_Lambda root))
 102          => Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
 103          -> ( forall h. Type_Root_of_Expr ex h
 104             -> Forall_Repr_with_Context ex hs' h
 105             -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
 106          ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
 107         go c k' =
 108                 case c of
 109                  Context_Empty -> Left $ lift_error_expr $
 110                         Error_Expr_Lambda_Var_unbound name ast
 111                  Lambda_Var n ty `Context_Next` _ | n == name ->
 112                         k' ty $ Forall_Repr_with_Context $
 113                          \(repr `Context_Next` _) -> repr
 114                  _ `Context_Next` ctx' ->
 115                         go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 116                                 k' ty $ Forall_Repr_with_Context $
 117                                  \(_ `Context_Next` c') -> repr c'
 118
 119 -- | Parse 'app'.
 120 app_from
 121  :: forall ty ast root hs ret.
 122  ( ty ~ Type_Root_of_Expr root
 123  , Type_from ast ty
 124  , Eq_Type ty
 125  , Expr_from ast root
 126  , Lift_Type Type_Fun (Type_of_Expr root)
 127  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 128                    (Error_of_Expr ast root)
 129  , Unlift_Type Type_Fun (Type_of_Expr root)
 130  , Root_of_Expr root ~ root
 131  ) => ast -> ast
 132  -> Expr_From ast (Expr_Lambda root) hs ret
 133 app_from ast_lam ast_arg_actual ex ast ctx k =
 134         expr_from (Proxy::Proxy root) ast_lam ctx $
 135          \(ty_lam::ty h_lam) (Forall_Repr_with_Context l) ->
 136         expr_from (Proxy::Proxy root) ast_arg_actual ctx $
 137          \(ty_arg_actual::ty h_arg_actual)
 138           (Forall_Repr_with_Context arg_actual) ->
 139                 case unlift_type $ unType_Root ty_lam of
 140                  Nothing -> Left $
 141                         error_expr ex $
 142                         Error_Expr_Type_mismatch ast
 143                          (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
 144                          :: ty ((->) Var0 Var0)))
 145                          (Exists_Type ty_lam)
 146                  Just (Type_Type2 Proxy ty_arg_expected ty_res
 147                   :: Type_Fun ty h_lam) ->
 148                         check_eq_type ex ast
 149                          ty_arg_expected ty_arg_actual $ \Refl ->
 150                                 k ty_res $ Forall_Repr_with_Context $
 151                                  \c -> l c $$ arg_actual c
 152
 153 -- | Parse given /lambda abstraction/.
 154 lam_from
 155  :: forall ty ast root hs ret.
 156  ( ty ~ Type_Root_of_Expr root
 157  , root ~ Root_of_Expr root
 158  , Type_from ast ty
 159  , Expr_from ast root
 160  , Lift_Type Type_Fun (Type_of_Expr root)
 161  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 162                    (Error_of_Expr ast root)
 163  ) => Text -> ast -> ast
 164  -> Expr_From ast (Expr_Lambda root) hs ret
 165 lam_from name ast_ty_arg ast_body ex ast ctx k =
 166         case type_from
 167          (Proxy::Proxy ty)
 168          ast_ty_arg (Right . Exists_Type) of
 169          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 170          Right (Exists_Type (ty_arg::ty h_arg)) ->
 171                 expr_from (Proxy::Proxy root) ast_body
 172                  (Lambda_Var name ty_arg `Context_Next` ctx) $
 173                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 174                         k (ty_arg `type_fun` ty_res
 175                          :: Root_of_Type ty ((->) h_arg h_res)) $
 176                         Forall_Repr_with_Context $
 177                          \c -> lam $
 178                                  \arg -> res (arg `Context_Next` c)
 179
 180 -- | Parse given /let/.
 181 let_from
 182  :: forall ty ast root hs ret.
 183  ( ty ~ Type_Root_of_Expr root
 184  , root ~ Root_of_Expr root
 185  , Type_from ast ty
 186  , Expr_from ast root
 187  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 188                    (Error_of_Expr ast root)
 189  ) => Text -> ast -> ast
 190  -> Expr_From ast (Expr_Lambda root) hs ret
 191 let_from name ast_var ast_body _ex _ast ctx k =
 192         expr_from (Proxy::Proxy root) ast_var ctx $
 193          \(ty_var::ty h_var) (Forall_Repr_with_Context var) ->
 194                 expr_from (Proxy::Proxy root) ast_body
 195                  (Lambda_Var name ty_var `Context_Next` ctx) $
 196                  \(ty_res::ty h_res) (Forall_Repr_with_Context res) ->
 197                         k ty_res $ Forall_Repr_with_Context $
 198                          \c -> let_ (var c) $
 199                                  \arg -> res (arg `Context_Next` c)
 200
 201 -- * Type 'Error_Expr_Lambda'
 202 data Error_Expr_Lambda ast
 203  =   Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast
 204  deriving (Eq, Show)