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
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)
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
26 -- * Class 'Sym_Lambda'
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)
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
41 -- | Convenient 'lam' and '$$' wrapper.
42 let_ :: repr var -> (repr var -> repr res) -> repr res
45 id :: repr a -> repr a
46 id a = (lam Fun.id) $$ a
48 const :: repr a -> repr b -> repr a
49 const a b = lam (lam . Fun.const) $$ a $$ b
51 (#) :: repr (b -> c) -> repr (a -> b) -> repr a -> repr c
52 (#) f g a = f $$ (g $$ a)
54 flip :: repr (a -> b -> c) -> repr b -> repr a -> repr c
55 flip f b a = f $$ a $$ b
59 -- * Type 'Expr_Lambda'
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
67 -- | Parsing utility to check that the given type is a 'Type_Fun'
68 -- or raise 'Error_Expr_Type_mismatch'.
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)
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
86 Error_Expr_Type_mismatch ast
87 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
88 :: ty ((->) Var0 Var0)))
91 -- | Parse a /lambda variable/.
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
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
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'
121 :: forall ty ast root hs ret.
122 ( ty ~ Type_Root_of_Expr 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
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
142 Error_Expr_Type_mismatch ast
143 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
144 :: ty ((->) Var0 Var0)))
146 Just (Type_Type2 Proxy ty_arg_expected ty_res
147 :: Type_Fun ty h_lam) ->
149 ty_arg_expected ty_arg_actual $ \Refl ->
150 k ty_res $ Forall_Repr_with_Context $
151 \c -> l c $$ arg_actual c
153 -- | Parse given /lambda abstraction/.
155 :: forall ty ast root hs ret.
156 ( ty ~ Type_Root_of_Expr root
157 , root ~ Root_of_Expr 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 =
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 $
178 \arg -> res (arg `Context_Next` c)
180 -- | Parse given /let/.
182 :: forall ty ast root hs ret.
183 ( ty ~ Type_Root_of_Expr root
184 , root ~ Root_of_Expr 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 $
199 \arg -> res (arg `Context_Next` c)
201 -- * Type 'Error_Expr_Lambda'
202 data Error_Expr_Lambda ast
203 = Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast