forked from drspro/metta-wam
-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.hvm
113 lines (102 loc) · 4.54 KB
/
main.hvm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
// The main effects of call/cc are:
// 1. create a "hole" where it was called
// 2. create a function 'k' which fills that hole when applied
// For example, consider the following Scheme expression:
//
// (+ 10 (call/cc (lambda (k) (+ (k 42) 1729))))
//
// To evaluate it, the entire `(call/cc ...)` part is replaced by a hole:
//
// (+ 10 _)
//
// Then, Scheme creates an internal function, `k`, which, when called `(k arg)`,
// will replace the hole `_` by `arg`. That function is sent to the user's
// callback `(lambda (k) ...)`, allowing they to decide when and how to fill
// that hole. In the example above, the user calls `(k 42)`, so the result is:
//
// (+ 10 42)
//
// And the remaining of the expression, `(+ _ 1729)`, will be garbage collected.
//
// This ability can be used for various useful purposes, such as exceptions.
// It's impossible to implement this behavior on the pure lambda calculus. On
// interaction combinators, call/cc can be implemented by manipulating some
// edges. For example, consider the graph below:
//
// result garbage
// | |
// + @
// / \_____, / \________,
// | | _____λ |
// 10 | | | ,--λ <-(very illegal)
// | | + | |
// | | / \ | *
// | | @ 1729 |
// | |_/ \ |
// | 42 |
// | |
// |__________________|
//
// After some reductions, an intermediate result will be:
//
// result garbage
// | |
// [+] [+]
// / \ / \
// 10 42 * 1729
//
// Here, the user-defined callback `(λ (k) (+ (k 42) 1729))` received a
// continuation `k` and applied it to `42`, "filling" the hole `(+ 10 _)`,
// giving us the correct result. We could implement continuations on the HVM by
// including a `call/cc` syntax, and then doing the transformation above when
// converting from text to graphs. Meanwhile, it is possible to implement an
// uglier version of it as a library, using scopeless λs. Here is an example:
// Creates a program capable of performing call/cc.
(CC.lang program) =
let callcc = λcallback (λ$garbage($hole) (callback λ$hole(0)))
let result = (program callcc)
let garbage = $garbage
(Seq garbage result)
// Helper function for strictness annotation
(Seq 0 b) = b
(Seq a b) = b
// Notice the call/cc function receives the user-defined callback. It then gives
// the user an internal function that, when called, will fill the hole, and
// return it on the position where call/cc was called. The value returned by the
// callback itself is then moved to the garbage, which is collected.
// Example usage
Main = (CC.lang λcallcc
(+ 10 (callcc λk(+ (k 42) 1729))))
// The result is `(Pair (Result 52) (Garbage 1729))`, as expected.
// Reference: http://www.madore.org/~david/computers/callcc.html
// -----------------------------------------------------------------------------
// Note: to be really useful, we must also be able to use a continuation more
// than once. For example, consider the following Scheme program:
// > (define k 0)
// > (+ 10 (call/cc (λ (k_) (set! cont k_))))
// > (k 3)
// > (k 4)
// Its result is to output `13` and `14`, which is the continuation filled with
// `3` and `4`. In theory, we should also be able to achieve that on HVM as:
//Main = (CC.lang λcallcc [
//(+ 10 (callcc λ$k (3)))
//($k 3)
//($k 4)
//])
// Notice that, while we're not able to move k_ out of the closure by setting a
// global variable, we can still do it by using scopeless lambdas. Sadly, using
// a global variable like `$k` more than once is not supported by the graph
// builder yet. We can kind of hack our way into having it though:
//Main = (CC.lang λcallcc [
//(+ 10 (callcc λ$k (λfλa(f a a) λ$k0λ$k1(3) $k)))
//($k0 3)
//($k1 4)
//])
// Which correctly computes 13 and 14 by filling the `(+ 10 _)` continuation.
// Note that this is *terribly* ugly as it accumulates results in a list of
// superpositions and the garbage. Of course a proper callcc library would
// support multiple calls, collecting intermediate garbage and results and
// displaying or returning them appropriately. The point of this is to
// illustrate how the ability to "freeze" a "call stack" and instantiate is
// already present on HVM "for free". There is no need to implement anything new
// on the evaluator, and everything can be done as a library with proper syntax.