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