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