git @ Cat's Eye Technologies Lanthorn / ebada16
Merge branch 'master' into experiment-in-modules Chris Pressey 1 year, 6 months ago
7 changed file(s) with 322 addition(s) and 53 deletion(s). Raw diff Collapse all Expand all
+282
-25
README.md less more
00 Lanthorn
11 ========
22
3 _Proof of Concept_
3 Version 1.0 | _Entry_ @ [catseye.tc](https://catseye.tc/node/Lanthorn)
44 | _See also:_ [Lariat](https://github.com/catseye/Lariat#readme)
5 ∘ [Iphigeneia](https://github.com/catseye/Iphigeneia#readme)
5 * [Iphigeneia](https://github.com/catseye/Iphigeneia#readme)
66
77 When I first came across a explanation of how `letrec` works, it was
88 in terms of updating references: each of the names is bound to a cell,
6161
6262 Our evaluator implements this transformation in the
6363 [Language.Lanthorn.LetRec](src/Language/Lanthorn/LetRec.hs) module.
64 Here is what it produces:
64 Here is what it produces. Note there is a bit of name-mangling
65 added, compared to the hand-written expansion above.
6566
6667 letrec
6768 odd = fun(x) -> if eq(x, 0) then false else even(sub(x, 1))
6970 in
7071 even(6)
7172 => let
72 => odd0 = fun(x, odd1, even1) -> let
73 => odd = fun(x1) -> odd1(x1, odd1, even1)
74 => even = fun(x1) -> even1(x1, odd1, even1)
73 => odd$0 = fun(x, odd$1, even$1) -> let
74 => odd = fun(x$1) -> odd$1(x$1, odd$1, even$1)
75 => even = fun(x$1) -> even$1(x$1, odd$1, even$1)
7576 => in
7677 => if eq(x, 0) then false else even(sub(x, 1))
77 => even0 = fun(x, odd1, even1) -> let
78 => odd = fun(x1) -> odd1(x1, odd1, even1)
79 => even = fun(x1) -> even1(x1, odd1, even1)
78 => even$0 = fun(x, odd$1, even$1) -> let
79 => odd = fun(x$1) -> odd$1(x$1, odd$1, even$1)
80 => even = fun(x$1) -> even$1(x$1, odd$1, even$1)
8081 => in
8182 => if eq(x, 0) then true else odd(sub(x, 1))
82 => odd = fun(x) -> odd0(x, odd0, even0)
83 => even = fun(x) -> even0(x, odd0, even0)
83 => odd = fun(x) -> odd$0(x, odd$0, even$0)
84 => even = fun(x) -> even$0(x, odd$0, even$0)
8485 => in
8586 => even(6)
8687
87 In English, it add a number of extra parameters to each function in
88 In English, it adds a number of extra parameters to each function in
8889 the set of bindings. Specifically, it adds one parameter for each
8990 of the bindings. It then sets up some bindings _inside_ each function
9091 so that the function uses these parameters for the recursive calls
9293 to that the body of the `letrec` sees functions with the original
9394 parameters they had, hiding all these extra parameters.
9495
95 TODO
96 ----
97
98 * The implementation of the transformation isn't fully general yet.
99 It needs to handle `let` inside the definitions and the body of a
100 `let`.
101 * The transformation should make more effort at name mangling
102 hygiene.
103 * The transformation should retain the names of the original
104 arguments of the functions.
105 * There needs to be a test confirming that it can handle multiple
106 arguments in the original functions.
96 Related Work
97 ------------
98
99 [Xavier Pinho](https://github.com/xavierpinho) has written up an
100 alternative way of transforming `letrec` into `let`, using
101 surjective pairing and the Y combinator, in
102 [an issue on the Lanthorn project on GitHub](https://github.com/catseye/Lanthorn/issues/1).
107103
108104 Appendix A
109105 ----------
128124 => in
129125 => zed(a, b)
130126
127 The character `$` may not appear in user-supplied names.
128
129 let
130 a$b = 1
131 in
132 zed(a$b)
133 ?> unexpected "$"
134
131135 Conditional by boolean (`if`).
132136
133137 if gt(a, b) then a else b
190194 let r = fun(x) -> let x = 3 in x in r(10)
191195 ???> Already defined: x
192196
193 `letrec`.
197 #### `letrec`
198
199 Basic usage of `letrec`.
194200
195201 letrec
196202 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
205211 in
206212 evenp(5)
207213 ===> false
214
215 `letrec` nested inside an `if` inside a function definition in an arm of
216 another `letrec`.
217
218 letrec
219 facto = fun(n) -> if eq(n, 1) then 1 else
220 letrec
221 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
222 evenp = fun(x) -> if eq(x, 0) then true else oddp(sub(x, 1))
223 in
224 if oddp(n) then
225 mul(n, facto(sub(n, 1)))
226 else
227 facto(sub(n, 1))
228 in
229 facto(8)
230 ===> 105
231
232 `letrec` nested in the body of another `letrec`.
233
234 letrec
235 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
236 evenp = fun(x) -> if eq(x, 0) then true else oddp(sub(x, 1))
237 in
238 letrec facto = fun(n) ->
239 if eq(n, 1) then
240 1
241 else if oddp(n) then
242 mul(n, facto(sub(n, 1)))
243 else
244 facto(sub(n, 1))
245 in
246 facto(8)
247 ===> 105
248
249 Nested `letrec`, nested right in the arm of another `letrec`. Currently,
250 this is an error, because the inner scope cannot "see" the outer `letrec`.
251 Though I'm not yet convinced of what the most reasonable behaviour is here.
252
253 letrec
254 facto =
255 letrec
256 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
257 evenp = fun(x) -> if eq(x, 0) then true else oddp(sub(x, 1))
258 in
259 fun(n) -> if eq(n, 1) then 1 else
260 if oddp(n) then
261 mul(n, facto(sub(n, 1)))
262 else
263 facto(sub(n, 1))
264 in
265 facto(8)
266 ???> Not in scope: facto
267
268 `letrec` nested inside a function definition inside an arm of a plain `let`.
269
270 let
271 factoo = fun(f, n) ->
272 letrec
273 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
274 evenp = fun(x) -> if eq(x, 0) then true else oddp(sub(x, 1))
275 in
276 if eq(n, 1) then 1 else
277 if oddp(n) then
278 mul(n, f(f, sub(n, 1)))
279 else
280 f(f, sub(n, 1))
281 in
282 factoo(factoo, 7)
283 ===> 105
284
285 `letrec` nested inside body of a plain `let`.
286
287 let
288 factopen = fun(f, n) -> if eq(n, 1) then 1 else mul(n, f(f, sub(n, 1)))
289 target = 7
290 in
291 letrec
292 oddp = fun(x) -> if eq(x, 0) then false else evenp(sub(x, 1))
293 evenp = fun(x) -> if eq(x, 0) then true else oddp(sub(x, 1))
294 in
295 if oddp(target) then factopen(factopen, target) else 0
296 ===> 5040
297
298 `letrec` works on functions that have more than one argument.
299
300 letrec
301 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
302 evensump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then true else oddsump(sub(x, 1), y, z)
303 in
304 evensump(5,3,1)
305 ===> false
306
307 letrec
308 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
309 evensump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then true else oddsump(sub(x, 1), y, z)
310 in
311 evensump(6,3,1)
312 ===> true
313
314 `letrec` works on functions which use different argument names.
315
316 letrec
317 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
318 evensump = fun(p,q,r) -> if eq(add(p, add(q, r)), add(q, r)) then true else oddsump(sub(p, 1), q, r)
319 in
320 evensump(5,3,1)
321 ===> false
322
323 letrec
324 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
325 evensump = fun(p,q,r) -> if eq(add(p, add(q, r)), add(q, r)) then true else oddsump(sub(p, 1), q, r)
326 in
327 evensump(6,3,1)
328 ===> true
329
330 `letrec` works on functions that have differing numbers of arguments.
331
332 letrec
333 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), add(y, z))
334 evensump = fun(p,q) -> if eq(add(p, q), q) then true else oddsump(sub(p, 1), 1, sub(q, 1))
335 in
336 oddsump(5,3,1)
337 ===> true
338
339 ### Properties of the `letrec` transformation
340
341 -> Tests for functionality "Desugar Lanthorn Program"
342
343 When a `letrec` is desugared, the generated functions have argument
344 names that are based on the original argument names. Also, the
345 innermost `let`s bind the plain names to functions with the same arity
346 as the original functions.
347
348 letrec
349 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
350 evensump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then true else oddsump(sub(x, 1), y, z)
351 in
352 evensump(5,3,1)
353 => let
354 => oddsump$0 = fun(x, y, z, oddsump$1, evensump$1) -> let
355 => oddsump = fun(x$1, y$1, z$1) -> oddsump$1(x$1, y$1, z$1, oddsump$1, evensump$1)
356 => evensump = fun(x$1, y$1, z$1) -> evensump$1(x$1, y$1, z$1, oddsump$1, evensump$1)
357 => in
358 => if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), y, z)
359 => evensump$0 = fun(x, y, z, oddsump$1, evensump$1) -> let
360 => oddsump = fun(x$1, y$1, z$1) -> oddsump$1(x$1, y$1, z$1, oddsump$1, evensump$1)
361 => evensump = fun(x$1, y$1, z$1) -> evensump$1(x$1, y$1, z$1, oddsump$1, evensump$1)
362 => in
363 => if eq(add(x, add(y, z)), add(y, z)) then true else oddsump(sub(x, 1), y, z)
364 => oddsump = fun(x, y, z) -> oddsump$0(x, y, z, oddsump$0, evensump$0)
365 => evensump = fun(x, y, z) -> evensump$0(x, y, z, oddsump$0, evensump$0)
366 => in
367 => evensump(5, 3, 1)
368
369 The transformation mangles names that it generates so that they never
370 shadow names that appear in the user's program. (Names containing `$` may
371 not appear in a user-supplied program.)
372
373 let
374 odd0 = fun(a, b, c) -> a
375 in
376 letrec
377 odd = fun(x) -> if eq(x, 0) then false else even(sub(x, 1))
378 even = fun(x) -> if eq(x, 0) then true else odd(sub(x, 1))
379 in
380 even(6)
381 => let
382 => odd0 = fun(a, b, c) -> a
383 => in
384 => let
385 => odd$0 = fun(x, odd$1, even$1) -> let
386 => odd = fun(x$1) -> odd$1(x$1, odd$1, even$1)
387 => even = fun(x$1) -> even$1(x$1, odd$1, even$1)
388 => in
389 => if eq(x, 0) then false else even(sub(x, 1))
390 => even$0 = fun(x, odd$1, even$1) -> let
391 => odd = fun(x$1) -> odd$1(x$1, odd$1, even$1)
392 => even = fun(x$1) -> even$1(x$1, odd$1, even$1)
393 => in
394 => if eq(x, 0) then true else odd(sub(x, 1))
395 => odd = fun(x) -> odd$0(x, odd$0, even$0)
396 => even = fun(x) -> even$0(x, odd$0, even$0)
397 => in
398 => even(6)
399
400 -> Tests for functionality "Evaluate Lanthorn Program"
401
402 letrec
403 odd = fun(x) -> if eq(x, 0) then false else even(sub(x, 1))
404 odd0 = fun(a, b, c) -> a
405 even = fun(x) -> if eq(x, 0) then true else odd(sub(x, 1))
406 in
407 even(6)
408 ===> true
409
410 You might think that instead of mangling names, we could just allow shadowing
411 in the language. But that by itself doesn't solve our problem, since you
412 could still say something like the following. The `letrec` desugaring would
413 have to be more aware of how it constructs names, at any rate, in order to
414 avoid the conflict here. And mangling is the simplest way to do that.
415
416 -> Tests for functionality "Desugar Lanthorn Program"
417
418 letrec
419 odd = fun(x) -> if eq(x, 0) then false else even(sub(x, 1))
420 odd0 = fun(a, b, c) -> a
421 even = fun(x) -> if eq(x, 0) then true else odd(sub(x, 1))
422 in
423 even(6)
424 => let
425 => odd$0 = fun(x, odd$1, odd0$1, even$1) -> let
426 => odd = fun(x$1) -> odd$1(x$1, odd$1, odd0$1, even$1)
427 => odd0 = fun(a$1, b$1, c$1) -> odd0$1(a$1, b$1, c$1, odd$1, odd0$1, even$1)
428 => even = fun(x$1) -> even$1(x$1, odd$1, odd0$1, even$1)
429 => in
430 => if eq(x, 0) then false else even(sub(x, 1))
431 => odd0$0 = fun(a, b, c, odd$1, odd0$1, even$1) -> let
432 => odd = fun(x$1) -> odd$1(x$1, odd$1, odd0$1, even$1)
433 => odd0 = fun(a$1, b$1, c$1) -> odd0$1(a$1, b$1, c$1, odd$1, odd0$1, even$1)
434 => even = fun(x$1) -> even$1(x$1, odd$1, odd0$1, even$1)
435 => in
436 => a
437 => even$0 = fun(x, odd$1, odd0$1, even$1) -> let
438 => odd = fun(x$1) -> odd$1(x$1, odd$1, odd0$1, even$1)
439 => odd0 = fun(a$1, b$1, c$1) -> odd0$1(a$1, b$1, c$1, odd$1, odd0$1, even$1)
440 => even = fun(x$1) -> even$1(x$1, odd$1, odd0$1, even$1)
441 => in
442 => if eq(x, 0) then true else odd(sub(x, 1))
443 => odd = fun(x) -> odd$0(x, odd$0, odd0$0, even$0)
444 => odd0 = fun(a, b, c) -> odd0$0(a, b, c, odd$0, odd0$0, even$0)
445 => even = fun(x) -> even$0(x, odd$0, odd0$0, even$0)
446 => in
447 => even(6)
448
449 -> Tests for functionality "Evaluate Lanthorn Program"
450
451 let
452 odd0 = fun(a, b, c) -> a
453 in
454 letrec
455 odd = fun(x) -> if eq(x, 0) then false else even(sub(x, 1))
456 even = fun(x) -> if eq(x, 0) then true else odd(sub(x, 1))
457 in
458 even(6)
459 ===> true
460
461 Note that there is probably a case where a `letrec` nested another `letrec`, and
462 which shadows variables of the enclosing `letrec`, produces a less readable
463 error message about shadowing, because it mentions the mangled names; but
464 I can live with that for now.
+5
-0
eg/different-arities.lanthorn less more
0 letrec
1 oddsump = fun(x,y,z) -> if eq(add(x, add(y, z)), add(y, z)) then false else evensump(sub(x, 1), add(y, z))
2 evensump = fun(p,q) -> if eq(add(p, q), q) then true else oddsump(sub(p, 1), 1, sub(q, 1))
3 in
4 oddsump(5,3,1)
+2
-1
src/Language/Lanthorn/Env.hs less more
00 module Language.Lanthorn.Env where
11
2 import qualified Data.Map.Strict as Map
2 import qualified Data.Map as Map
33
44 import Language.Lanthorn.Value
55
2121 [
2222 ("true", Boolean True),
2323 ("false", Boolean False),
24 ("add", Function (\[Number a, Number b] -> Number (a + b))),
2425 ("sub", Function (\[Number a, Number b] -> Number (a - b))),
2526 ("mul", Function (\[Number a, Number b] -> Number (a * b))),
2627 ("eq", Function (\[a, b] -> Boolean (a == b)))
+2
-0
src/Language/Lanthorn/Eval.hs less more
5050 in
5151 f actuals
5252 other -> error ("Expected function: " ++ show other)
53
54 evalExpr env other = error ("Unimplemented: " ++ show other)
+21
-16
src/Language/Lanthorn/LetRec.hs less more
66 convert (Apply name args) = Apply name (map (convert) args)
77 convert (LetRec bindings body) = convertToLetStar (convertBindings bindings) (convert body)
88 convert (If c t f) = If (convert c) (convert t) (convert f)
9 convert other = other -- TODO: handle LetStar!
9 convert (LetStar bindings body) = LetStar (convertBindings bindings) (convert body)
10 convert other = other
1011
1112 convertBindings :: [(String, Expr)] -> [(String, Expr)]
1213 convertBindings [] = []
1314 convertBindings ((name, expr):rest) = ((name, (convert expr)):(convertBindings rest))
1415
15 convertArms [] = []
16 convertArms ((ante, cons):rest) = (((convert ante), (convert cons)):(convertArms rest))
17
1816 convertToLetStar :: [(String, Expr)] -> Expr -> Expr
1917 convertToLetStar bindings body =
2018 let
21 injecteds = map (fst) bindings
19 -- For each binding, we need to send down the relevant parts of all
20 -- the bindings in the letrec, so it can compose the recursive call.
21 -- The relevant parts are the *name* of each binding and its *formals*.
22 -- We call such a pair an "injected", for no terribly good reason
23 -- (possibly because it is "injected" into every binding in the letrec).
24 getInjected (name, (Fun formals body)) = (name, formals)
25 injecteds = map (getInjected) bindings
2226 enrichedBindings = createEnrichedBindings bindings injecteds
2327 wrapperBindings = createWrapperBindings bindings injecteds
2428 in
2529 LetStar (enrichedBindings ++ wrapperBindings) body
2630
27 wrapperNameOuter name = name ++ "0" -- TODO: more hygenic!
28 wrapperNameInner name = name ++ "1"
31 wrapperNameOuter name = name ++ "$0"
32 wrapperNameInner name = name ++ "$1"
2933
3034 createEnrichedBindings [] injecteds = []
31 createEnrichedBindings ((name, (Fun formals body)):rest) injecteds =
35 createEnrichedBindings (binding@(name, (Fun formals body)):rest) injecteds =
3236 let
3337 name' = wrapperNameOuter name
34 formals' = formals ++ (map (wrapperNameInner) injecteds)
35 body' = (LetStar (createLocalBindings injecteds injecteds) body)
38 injectedNames = map (fst) injecteds
39 formals' = formals ++ (map (wrapperNameInner) injectedNames)
40 body' = (LetStar (createLocalBindings injecteds injectedNames) body)
3641 expr' = (Fun formals' body')
3742 binding = (name', expr')
3843 in
4146 (binding:createEnrichedBindings rest injecteds)
4247
4348 createLocalBindings [] _ = []
44 createLocalBindings (injected:injecteds) allInjecteds =
49 createLocalBindings (injected@(injectedName, formals):injecteds) allInjectedNames =
4550 let
46 -- FIXME use the real formals of each injected identifier! also, allow shadowing!
47 actuals = map (ValueOf) (["x1"] ++ (map (wrapperNameInner) allInjecteds))
48 binding = (injected, Fun ["x1"] (Apply (wrapperNameInner injected) actuals))
51 formals' = map (wrapperNameInner) formals
52 actuals = map (ValueOf) (formals' ++ (map (wrapperNameInner) allInjectedNames))
53 binding = (injectedName, Fun formals' (Apply (wrapperNameInner injectedName) actuals))
4954 in
50 (binding:createLocalBindings injecteds allInjecteds)
55 (binding:createLocalBindings injecteds allInjectedNames)
5156
5257 createWrapperBindings [] injecteds = []
5358 createWrapperBindings ((name, (Fun formals body)):rest) injecteds =
5459 let
5560 name' = name
56 actuals = map (ValueOf) (formals ++ (map (wrapperNameOuter) injecteds))
61 actuals = map (ValueOf) (formals ++ (map (\x -> wrapperNameOuter $ fst x) injecteds))
5762 expr' = Fun formals (Apply (wrapperNameOuter name) actuals)
5863 binding = (name', expr')
5964 in
+2
-11
test.sh less more
00 #!/bin/sh
11
2 cat >/tmp/fixtures.md <<EOF
3 -> Functionality "Evaluate Lanthorn Program" is implemented by
4 -> shell command "bin/lanthorn eval %(test-body-file)"
2 APPLIANCES="tests/appliances/lanthorn.md"
53
6 -> Functionality "Pretty-print Lanthorn Program" is implemented by
7 -> shell command "bin/lanthorn pretty %(test-body-file)"
8
9 -> Functionality "Desugar Lanthorn Program" is implemented by
10 -> shell command "bin/lanthorn desugar %(test-body-file)"
11 EOF
12
13 falderal /tmp/fixtures.md README.md || exit 1
4 falderal $APPLIANCES README.md || exit 1
+8
-0
tests/appliances/lanthorn.md less more
0 -> Functionality "Evaluate Lanthorn Program" is implemented by
1 -> shell command "bin/lanthorn eval %(test-body-file)"
2
3 -> Functionality "Pretty-print Lanthorn Program" is implemented by
4 -> shell command "bin/lanthorn pretty %(test-body-file)"
5
6 -> Functionality "Desugar Lanthorn Program" is implemented by
7 -> shell command "bin/lanthorn desugar %(test-body-file)"