Minor edits.

This commit is contained in:
Simon Forman 2018-06-27 16:31:00 -07:00
parent 4321ea874b
commit 9ee50a6268
9 changed files with 2137 additions and 2127 deletions

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

View File

@ -1,15 +1,11 @@
# Type Inference
This notebook presents a simple type inferencer for Joy code. It can infer the stack effect of most Joy expressions. It built largely by means of existing ideas and research (some of it may be original but I'm not able to say, as I don't fully understand the all of the source material in the depth required to make that call.) A great overview of the existing knowledge is a talk ["Type Inference in Stack-Based Programming Languages"](http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/) given by Rob Kleffner on or about 2017-03-10 as part of a course on the history of programming languages.
This notebook presents a simple type inferencer for Joy code. It can infer the stack effect of most Joy expressions. It's built largely by means of existing ideas and research. (A great overview of the existing knowledge is a talk ["Type Inference in Stack-Based Programming Languages"](http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/) given by Rob Kleffner on or about 2017-03-10 as part of a course on the history of programming languages.)
The notebook starts with a simple inferencer based on the work of Jaanus Pöial which we then progressively elaborate to cover more Joy semantics. Along the way we write a simple "compiler" that emits Python code for what I like to call Yin functions.
The notebook starts with a simple inferencer based on the work of Jaanus Pöial which we then progressively elaborate to cover more Joy semantics. Along the way we write a simple "compiler" that emits Python code for what I like to call Yin functions. (Yin functions are those that only rearrange values in stacks, as opposed to Yang functions that actually work on the values themselves.)
Yin functions are those that only rearrange values in stacks, as opposed to Yang functions that actually work on the values themselves. It's interesting to note that a Joy with *only* stacks (no other kinds of values) can be made and is Turing-complete, therefore all Yang functions are actually Yin functions, and all computation can be performed by manipulations of structures of containers, which is a restatement of the Laws of Form. (Also, this implies that every program can be put into a form such that it can be computed in a single step, although that step may be enormous or unending.)
Although I haven't completed it yet, a Joy based on Laws of Form provides the foundation for a provably correct computing system "down to the metal". This is my original and still primary motivation for developing Joy. (I want a proven-correct Operating System for a swarm of trash-collecting recycler robots. To trust it I have to implementment it myself from first principles, and I'm not smart enough to truly grok the existing literature and software, so I had to go look for and find LoF and Joy. Now that I have the mental tools to build my robot OS I can get down to it.
Anyhow, here's type inference...
## Part I: Pöial's Rules
@ -147,7 +143,7 @@ def poswrd(stack):
This eliminates the internal work of the first version. Because this function only rearranges the stack and doesn't do any actual processing on the stack items themselves all the information needed to implement it is in the stack effect comment.
### Functions on Lists
### Functions on Stacks
These are slightly tricky.
rest ( [1 ...] -- [...] )
@ -345,18 +341,12 @@ def unify(u, v, s=None):
if s is None:
s = {}
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
return False
return s
```
### `update()`
@ -566,9 +556,6 @@ except Exception, e:
print e
```
Cannot unify (1, 2) and (1001, 1002).
#### `unify()` version 2
The problem is that the `unify()` function as written doesn't handle the case when both terms are tuples. We just have to add a clause to deal with this recursively:
@ -581,27 +568,24 @@ def unify(u, v, s=None):
u = update(s, u)
v = update(s, v)
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
if isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != len(v) != 2:
raise ValueError(repr((u, v)))
for uu, vv in zip(u, v):
s = unify(uu, vv, s)
if s == False: # (instead of a substitution dict.)
break
return s
return False
elif isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != 2 or len(v) != 2:
# Not a type error, caller passed in a bad value.
raise ValueError(repr((u, v))) # FIXME this message sucks.
(a, b), (c, d) = u, v
s = unify(a, c, s)
if s != False:
s = unify(b, d, s)
return s
```
@ -1142,7 +1126,7 @@ def delabel(f, seen=None, c=None):
pass
if not isinstance(f, tuple):
seen[f] = f.__class__(c[f.prefix])
seen[f] = f.__class__(c[f.prefix] + 1)
c[f.prefix] += 1
return seen[f]
@ -1157,7 +1141,7 @@ delabel(foo)
(((a0,), (a0, a0)), ((n0, n1), (n2,)))
(((a1,), (a1, a1)), ((n1, n2), (n3,)))
@ -1280,7 +1264,7 @@ for name, stack_effect_comment in sorted(DEFS.items()):
print name, '=', doc_from_stack_effect(*stack_effect_comment)
```
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1297,13 +1281,13 @@ for name, stack_effect_comment in sorted(DEFS.items()):
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
succ = (n1 -- n2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1323,7 +1307,7 @@ C(dup, mul)
((n0,), (n1,))
((n1,), (n2,))
@ -1338,7 +1322,7 @@ F
(((a0, (a1, s0)), a2, a3, a4), ((a3, (a2, s0)),))
(((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
@ -1347,7 +1331,7 @@ F
print doc_from_stack_effect(*F)
```
([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])
([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])
Some otherwise inefficient functions are no longer to be feared. We can also get the effect of combinators in some limited cases.
@ -1364,7 +1348,7 @@ def neato(*funcs):
neato(rollup, swap, rolldown)
```
(a0 a1 a2 -- a1 a0 a2)
(a1 a2 a3 -- a2 a1 a3)
@ -1373,7 +1357,7 @@ neato(rollup, swap, rolldown)
neato(popdd, rolldown, pop)
```
(a0 a1 a2 a3 -- a2 a3)
(a1 a2 a3 a4 -- a3 a4)
@ -1382,7 +1366,7 @@ neato(popdd, rolldown, pop)
neato(rollup, swap)
```
(a0 a1 a2 -- a2 a1 a0)
(a1 a2 a3 -- a3 a2 a1)
#### `compile_()` version 2
@ -1411,9 +1395,9 @@ print compile_('F', F)
```
def F(stack):
"""([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])"""
(a4, (a3, (a2, ((a0, (a1, s0)), stack)))) = stack
return ((a3, (a2, s0)), stack)
"""([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])"""
(a5, (a4, (a3, ((a1, (a2, s1)), stack)))) = stack
return ((a4, (a3, s1)), stack)
But it cannot magically create new functions that involve e.g. math and such. Note that this is *not* a `sqr` function implementation:
@ -1424,9 +1408,9 @@ print compile_('sqr', C(dup, mul))
```
def sqr(stack):
"""(n0 -- n1)"""
(n0, stack) = stack
return (n1, stack)
"""(n1 -- n2)"""
(n1, stack) = stack
return (n2, stack)
(Eventually I should come back around to this becuase it's not tooo difficult to exend this code to be able to compile e.g. `n3 = mul(n1, n2)` for `mul` and insert it in the right place with the right variable names. It requires a little more support from the library functions, in that we need to know to call `mul()` the Python function for `mul` the Joy function, but since *most* of the math functions (at least) are already wrappers it should be straightforward.)
@ -1450,7 +1434,7 @@ for name, stack_effect_comment in sorted(defs().items()):
print name, '=', doc_from_stack_effect(*stack_effect_comment)
```
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
dup = (a1 -- a1 a1)
dupd = (a2 a1 -- a2 a2 a1)
@ -1463,11 +1447,11 @@ for name, stack_effect_comment in sorted(defs().items()):
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1530,7 +1514,7 @@ Let's try `stack∘uncons∘uncons`:
It works.
#### `compose()` version 2
This function has to be modified to use the new datastructures and it is no longer recursive, instead recursion happens as part of unification. Further, the first and second of Pöial's rules are now handled automatically by the unification algorithm.
This function has to be modified to use the new datastructures and it is no longer recursive, instead recursion happens as part of unification. Further, the first and second of Pöial's rules are now handled automatically by the unification algorithm. (One easy way to see this is that now an empty stack effect comment is represented by a `StackJoyType` instance which is not "falsey" and so neither of the first two rules' `if` clauses will ever be `True`. Later on I change the "truthiness" of `StackJoyType` to false to let e.g. `joy.utils.stack.concat` work with our stack effect comment cons-list tuples.)
```python
@ -1567,19 +1551,19 @@ C(stack, uncons)
((a0, s0), (s0, (a0, (a0, s0))))
((a1, s1), (s1, (a1, (a1, s1))))
```python
C(C(stack, uncons), uncons)
reduce(C, (stack, uncons, uncons))
```
((a0, (a1, s0)), (s0, (a1, (a0, (a0, (a1, s0))))))
((a1, (a2, s1)), (s1, (a2, (a1, (a1, (a2, s1))))))
@ -1643,7 +1627,7 @@ for name, stack_effect_comment in sorted(NEW_DEFS.items()):
print name, '=', doc_from_stack_effect(*stack_effect_comment)
```
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1660,15 +1644,15 @@ for name, stack_effect_comment in sorted(NEW_DEFS.items()):
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
stack = (... -- ... [...])
succ = (n1 -- n2)
swaack = ([.1.] -- [.0.])
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1677,18 +1661,18 @@ for name, stack_effect_comment in sorted(NEW_DEFS.items()):
```python
print ; print doc_from_stack_effect(*stack)
print ; print doc_from_stack_effect(*C(stack, uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), cons))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, uncons)))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, cons)))
```
(... -- ... [...])
(... a0 -- ... a0 a0 [...])
(... a1 -- ... a1 a1 [...])
(... a1 a0 -- ... a1 a0 a0 a1 [...])
(... a2 a1 -- ... a2 a1 a1 a2 [...])
(... a0 -- ... a0 [a0 ...])
(... a1 -- ... a1 [a1 ...])
@ -1696,7 +1680,7 @@ print ; print doc_from_stack_effect(*C(C(stack, uncons), cons))
print doc_from_stack_effect(*C(ccons, stack))
```
(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])
(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])
@ -1709,7 +1693,7 @@ Q
((s0, (a0, (a1, s1))), (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1)))
((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
@ -1734,9 +1718,9 @@ print compile_('Q', Q)
```
def Q(stack):
"""(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])"""
(s0, (a0, (a1, s1))) = stack
return (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1))
"""(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])"""
(s1, (a1, (a2, s2))) = stack
return (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2))
@ -1766,7 +1750,7 @@ print doc_from_stack_effect(*enstacken)
print doc_from_stack_effect(*C(cons, unstack))
```
(a0 [.0.] -- a0)
(a1 [.1.] -- a1)
@ -1774,7 +1758,7 @@ print doc_from_stack_effect(*C(cons, unstack))
print doc_from_stack_effect(*C(cons, enstacken))
```
(a0 [.0.] -- [[a0 .0.] .1.])
(a1 [.1.] -- [[a1 .1.] .2.])
@ -1785,7 +1769,7 @@ C(cons, unstack)
((s0, (a0, s1)), (a0, s0))
((s1, (a1, s2)), (a1, s1))
@ -1833,8 +1817,8 @@ for f in muls:
print doc_from_stack_effect(*dup), doc_from_stack_effect(*f), doc_from_stack_effect(*e)
```
(a1 -- a1 a1) (i1 i2 -- i3) (i0 -- i1)
(a1 -- a1 a1) (f1 f2 -- f3) (f0 -- f1)
(a1 -- a1 a1) (i1 i2 -- i3) (i1 -- i2)
(a1 -- a1 a1) (f1 f2 -- f3) (f1 -- f2)
@ -1855,22 +1839,22 @@ def MC(F, G):
```
```python
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
```
(f0 -- f1)
(i0 -- i1)
```python
for f in MC([dup], [mul]):
print doc_from_stack_effect(*f)
```
(n0 -- n1)
(n1 -- n2)
```python
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
```
(f1 -- f2)
(i1 -- i2)
### Representing an Unbounded Sequence of Types
@ -2155,8 +2139,8 @@ for f in MC([dup], muls):
print doc_from_stack_effect(*f)
```
(f0 -- f1)
(i0 -- i1)
(f1 -- f2)
(i1 -- i2)
@ -2167,7 +2151,7 @@ for f in MC([dup], [sum_]):
print doc_from_stack_effect(*f)
```
([n0* .0.] -- [n0* .0.] n0)
([n1* .1.] -- [n1* .1.] n1)
@ -2178,8 +2162,8 @@ for f in MC([cons], [sum_]):
print doc_from_stack_effect(*f)
```
(a0 [.0.] -- n0)
(n0 [n0* .0.] -- n1)
(a1 [.1.] -- n1)
(n1 [n1* .1.] -- n2)
@ -2192,7 +2176,7 @@ for f in MC([cons], [sum_]):
print doc_from_stack_effect(*f)
```
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n0 [n0* .0.] -- n1)
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n1 [n1* .1.] -- n2)
@ -2415,6 +2399,18 @@ expression = l2s([n1, n2, mul])
```
```python
expression
```
(n1, (n2, (mul, ())))
```python
infer(expression)
```
@ -2422,72 +2418,78 @@ infer(expression)
[]
[(s1, (f1, s1)), (s1, (i1, s1))]
```python
class SymbolJoyType(AnyJoyType):
prefix = 'F'
def __init__(self, name, sec, number):
self.name = name
self.stack_effects = sec
self.number = number
class CombinatorJoyType(SymbolJoyType): prefix = 'C'
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
CONS = SymbolJoyType('cons', [cons], 23)
DIP = CombinatorJoyType('dip', [dip_t], 44)
def kav(F, e):
#i, stack = F
if not e:
return [(F, e)]
n, e = e
if isinstance(n, SymbolJoyType):
Fs = []
for sec in n.stack_effects:
Fs.extend(MC([F], sec))
return [kav(Fn, e) for Fn in Fs]
if isinstance(n, CombinatorJoyType):
res = []
for f in n.stack_effects:
s, e = f(F[1], e)
new_F = F[0], s
res.extend(kav(new_F, e))
return res
lit = S[0], (n, S[0])
return [kav(Fn, e) for Fn in MC([F], [lit])]
infer(expression)
```
compare, and be amazed:
[(s1, (f1, s1)), (s1, (i1, s1))]
```python
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
for stack_effect_comment in infer(expression):
print doc_from_stack_effect(*stack_effect_comment)
```
(-- f1)
(-- i1)
```python
def dip(stack, expression, dictionary):
(quote, (x, stack)) = stack
expression = (x, expression)
return stack, concat(quote, expression), dictionary
expression
```
And that brings us to current Work-In-Progress. I'm pretty hopeful that the mixed-mode inferencer/interpreter `kav()` function along with the ability to specify multiple implementations for the combinators will permit modelling of the stack effects of e.g. `ifte`. If I can keep up the pace I should be able to verify that conjecture by the end of June.
(n1, (n2, (mul, ())))
```python
infer(expression)
```
[(s1, (f1, s1)), (s1, (i1, s1))]
And that brings us to current Work-In-Progress. I'm pretty hopeful that the mixed-mode inferencer/interpreter `infer()` function along with the ability to specify multiple implementations for the combinators will permit modelling of the stack effects of e.g. `ifte`. If I can keep up the pace I should be able to verify that conjecture by the end of June.
## Conclusion
(for now...)
Work remains to be done:
- the rest of the library has to be covered
- figure out how to deal with `loop` and `genrec`, etc..
- extend the types to check values (see the appendix)
- other kinds of "higher order" type variables, OR, AND, etc..
- maybe rewrite in Prolog for great good?
- definitions
- don't permit composition of functions that don't compose
- auto-compile compilable functions
- Compiling more than just the Yin functions.
- getting better visibility (than Python debugger.)
- DOOOOCS!!!! Lots of docs!
- docstrings all around
- improve this notebook (it kinda falls apart at the end narratively. I went off and just started writing code to see if it would work. It does, but now I have to come back and describe here what I did.
I'm starting to realize that, with the inferencer/checker/compiler coming along, and with the UI ready to be rewritten in Joy, I'm close to a time when my ephasis is going to have to shift from crunchy code stuff to squishy human stuff. I'm going to have to put normal people in front of this and see if, in fact, they *can* learn the basics of programming with it.
The rest of this stuff is junk and/or unfinished material.
@ -2496,113 +2498,25 @@ For this to work the type label classes have to be modified to let `T >= t` succ
```python
F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
def _ge(self, other):
return (issubclass(other.__class__, self.__class__)
or hasattr(self, 'accept')
and isinstance(other, self.accept))
print doc_from_stack_effect(*F)
AnyJoyType.__ge__ = _ge
AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
StackJoyType.accept = tuple
```
---------------------------------------------------------------------------
```python
F = infer(l2s((pop, swap, rolldown, rest, rest, cons, cons)))
TypeError Traceback (most recent call last)
for f in F:
print doc_from_stack_effect(*f)
```
<ipython-input-119-7fde90b4e88f> in <module>()
1 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
2
----> 3 print doc_from_stack_effect(*F)
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
TypeError: 'SymbolJoyType' object is not iterable
([a4 a5 .1.] a3 a2 a1 -- [a2 a3 .1.])
@ -2612,31 +2526,131 @@ from joy.parser import text_to_expression
```python
s = text_to_expression('[3 4 ...] 2 1')
F = infer(l2s((pop, pop, pop)))
for f in F:
print doc_from_stack_effect(*f)
```
(a3 a2 a1 --)
```python
s = text_to_expression('0 1 2')
s
```
(0, (1, (2, ())))
```python
L = unify(F[1], s)
F[0][0]
```
(a1, (a2, (a3, s1)))
```python
L = unify(s, F[0][0])
L
```
()
```python
F[1]
s = text_to_expression('0 1 2 [3 4]')
s
```
(0, (1, (2, ((3, (4, ())), ()))))
```python
F[0][0]
```
(a1, (a2, (a3, s1)))
```python
L = unify(s, F[0][0])
L
```
()
```python
L = unify(F[0][0], s)
L
```
()
```python
F[1][0]
```
---------------------------------------------------------------------------
IndexError Traceback (most recent call last)
<ipython-input-133-58a8e44e9cba> in <module>()
----> 1 F[1][0]
IndexError: list index out of range
```python
s[0]
```
```python
A[1] >= 23
```
## [Abstract Interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation)
I *think* this might be sorta what I'm doing above with the `kav()` function...
In any event "mixed-mode" interpreters that include values and type variables and can track constraints, etc. will be, uh, super-useful. And Abstract Interpretation should be a rich source of ideas.

View File

@ -3,42 +3,19 @@ Type Inference
==============
This notebook presents a simple type inferencer for Joy code. It can
infer the stack effect of most Joy expressions. It built largely by
means of existing ideas and research (some of it may be original but I'm
not able to say, as I don't fully understand the all of the source
material in the depth required to make that call.) A great overview of
the existing knowledge is a talk `"Type Inference in Stack-Based
Programming
infer the stack effect of most Joy expressions. It's built largely by
means of existing ideas and research. (A great overview of the existing
knowledge is a talk `"Type Inference in Stack-Based Programming
Languages" <http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/>`__
given by Rob Kleffner on or about 2017-03-10 as part of a course on the
history of programming languages.
history of programming languages.)
The notebook starts with a simple inferencer based on the work of Jaanus
Pöial which we then progressively elaborate to cover more Joy semantics.
Along the way we write a simple "compiler" that emits Python code for
what I like to call Yin functions.
Yin functions are those that only rearrange values in stacks, as opposed
to Yang functions that actually work on the values themselves. It's
interesting to note that a Joy with *only* stacks (no other kinds of
values) can be made and is Turing-complete, therefore all Yang functions
are actually Yin functions, and all computation can be performed by
manipulations of structures of containers, which is a restatement of the
Laws of Form. (Also, this implies that every program can be put into a
form such that it can be computed in a single step, although that step
may be enormous or unending.)
Although I haven't completed it yet, a Joy based on Laws of Form
provides the foundation for a provably correct computing system "down to
the metal". This is my original and still primary motivation for
developing Joy. (I want a proven-correct Operating System for a swarm of
trash-collecting recycler robots. To trust it I have to implementment it
myself from first principles, and I'm not smart enough to truly grok the
existing literature and software, so I had to go look for and find LoF
and Joy. Now that I have the mental tools to build my robot OS I can get
down to it.
Anyhow, here's type inference...
what I like to call Yin functions. (Yin functions are those that only
rearrange values in stacks, as opposed to Yang functions that actually
work on the values themselves.)
Part I: Pöial's Rules
---------------------
@ -235,8 +212,8 @@ function only rearranges the stack and doesn't do any actual processing
on the stack items themselves all the information needed to implement it
is in the stack effect comment.
Functions on Lists
~~~~~~~~~~~~~~~~~~
Functions on Stacks
~~~~~~~~~~~~~~~~~~~
These are slightly tricky.
@ -495,18 +472,12 @@ integers or tuples of type descriptors:
if s is None:
s = {}
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
return False
return s
``update()``
~~~~~~~~~~~~
@ -738,12 +709,6 @@ work:
except Exception, e:
print e
.. parsed-literal::
Cannot unify (1, 2) and (1001, 1002).
``unify()`` version 2
^^^^^^^^^^^^^^^^^^^^^
@ -760,27 +725,24 @@ deal with this recursively:
u = update(s, u)
v = update(s, v)
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
if isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != len(v) != 2:
raise ValueError(repr((u, v)))
for uu, vv in zip(u, v):
s = unify(uu, vv, s)
if s == False: # (instead of a substitution dict.)
break
return s
return False
elif isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != 2 or len(v) != 2:
# Not a type error, caller passed in a bad value.
raise ValueError(repr((u, v))) # FIXME this message sucks.
(a, b), (c, d) = u, v
s = unify(a, c, s)
if s != False:
s = unify(b, d, s)
return s
.. code:: ipython2
@ -1406,7 +1368,7 @@ of how many labels of each domain it has "seen".
pass
if not isinstance(f, tuple):
seen[f] = f.__class__(c[f.prefix])
seen[f] = f.__class__(c[f.prefix] + 1)
c[f.prefix] += 1
return seen[f]
@ -1421,7 +1383,7 @@ of how many labels of each domain it has "seen".
.. parsed-literal::
(((a0,), (a0, a0)), ((n0, n1), (n2,)))
(((a1,), (a1, a1)), ((n1, n2), (n3,)))
@ -1544,7 +1506,7 @@ Rewrite the stack effect comments:
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1561,13 +1523,13 @@ Rewrite the stack effect comments:
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
succ = (n1 -- n2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1588,7 +1550,7 @@ Compose ``dup`` and ``mul``
.. parsed-literal::
((n0,), (n1,))
((n1,), (n2,))
@ -1604,7 +1566,7 @@ Revisit the ``F`` function, works fine.
.. parsed-literal::
(((a0, (a1, s0)), a2, a3, a4), ((a3, (a2, s0)),))
(((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
@ -1615,7 +1577,7 @@ Revisit the ``F`` function, works fine.
.. parsed-literal::
([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])
([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])
Some otherwise inefficient functions are no longer to be feared. We can
@ -1634,7 +1596,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 -- a1 a0 a2)
(a1 a2 a3 -- a2 a1 a3)
.. code:: ipython2
@ -1645,7 +1607,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 a3 -- a2 a3)
(a1 a2 a3 a4 -- a3 a4)
.. code:: ipython2
@ -1656,7 +1618,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 -- a2 a1 a0)
(a1 a2 a3 -- a3 a2 a1)
``compile_()`` version 2
@ -1689,9 +1651,9 @@ the ``compile_()`` function doesn't need to generate them anymore:
.. parsed-literal::
def F(stack):
"""([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])"""
(a4, (a3, (a2, ((a0, (a1, s0)), stack)))) = stack
return ((a3, (a2, s0)), stack)
"""([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])"""
(a5, (a4, (a3, ((a1, (a2, s1)), stack)))) = stack
return ((a4, (a3, s1)), stack)
But it cannot magically create new functions that involve e.g. math and
@ -1705,9 +1667,9 @@ such. Note that this is *not* a ``sqr`` function implementation:
.. parsed-literal::
def sqr(stack):
"""(n0 -- n1)"""
(n0, stack) = stack
return (n1, stack)
"""(n1 -- n2)"""
(n1, stack) = stack
return (n2, stack)
(Eventually I should come back around to this becuase it's not tooo
@ -1742,7 +1704,7 @@ comments. We can write a function to check that:
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
dup = (a1 -- a1 a1)
dupd = (a2 a1 -- a2 a2 a1)
@ -1755,11 +1717,11 @@ comments. We can write a function to check that:
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1849,7 +1811,13 @@ It works.
This function has to be modified to use the new datastructures and it is
no longer recursive, instead recursion happens as part of unification.
Further, the first and second of Pöial's rules are now handled
automatically by the unification algorithm.
automatically by the unification algorithm. (One easy way to see this is
that now an empty stack effect comment is represented by a
``StackJoyType`` instance which is not "falsey" and so neither of the
first two rules' ``if`` clauses will ever be ``True``. Later on I change
the "truthiness" of ``StackJoyType`` to false to let e.g.
``joy.utils.stack.concat`` work with our stack effect comment cons-list
tuples.)
.. code:: ipython2
@ -1886,20 +1854,20 @@ conversion function instead. This is programmer's laziness.
.. parsed-literal::
((a0, s0), (s0, (a0, (a0, s0))))
((a1, s1), (s1, (a1, (a1, s1))))
.. code:: ipython2
C(C(stack, uncons), uncons)
reduce(C, (stack, uncons, uncons))
.. parsed-literal::
((a0, (a1, s0)), (s0, (a1, (a0, (a0, (a1, s0))))))
((a1, (a2, s1)), (s1, (a2, (a1, (a1, (a2, s1))))))
@ -1966,7 +1934,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1983,15 +1951,15 @@ Clunky junk, but it will suffice for now.
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
stack = (... -- ... [...])
succ = (n1 -- n2)
swaack = ([.1.] -- [.0.])
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -2000,8 +1968,8 @@ Clunky junk, but it will suffice for now.
print ; print doc_from_stack_effect(*stack)
print ; print doc_from_stack_effect(*C(stack, uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), cons))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, uncons)))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, cons)))
.. parsed-literal::
@ -2009,11 +1977,11 @@ Clunky junk, but it will suffice for now.
(... -- ... [...])
(... a0 -- ... a0 a0 [...])
(... a1 -- ... a1 a1 [...])
(... a1 a0 -- ... a1 a0 a0 a1 [...])
(... a2 a1 -- ... a2 a1 a1 a2 [...])
(... a0 -- ... a0 [a0 ...])
(... a1 -- ... a1 [a1 ...])
.. code:: ipython2
@ -2023,7 +1991,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])
(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])
.. code:: ipython2
@ -2037,7 +2005,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
((s0, (a0, (a1, s1))), (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1)))
((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
@ -2066,9 +2034,9 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
def Q(stack):
"""(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])"""
(s0, (a0, (a1, s1))) = stack
return (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1))
"""(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])"""
(s1, (a1, (a2, s2))) = stack
return (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2))
.. code:: ipython2
@ -2103,7 +2071,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
(a0 [.0.] -- a0)
(a1 [.1.] -- a1)
.. code:: ipython2
@ -2113,7 +2081,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
(a0 [.0.] -- [[a0 .0.] .1.])
(a1 [.1.] -- [[a1 .1.] .2.])
.. code:: ipython2
@ -2125,7 +2093,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
((s0, (a0, s1)), (a0, s0))
((s1, (a1, s2)), (a1, s1))
@ -2177,8 +2145,8 @@ Part VI: Multiple Stack Effects
.. parsed-literal::
(a1 -- a1 a1) (i1 i2 -- i3) (i0 -- i1)
(a1 -- a1 a1) (f1 f2 -- f3) (f0 -- f1)
(a1 -- a1 a1) (i1 i2 -- i3) (i1 -- i2)
(a1 -- a1 a1) (f1 f2 -- f3) (f1 -- f2)
.. code:: ipython2
@ -2197,18 +2165,6 @@ Part VI: Multiple Stack Effects
def MC(F, G):
return sorted(set(meta_compose(F, G)))
.. code:: ipython2
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
.. parsed-literal::
(f0 -- f1)
(i0 -- i1)
.. code:: ipython2
for f in MC([dup], [mul]):
@ -2217,7 +2173,19 @@ Part VI: Multiple Stack Effects
.. parsed-literal::
(n0 -- n1)
(n1 -- n2)
.. code:: ipython2
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
.. parsed-literal::
(f1 -- f2)
(i1 -- i2)
Representing an Unbounded Sequence of Types
@ -2541,8 +2509,8 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(f0 -- f1)
(i0 -- i1)
(f1 -- f2)
(i1 -- i2)
.. code:: ipython2
@ -2555,7 +2523,7 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
([n0* .0.] -- [n0* .0.] n0)
([n1* .1.] -- [n1* .1.] n1)
.. code:: ipython2
@ -2568,8 +2536,8 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(a0 [.0.] -- n0)
(n0 [n0* .0.] -- n1)
(a1 [.1.] -- n1)
(n1 [n1* .1.] -- n2)
.. code:: ipython2
@ -2584,7 +2552,7 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n0 [n0* .0.] -- n1)
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n1 [n1* .1.] -- n2)
.. code:: ipython2
@ -2826,6 +2794,19 @@ stack effect we have to "split universes" again and return both.
expression = l2s([n1, n2, mul])
.. code:: ipython2
expression
.. parsed-literal::
(n1, (n2, (mul, ())))
.. code:: ipython2
infer(expression)
@ -2835,74 +2816,97 @@ stack effect we have to "split universes" again and return both.
.. parsed-literal::
[]
[(s1, (f1, s1)), (s1, (i1, s1))]
.. code:: ipython2
class SymbolJoyType(AnyJoyType):
prefix = 'F'
def __init__(self, name, sec, number):
self.name = name
self.stack_effects = sec
self.number = number
class CombinatorJoyType(SymbolJoyType): prefix = 'C'
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
CONS = SymbolJoyType('cons', [cons], 23)
DIP = CombinatorJoyType('dip', [dip_t], 44)
def kav(F, e):
#i, stack = F
if not e:
return [(F, e)]
n, e = e
if isinstance(n, SymbolJoyType):
Fs = []
for sec in n.stack_effects:
Fs.extend(MC([F], sec))
return [kav(Fn, e) for Fn in Fs]
if isinstance(n, CombinatorJoyType):
res = []
for f in n.stack_effects:
s, e = f(F[1], e)
new_F = F[0], s
res.extend(kav(new_F, e))
return res
lit = S[0], (n, S[0])
return [kav(Fn, e) for Fn in MC([F], [lit])]
infer(expression)
.. parsed-literal::
[(s1, (f1, s1)), (s1, (i1, s1))]
compare, and be amazed:
.. code:: ipython2
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
for stack_effect_comment in infer(expression):
print doc_from_stack_effect(*stack_effect_comment)
.. parsed-literal::
(-- f1)
(-- i1)
.. code:: ipython2
def dip(stack, expression, dictionary):
(quote, (x, stack)) = stack
expression = (x, expression)
return stack, concat(quote, expression), dictionary
expression
.. parsed-literal::
(n1, (n2, (mul, ())))
.. code:: ipython2
infer(expression)
.. parsed-literal::
[(s1, (f1, s1)), (s1, (i1, s1))]
And that brings us to current Work-In-Progress. I'm pretty hopeful that
the mixed-mode inferencer/interpreter ``kav()`` function along with the
ability to specify multiple implementations for the combinators will
the mixed-mode inferencer/interpreter ``infer()`` function along with
the ability to specify multiple implementations for the combinators will
permit modelling of the stack effects of e.g. ``ifte``. If I can keep up
the pace I should be able to verify that conjecture by the end of June.
Conclusion
----------
(for now...)
Work remains to be done:
- the rest of the library has to be covered
- figure out how to deal with ``loop`` and ``genrec``, etc..
- extend the types to check values (see the appendix)
- other kinds of "higher order" type variables, OR, AND, etc..
- maybe rewrite in Prolog for great good?
- definitions
- don't permit composition of functions that don't compose
- auto-compile compilable functions
- Compiling more than just the Yin functions.
- getting better visibility (than Python debugger.)
- DOOOOCS!!!! Lots of docs!
- docstrings all around
- improve this notebook (it kinda falls apart at the end narratively. I
went off and just started writing code to see if it would work. It
does, but now I have to come back and describe here what I did.
I'm starting to realize that, with the inferencer/checker/compiler
coming along, and with the UI ready to be rewritten in Joy, I'm close to
a time when my ephasis is going to have to shift from crunchy code stuff
to squishy human stuff. I'm going to have to put normal people in front
of this and see if, in fact, they *can* learn the basics of programming
with it.
The rest of this stuff is junk and/or unfinished material.
Appendix: Joy in the Logical Paradigm
@ -2914,115 +2918,26 @@ For this to work the type label classes have to be modified to let
.. code:: ipython2
F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
def _ge(self, other):
return (issubclass(other.__class__, self.__class__)
or hasattr(self, 'accept')
and isinstance(other, self.accept))
print doc_from_stack_effect(*F)
AnyJoyType.__ge__ = _ge
AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
StackJoyType.accept = tuple
.. code:: ipython2
::
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-119-7fde90b4e88f> in <module>()
1 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
2
----> 3 print doc_from_stack_effect(*F)
F = infer(l2s((pop, swap, rolldown, rest, rest, cons, cons)))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
for f in F:
print doc_from_stack_effect(*f)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
.. parsed-literal::
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
TypeError: 'SymbolJoyType' object is not iterable
([a4 a5 .1.] a3 a2 a1 -- [a2 a3 .1.])
.. code:: ipython2
@ -3031,26 +2946,140 @@ For this to work the type label classes have to be modified to let
.. code:: ipython2
s = text_to_expression('[3 4 ...] 2 1')
F = infer(l2s((pop, pop, pop)))
for f in F:
print doc_from_stack_effect(*f)
.. parsed-literal::
(a3 a2 a1 --)
.. code:: ipython2
s = text_to_expression('0 1 2')
s
.. parsed-literal::
(0, (1, (2, ())))
.. code:: ipython2
L = unify(F[1], s)
F[0][0]
.. parsed-literal::
(a1, (a2, (a3, s1)))
.. code:: ipython2
L = unify(s, F[0][0])
L
.. parsed-literal::
()
.. code:: ipython2
F[1]
s = text_to_expression('0 1 2 [3 4]')
s
.. parsed-literal::
(0, (1, (2, ((3, (4, ())), ()))))
.. code:: ipython2
F[0][0]
.. parsed-literal::
(a1, (a2, (a3, s1)))
.. code:: ipython2
L = unify(s, F[0][0])
L
.. parsed-literal::
()
.. code:: ipython2
L = unify(F[0][0], s)
L
.. parsed-literal::
()
.. code:: ipython2
F[1][0]
::
---------------------------------------------------------------------------
IndexError Traceback (most recent call last)
<ipython-input-133-58a8e44e9cba> in <module>()
----> 1 F[1][0]
IndexError: list index out of range
.. code:: ipython2
s[0]
.. code:: ipython2
A[1] >= 23
`Abstract Interpretation <https://en.wikipedia.org/wiki/Abstract_interpretation>`__
-----------------------------------------------------------------------------------

View File

@ -35,38 +35,18 @@
<div class="section" id="type-inference">
<h1>Type Inference<a class="headerlink" href="#type-inference" title="Permalink to this headline"></a></h1>
<p>This notebook presents a simple type inferencer for Joy code. It can
infer the stack effect of most Joy expressions. It built largely by
means of existing ideas and research (some of it may be original but Im
not able to say, as I dont fully understand the all of the source
material in the depth required to make that call.) A great overview of
the existing knowledge is a talk <a class="reference external" href="http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/">“Type Inference in Stack-Based
Programming
infer the stack effect of most Joy expressions. Its built largely by
means of existing ideas and research. (A great overview of the existing
knowledge is a talk <a class="reference external" href="http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/">“Type Inference in Stack-Based Programming
Languages”</a>
given by Rob Kleffner on or about 2017-03-10 as part of a course on the
history of programming languages.</p>
history of programming languages.)</p>
<p>The notebook starts with a simple inferencer based on the work of Jaanus
Pöial which we then progressively elaborate to cover more Joy semantics.
Along the way we write a simple “compiler” that emits Python code for
what I like to call Yin functions.</p>
<p>Yin functions are those that only rearrange values in stacks, as opposed
to Yang functions that actually work on the values themselves. Its
interesting to note that a Joy with <em>only</em> stacks (no other kinds of
values) can be made and is Turing-complete, therefore all Yang functions
are actually Yin functions, and all computation can be performed by
manipulations of structures of containers, which is a restatement of the
Laws of Form. (Also, this implies that every program can be put into a
form such that it can be computed in a single step, although that step
may be enormous or unending.)</p>
<p>Although I havent completed it yet, a Joy based on Laws of Form
provides the foundation for a provably correct computing system “down to
the metal”. This is my original and still primary motivation for
developing Joy. (I want a proven-correct Operating System for a swarm of
trash-collecting recycler robots. To trust it I have to implementment it
myself from first principles, and Im not smart enough to truly grok the
existing literature and software, so I had to go look for and find LoF
and Joy. Now that I have the mental tools to build my robot OS I can get
down to it.</p>
<p>Anyhow, heres type inference…</p>
what I like to call Yin functions. (Yin functions are those that only
rearrange values in stacks, as opposed to Yang functions that actually
work on the values themselves.)</p>
<div class="section" id="part-i-poial-s-rules">
<h2>Part I: Pöials Rules<a class="headerlink" href="#part-i-poial-s-rules" title="Permalink to this headline"></a></h2>
<p><a class="reference external" href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.212.6026">“Typing Tools for Typeless Stack Languages” by Jaanus
@ -222,8 +202,8 @@ function only rearranges the stack and doesnt do any actual processing
on the stack items themselves all the information needed to implement it
is in the stack effect comment.</p>
</div>
<div class="section" id="functions-on-lists">
<h3>Functions on Lists<a class="headerlink" href="#functions-on-lists" title="Permalink to this headline"></a></h3>
<div class="section" id="functions-on-stacks">
<h3>Functions on Stacks<a class="headerlink" href="#functions-on-stacks" title="Permalink to this headline"></a></h3>
<p>These are slightly tricky.</p>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">rest</span> <span class="p">(</span> <span class="p">[</span><span class="mi">1</span> <span class="o">...</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">...</span><span class="p">]</span> <span class="p">)</span>
@ -426,18 +406,12 @@ integers or tuples of type descriptors:</p>
<span class="k">if</span> <span class="n">s</span> <span class="ow">is</span> <span class="kc">None</span><span class="p">:</span>
<span class="n">s</span> <span class="o">=</span> <span class="p">{}</span>
<span class="k">if</span> <span class="n">u</span> <span class="o">==</span> <span class="n">v</span><span class="p">:</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="n">s</span><span class="p">[</span><span class="n">u</span><span class="p">]</span> <span class="o">=</span> <span class="n">v</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="k">elif</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="n">s</span><span class="p">[</span><span class="n">v</span><span class="p">]</span> <span class="o">=</span> <span class="n">u</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">return</span> <span class="kc">False</span>
<span class="k">return</span> <span class="n">s</span>
</pre></div>
</div>
</div>
@ -592,9 +566,6 @@ work:</p>
<span class="nb">print</span> <span class="n">e</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">Cannot</span> <span class="n">unify</span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">)</span> <span class="ow">and</span> <span class="p">(</span><span class="mi">1001</span><span class="p">,</span> <span class="mi">1002</span><span class="p">)</span><span class="o">.</span>
</pre></div>
</div>
<div class="section" id="unify-version-2">
<h4><code class="docutils literal notranslate"><span class="pre">unify()</span></code> version 2<a class="headerlink" href="#unify-version-2" title="Permalink to this headline"></a></h4>
<p>The problem is that the <code class="docutils literal notranslate"><span class="pre">unify()</span></code> function as written doesnt handle
@ -607,27 +578,24 @@ deal with this recursively:</p>
<span class="n">u</span> <span class="o">=</span> <span class="n">update</span><span class="p">(</span><span class="n">s</span><span class="p">,</span> <span class="n">u</span><span class="p">)</span>
<span class="n">v</span> <span class="o">=</span> <span class="n">update</span><span class="p">(</span><span class="n">s</span><span class="p">,</span> <span class="n">v</span><span class="p">)</span>
<span class="k">if</span> <span class="n">u</span> <span class="o">==</span> <span class="n">v</span><span class="p">:</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="n">s</span><span class="p">[</span><span class="n">u</span><span class="p">]</span> <span class="o">=</span> <span class="n">v</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="k">elif</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">int</span><span class="p">):</span>
<span class="n">s</span><span class="p">[</span><span class="n">v</span><span class="p">]</span> <span class="o">=</span> <span class="n">u</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="nb">tuple</span><span class="p">)</span> <span class="ow">and</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">tuple</span><span class="p">):</span>
<span class="k">if</span> <span class="nb">len</span><span class="p">(</span><span class="n">u</span><span class="p">)</span> <span class="o">!=</span> <span class="nb">len</span><span class="p">(</span><span class="n">v</span><span class="p">)</span> <span class="o">!=</span> <span class="mi">2</span><span class="p">:</span>
<span class="k">raise</span> <span class="ne">ValueError</span><span class="p">(</span><span class="nb">repr</span><span class="p">((</span><span class="n">u</span><span class="p">,</span> <span class="n">v</span><span class="p">)))</span>
<span class="k">for</span> <span class="n">uu</span><span class="p">,</span> <span class="n">vv</span> <span class="ow">in</span> <span class="nb">zip</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="n">v</span><span class="p">):</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">uu</span><span class="p">,</span> <span class="n">vv</span><span class="p">,</span> <span class="n">s</span><span class="p">)</span>
<span class="k">if</span> <span class="n">s</span> <span class="o">==</span> <span class="kc">False</span><span class="p">:</span> <span class="c1"># (instead of a substitution dict.)</span>
<span class="k">break</span>
<span class="k">return</span> <span class="n">s</span>
<span class="k">elif</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="nb">tuple</span><span class="p">)</span> <span class="ow">and</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">v</span><span class="p">,</span> <span class="nb">tuple</span><span class="p">):</span>
<span class="k">return</span> <span class="kc">False</span>
<span class="k">if</span> <span class="nb">len</span><span class="p">(</span><span class="n">u</span><span class="p">)</span> <span class="o">!=</span> <span class="mi">2</span> <span class="ow">or</span> <span class="nb">len</span><span class="p">(</span><span class="n">v</span><span class="p">)</span> <span class="o">!=</span> <span class="mi">2</span><span class="p">:</span>
<span class="c1"># Not a type error, caller passed in a bad value.</span>
<span class="k">raise</span> <span class="ne">ValueError</span><span class="p">(</span><span class="nb">repr</span><span class="p">((</span><span class="n">u</span><span class="p">,</span> <span class="n">v</span><span class="p">)))</span> <span class="c1"># FIXME this message sucks.</span>
<span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">),</span> <span class="p">(</span><span class="n">c</span><span class="p">,</span> <span class="n">d</span><span class="p">)</span> <span class="o">=</span> <span class="n">u</span><span class="p">,</span> <span class="n">v</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">s</span><span class="p">)</span>
<span class="k">if</span> <span class="n">s</span> <span class="o">!=</span> <span class="kc">False</span><span class="p">:</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">b</span><span class="p">,</span> <span class="n">d</span><span class="p">,</span> <span class="n">s</span><span class="p">)</span>
<span class="k">return</span> <span class="n">s</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">C</span><span class="p">(</span><span class="n">cons</span><span class="p">,</span> <span class="n">uncons</span><span class="p">)</span>
@ -1122,7 +1090,7 @@ of how many labels of each domain it has “seen”.</p>
<span class="k">pass</span>
<span class="k">if</span> <span class="ow">not</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="nb">tuple</span><span class="p">):</span>
<span class="n">seen</span><span class="p">[</span><span class="n">f</span><span class="p">]</span> <span class="o">=</span> <span class="n">f</span><span class="o">.</span><span class="vm">__class__</span><span class="p">(</span><span class="n">c</span><span class="p">[</span><span class="n">f</span><span class="o">.</span><span class="n">prefix</span><span class="p">])</span>
<span class="n">seen</span><span class="p">[</span><span class="n">f</span><span class="p">]</span> <span class="o">=</span> <span class="n">f</span><span class="o">.</span><span class="vm">__class__</span><span class="p">(</span><span class="n">c</span><span class="p">[</span><span class="n">f</span><span class="o">.</span><span class="n">prefix</span><span class="p">]</span> <span class="o">+</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">c</span><span class="p">[</span><span class="n">f</span><span class="o">.</span><span class="n">prefix</span><span class="p">]</span> <span class="o">+=</span> <span class="mi">1</span>
<span class="k">return</span> <span class="n">seen</span><span class="p">[</span><span class="n">f</span><span class="p">]</span>
@ -1132,7 +1100,7 @@ of how many labels of each domain it has “seen”.</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">delabel</span><span class="p">(</span><span class="n">foo</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(((</span><span class="n">a0</span><span class="p">,),</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">a0</span><span class="p">)),</span> <span class="p">((</span><span class="n">n0</span><span class="p">,</span> <span class="n">n1</span><span class="p">),</span> <span class="p">(</span><span class="n">n2</span><span class="p">,)))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(((</span><span class="n">a1</span><span class="p">,),</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">a1</span><span class="p">)),</span> <span class="p">((</span><span class="n">n1</span><span class="p">,</span> <span class="n">n2</span><span class="p">),</span> <span class="p">(</span><span class="n">n3</span><span class="p">,)))</span>
</pre></div>
</div>
</div>
@ -1246,7 +1214,7 @@ of how many labels of each domain it has “seen”.</p>
<span class="nb">print</span> <span class="n">name</span><span class="p">,</span> <span class="s1">&#39;=&#39;</span><span class="p">,</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">stack_effect_comment</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">cons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">divmod_</span> <span class="o">=</span> <span class="p">(</span><span class="n">n2</span> <span class="n">n1</span> <span class="o">--</span> <span class="n">n4</span> <span class="n">n3</span><span class="p">)</span>
<span class="n">dup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span>
@ -1263,13 +1231,13 @@ of how many labels of each domain it has “seen”.</p>
<span class="n">rest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">rolldown</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a3</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">rollup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a3</span> <span class="n">a1</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">sqrt</span> <span class="o">=</span> <span class="p">(</span><span class="n">n0</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">sqrt</span> <span class="o">=</span> <span class="p">(</span><span class="n">n1</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
<span class="n">succ</span> <span class="o">=</span> <span class="p">(</span><span class="n">n1</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
<span class="n">swap</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="n">a0</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">a1</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a3</span><span class="p">)</span>
<span class="n">tuck</span> <span class="o">=</span> <span class="p">(</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">uncons</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
</pre></div>
@ -1283,7 +1251,7 @@ of how many labels of each domain it has “seen”.</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">C</span><span class="p">(</span><span class="n">dup</span><span class="p">,</span> <span class="n">mul</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">n0</span><span class="p">,),</span> <span class="p">(</span><span class="n">n1</span><span class="p">,))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">n1</span><span class="p">,),</span> <span class="p">(</span><span class="n">n2</span><span class="p">,))</span>
</pre></div>
</div>
<p>Revisit the <code class="docutils literal notranslate"><span class="pre">F</span></code> function, works fine.</p>
@ -1291,13 +1259,13 @@ of how many labels of each domain it has “seen”.</p>
<span class="n">F</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(((</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">a2</span><span class="p">,</span> <span class="n">a3</span><span class="p">,</span> <span class="n">a4</span><span class="p">),</span> <span class="p">((</span><span class="n">a3</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">a3</span><span class="p">,</span> <span class="n">a4</span><span class="p">,</span> <span class="n">a5</span><span class="p">),</span> <span class="p">((</span><span class="n">a4</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">F</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="n">a2</span> <span class="n">a3</span> <span class="n">a4</span> <span class="o">--</span> <span class="p">[</span><span class="n">a3</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">a3</span> <span class="n">a4</span> <span class="n">a5</span> <span class="o">--</span> <span class="p">[</span><span class="n">a4</span> <span class="n">a3</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
</pre></div>
</div>
<p>Some otherwise inefficient functions are no longer to be feared. We can
@ -1310,21 +1278,21 @@ also get the effect of combinators in some limited cases.</p>
<span class="n">neato</span><span class="p">(</span><span class="n">rollup</span><span class="p">,</span> <span class="n">swap</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a0</span> <span class="n">a2</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a1</span> <span class="n">a3</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="c1"># e.g. [popop] dipd</span>
<span class="n">neato</span><span class="p">(</span><span class="n">popdd</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">,</span> <span class="n">pop</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a3</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="n">a4</span> <span class="o">--</span> <span class="n">a3</span> <span class="n">a4</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="c1"># Reverse the order of the top three items.</span>
<span class="n">neato</span><span class="p">(</span><span class="n">rollup</span><span class="p">,</span> <span class="n">swap</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a1</span> <span class="n">a0</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a3</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
</pre></div>
</div>
</div>
@ -1351,9 +1319,9 @@ the <code class="docutils literal notranslate"><span class="pre">compile_()</spa
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">F</span><span class="p">(</span><span class="n">stack</span><span class="p">):</span>
<span class="sd">&quot;&quot;&quot;([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">a4</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="p">((</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">stack</span><span class="p">))))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">((</span><span class="n">a3</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">stack</span><span class="p">)</span>
<span class="sd">&quot;&quot;&quot;([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">a5</span><span class="p">,</span> <span class="p">(</span><span class="n">a4</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="p">((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">stack</span><span class="p">))))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">((</span><span class="n">a4</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">stack</span><span class="p">)</span>
</pre></div>
</div>
<p>But it cannot magically create new functions that involve e.g. math and
@ -1362,9 +1330,9 @@ such. Note that this is <em>not</em> a <code class="docutils literal notranslate
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">sqr</span><span class="p">(</span><span class="n">stack</span><span class="p">):</span>
<span class="sd">&quot;&quot;&quot;(n0 -- n1)&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">n0</span><span class="p">,</span> <span class="n">stack</span><span class="p">)</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">(</span><span class="n">n1</span><span class="p">,</span> <span class="n">stack</span><span class="p">)</span>
<span class="sd">&quot;&quot;&quot;(n1 -- n2)&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">n1</span><span class="p">,</span> <span class="n">stack</span><span class="p">)</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">(</span><span class="n">n2</span><span class="p">,</span> <span class="n">stack</span><span class="p">)</span>
</pre></div>
</div>
<p>(Eventually I should come back around to this becuase its not tooo
@ -1392,7 +1360,7 @@ comments. We can write a function to check that:</p>
<span class="nb">print</span> <span class="n">name</span><span class="p">,</span> <span class="s1">&#39;=&#39;</span><span class="p">,</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">stack_effect_comment</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">cons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">dup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">dupd</span> <span class="o">=</span> <span class="p">(</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
@ -1405,11 +1373,11 @@ comments. We can write a function to check that:</p>
<span class="n">rest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">rolldown</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a3</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">rollup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a3</span> <span class="n">a1</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">swap</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="n">a0</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">a1</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a3</span><span class="p">)</span>
<span class="n">tuck</span> <span class="o">=</span> <span class="p">(</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">uncons</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
</pre></div>
@ -1482,7 +1450,13 @@ sequence and <code class="docutils literal notranslate"><span class="pre">unify(
<p>This function has to be modified to use the new datastructures and it is
no longer recursive, instead recursion happens as part of unification.
Further, the first and second of Pöials rules are now handled
automatically by the unification algorithm.</p>
automatically by the unification algorithm. (One easy way to see this is
that now an empty stack effect comment is represented by a
<code class="docutils literal notranslate"><span class="pre">StackJoyType</span></code> instance which is not “falsey” and so neither of the
first two rules <code class="docutils literal notranslate"><span class="pre">if</span></code> clauses will ever be <code class="docutils literal notranslate"><span class="pre">True</span></code>. Later on I change
the “truthiness” of <code class="docutils literal notranslate"><span class="pre">StackJoyType</span></code> to false to let e.g.
<code class="docutils literal notranslate"><span class="pre">joy.utils.stack.concat</span></code> work with our stack effect comment cons-list
tuples.)</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
@ -1509,13 +1483,13 @@ conversion function instead. This is programmers laziness.</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">C</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">),</span> <span class="p">(</span><span class="n">s0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">))))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">),</span> <span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">C</span><span class="p">(</span><span class="n">C</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">),</span> <span class="n">uncons</span><span class="p">)</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">reduce</span><span class="p">(</span><span class="n">C</span><span class="p">,</span> <span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">,</span> <span class="n">uncons</span><span class="p">))</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="p">(</span><span class="n">s0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s0</span><span class="p">))))))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s1</span><span class="p">))))))</span>
</pre></div>
</div>
<p>The display function should be changed too.</p>
@ -1575,7 +1549,7 @@ conversion function instead. This is programmers laziness.</p>
<span class="nb">print</span> <span class="n">name</span><span class="p">,</span> <span class="s1">&#39;=&#39;</span><span class="p">,</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">stack_effect_comment</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a0</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">ccons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">cons</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">divmod_</span> <span class="o">=</span> <span class="p">(</span><span class="n">n2</span> <span class="n">n1</span> <span class="o">--</span> <span class="n">n4</span> <span class="n">n3</span><span class="p">)</span>
<span class="n">dup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span>
@ -1592,38 +1566,38 @@ conversion function instead. This is programmers laziness.</p>
<span class="n">rest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">rolldown</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a3</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">rollup</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">--</span> <span class="n">a3</span> <span class="n">a1</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">sqrt</span> <span class="o">=</span> <span class="p">(</span><span class="n">n0</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<span class="n">rrest</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">second</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">sqrt</span> <span class="o">=</span> <span class="p">(</span><span class="n">n1</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
<span class="n">stack</span> <span class="o">=</span> <span class="p">(</span><span class="o">...</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="n">succ</span> <span class="o">=</span> <span class="p">(</span><span class="n">n1</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
<span class="n">swaack</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">swap</span> <span class="o">=</span> <span class="p">(</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">--</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="n">a0</span> <span class="o">--</span> <span class="p">[</span><span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a0</span> <span class="n">a1</span> <span class="n">a2</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a2</span><span class="p">)</span>
<span class="n">swons</span> <span class="o">=</span> <span class="p">([</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">a1</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<span class="n">third</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">a3</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a3</span><span class="p">)</span>
<span class="n">tuck</span> <span class="o">=</span> <span class="p">(</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a2</span> <span class="n">a1</span><span class="p">)</span>
<span class="n">uncons</span> <span class="o">=</span> <span class="p">([</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">stack</span><span class="p">)</span>
<span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">))</span>
<span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">C</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">),</span> <span class="n">uncons</span><span class="p">))</span>
<span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">C</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">),</span> <span class="n">cons</span><span class="p">))</span>
<span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">reduce</span><span class="p">(</span><span class="n">C</span><span class="p">,</span> <span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">,</span> <span class="n">uncons</span><span class="p">)))</span>
<span class="nb">print</span> <span class="p">;</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">reduce</span><span class="p">(</span><span class="n">C</span><span class="p">,</span> <span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">uncons</span><span class="p">,</span> <span class="n">cons</span><span class="p">)))</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">...</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a0</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a0</span> <span class="n">a0</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a1</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a1</span> <span class="n">a1</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a1</span> <span class="n">a0</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a1</span> <span class="n">a0</span> <span class="n">a0</span> <span class="n">a1</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a2</span> <span class="n">a1</span> <span class="n">a1</span> <span class="n">a2</span> <span class="p">[</span><span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a0</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a0</span> <span class="p">[</span><span class="n">a0</span> <span class="o">...</span><span class="p">])</span>
<span class="p">(</span><span class="o">...</span> <span class="n">a1</span> <span class="o">--</span> <span class="o">...</span> <span class="n">a1</span> <span class="p">[</span><span class="n">a1</span> <span class="o">...</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">ccons</span><span class="p">,</span> <span class="n">stack</span><span class="p">))</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">...</span> <span class="n">a1</span> <span class="n">a0</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="n">a1</span> <span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="p">[[</span><span class="n">a1</span> <span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">...</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">...</span> <span class="n">a2</span> <span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="p">[[</span><span class="n">a2</span> <span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">...</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">Q</span> <span class="o">=</span> <span class="n">C</span><span class="p">(</span><span class="n">ccons</span><span class="p">,</span> <span class="n">stack</span><span class="p">)</span>
@ -1631,7 +1605,7 @@ conversion function instead. This is programmers laziness.</p>
<span class="n">Q</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">s0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))),</span> <span class="p">(((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">s1</span><span class="p">),</span> <span class="p">((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">s1</span><span class="p">)))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s2</span><span class="p">))),</span> <span class="p">(((</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">s2</span><span class="p">),</span> <span class="p">((</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">s2</span><span class="p">)))</span>
</pre></div>
</div>
<div class="section" id="compile-version-3">
@ -1652,9 +1626,9 @@ comments are now already in the form needed for the Python code:</p>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">Q</span><span class="p">(</span><span class="n">stack</span><span class="p">):</span>
<span class="sd">&quot;&quot;&quot;(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">s0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">(((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">s1</span><span class="p">),</span> <span class="p">((</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">)),</span> <span class="n">s1</span><span class="p">))</span>
<span class="sd">&quot;&quot;&quot;(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])&quot;&quot;&quot;</span>
<span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="n">s2</span><span class="p">)))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="k">return</span> <span class="p">(((</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">s2</span><span class="p">),</span> <span class="p">((</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="n">s2</span><span class="p">))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">unstack</span> <span class="o">=</span> <span class="p">(</span><span class="n">S</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="n">S</span><span class="p">[</span><span class="mi">0</span><span class="p">]),</span> <span class="n">S</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span>
@ -1676,19 +1650,19 @@ comments are now already in the form needed for the Python code:</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">cons</span><span class="p">,</span> <span class="n">unstack</span><span class="p">))</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a0</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">a1</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">C</span><span class="p">(</span><span class="n">cons</span><span class="p">,</span> <span class="n">enstacken</span><span class="p">))</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[[</span><span class="n">a0</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">.</span><span class="mf">2.</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">C</span><span class="p">(</span><span class="n">cons</span><span class="p">,</span> <span class="n">unstack</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">s0</span><span class="p">,</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="p">(</span><span class="n">a0</span><span class="p">,</span> <span class="n">s0</span><span class="p">))</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">((</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s2</span><span class="p">)),</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))</span>
</pre></div>
</div>
</div>
@ -1730,8 +1704,8 @@ comments are now already in the form needed for the Python code:</p>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">dup</span><span class="p">),</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">),</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">e</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span> <span class="p">(</span><span class="n">i1</span> <span class="n">i2</span> <span class="o">--</span> <span class="n">i3</span><span class="p">)</span> <span class="p">(</span><span class="n">i0</span> <span class="o">--</span> <span class="n">i1</span><span class="p">)</span>
<span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span> <span class="p">(</span><span class="n">f1</span> <span class="n">f2</span> <span class="o">--</span> <span class="n">f3</span><span class="p">)</span> <span class="p">(</span><span class="n">f0</span> <span class="o">--</span> <span class="n">f1</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span> <span class="p">(</span><span class="n">i1</span> <span class="n">i2</span> <span class="o">--</span> <span class="n">i3</span><span class="p">)</span> <span class="p">(</span><span class="n">i1</span> <span class="o">--</span> <span class="n">i2</span><span class="p">)</span>
<span class="p">(</span><span class="n">a1</span> <span class="o">--</span> <span class="n">a1</span> <span class="n">a1</span><span class="p">)</span> <span class="p">(</span><span class="n">f1</span> <span class="n">f2</span> <span class="o">--</span> <span class="n">f3</span><span class="p">)</span> <span class="p">(</span><span class="n">f1</span> <span class="o">--</span> <span class="n">f2</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">itertools</span> <span class="k">import</span> <span class="n">product</span>
@ -1749,19 +1723,19 @@ comments are now already in the form needed for the Python code:</p>
<span class="k">return</span> <span class="nb">sorted</span><span class="p">(</span><span class="nb">set</span><span class="p">(</span><span class="n">meta_compose</span><span class="p">(</span><span class="n">F</span><span class="p">,</span> <span class="n">G</span><span class="p">)))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">dup</span><span class="p">],</span> <span class="n">muls</span><span class="p">):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">f0</span> <span class="o">--</span> <span class="n">f1</span><span class="p">)</span>
<span class="p">(</span><span class="n">i0</span> <span class="o">--</span> <span class="n">i1</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">dup</span><span class="p">],</span> <span class="p">[</span><span class="n">mul</span><span class="p">]):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">n0</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">n1</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">dup</span><span class="p">],</span> <span class="n">muls</span><span class="p">):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">f1</span> <span class="o">--</span> <span class="n">f2</span><span class="p">)</span>
<span class="p">(</span><span class="n">i1</span> <span class="o">--</span> <span class="n">i2</span><span class="p">)</span>
</pre></div>
</div>
<div class="section" id="representing-an-unbounded-sequence-of-types">
@ -2024,23 +1998,23 @@ disappears:</p>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">f0</span> <span class="o">--</span> <span class="n">f1</span><span class="p">)</span>
<span class="p">(</span><span class="n">i0</span> <span class="o">--</span> <span class="n">i1</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">f1</span> <span class="o">--</span> <span class="n">f2</span><span class="p">)</span>
<span class="p">(</span><span class="n">i1</span> <span class="o">--</span> <span class="n">i2</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">dup</span><span class="p">],</span> <span class="p">[</span><span class="n">sum_</span><span class="p">]):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">n0</span><span class="o">*</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">n0</span><span class="o">*</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="n">n0</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">n1</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">cons</span><span class="p">],</span> <span class="p">[</span><span class="n">sum_</span><span class="p">]):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a0</span> <span class="p">[</span><span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n0</span><span class="p">)</span>
<span class="p">(</span><span class="n">n0</span> <span class="p">[</span><span class="n">n0</span><span class="o">*</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<span class="p">(</span><span class="n">n1</span> <span class="p">[</span><span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">sum_</span> <span class="o">=</span> <span class="p">(((</span><span class="n">N</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="p">(</span><span class="n">Ns</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="n">S</span><span class="p">[</span><span class="mi">1</span><span class="p">])),</span> <span class="n">S</span><span class="p">[</span><span class="mi">0</span><span class="p">]),</span> <span class="p">(</span><span class="n">N</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="n">S</span><span class="p">[</span><span class="mi">0</span><span class="p">]))</span>
@ -2051,7 +2025,7 @@ disappears:</p>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span> <span class="p">([</span><span class="n">n1</span> <span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n0</span><span class="p">)</span> <span class="p">(</span><span class="n">n0</span> <span class="p">[</span><span class="n">n0</span><span class="o">*</span> <span class="o">.</span><span class="mf">0.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n1</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span> <span class="p">[</span><span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="p">[</span><span class="n">a1</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span> <span class="p">([</span><span class="n">n1</span> <span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n0</span><span class="p">)</span> <span class="p">(</span><span class="n">n1</span> <span class="p">[</span><span class="n">n1</span><span class="o">*</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="o">--</span> <span class="n">n2</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">a</span> <span class="o">=</span> <span class="p">(</span><span class="n">A</span><span class="p">[</span><span class="mi">4</span><span class="p">],</span> <span class="p">(</span><span class="n">As</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="p">(</span><span class="n">A</span><span class="p">[</span><span class="mi">3</span><span class="p">],</span> <span class="n">S</span><span class="p">[</span><span class="mi">1</span><span class="p">])))</span>
@ -2241,70 +2215,77 @@ stack effect we have to “split universes” again and return both.</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">expression</span> <span class="o">=</span> <span class="n">l2s</span><span class="p">([</span><span class="n">n1</span><span class="p">,</span> <span class="n">n2</span><span class="p">,</span> <span class="n">mul</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">expression</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">n1</span><span class="p">,</span> <span class="p">(</span><span class="n">n2</span><span class="p">,</span> <span class="p">(</span><span class="n">mul</span><span class="p">,</span> <span class="p">())))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">infer</span><span class="p">(</span><span class="n">expression</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">[]</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">[(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">f1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">i1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))]</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">class</span> <span class="nc">SymbolJoyType</span><span class="p">(</span><span class="n">AnyJoyType</span><span class="p">):</span>
<span class="n">prefix</span> <span class="o">=</span> <span class="s1">&#39;F&#39;</span>
<span class="k">def</span> <span class="nf">__init__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">name</span><span class="p">,</span> <span class="n">sec</span><span class="p">,</span> <span class="n">number</span><span class="p">):</span>
<span class="bp">self</span><span class="o">.</span><span class="n">name</span> <span class="o">=</span> <span class="n">name</span>
<span class="bp">self</span><span class="o">.</span><span class="n">stack_effects</span> <span class="o">=</span> <span class="n">sec</span>
<span class="bp">self</span><span class="o">.</span><span class="n">number</span> <span class="o">=</span> <span class="n">number</span>
<span class="k">class</span> <span class="nc">CombinatorJoyType</span><span class="p">(</span><span class="n">SymbolJoyType</span><span class="p">):</span> <span class="n">prefix</span> <span class="o">=</span> <span class="s1">&#39;C&#39;</span>
<span class="k">def</span> <span class="nf">dip_t</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">expression</span><span class="p">):</span>
<span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">stack</span><span class="p">))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="n">expression</span> <span class="o">=</span> <span class="n">stack_concat</span><span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">expression</span><span class="p">))</span>
<span class="k">return</span> <span class="n">stack</span><span class="p">,</span> <span class="n">expression</span>
<span class="n">CONS</span> <span class="o">=</span> <span class="n">SymbolJoyType</span><span class="p">(</span><span class="s1">&#39;cons&#39;</span><span class="p">,</span> <span class="p">[</span><span class="n">cons</span><span class="p">],</span> <span class="mi">23</span><span class="p">)</span>
<span class="n">DIP</span> <span class="o">=</span> <span class="n">CombinatorJoyType</span><span class="p">(</span><span class="s1">&#39;dip&#39;</span><span class="p">,</span> <span class="p">[</span><span class="n">dip_t</span><span class="p">],</span> <span class="mi">44</span><span class="p">)</span>
<span class="k">def</span> <span class="nf">kav</span><span class="p">(</span><span class="n">F</span><span class="p">,</span> <span class="n">e</span><span class="p">):</span>
<span class="c1">#i, stack = F</span>
<span class="k">if</span> <span class="ow">not</span> <span class="n">e</span><span class="p">:</span>
<span class="k">return</span> <span class="p">[(</span><span class="n">F</span><span class="p">,</span> <span class="n">e</span><span class="p">)]</span>
<span class="n">n</span><span class="p">,</span> <span class="n">e</span> <span class="o">=</span> <span class="n">e</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">n</span><span class="p">,</span> <span class="n">SymbolJoyType</span><span class="p">):</span>
<span class="n">Fs</span> <span class="o">=</span> <span class="p">[]</span>
<span class="k">for</span> <span class="n">sec</span> <span class="ow">in</span> <span class="n">n</span><span class="o">.</span><span class="n">stack_effects</span><span class="p">:</span>
<span class="n">Fs</span><span class="o">.</span><span class="n">extend</span><span class="p">(</span><span class="n">MC</span><span class="p">([</span><span class="n">F</span><span class="p">],</span> <span class="n">sec</span><span class="p">))</span>
<span class="k">return</span> <span class="p">[</span><span class="n">kav</span><span class="p">(</span><span class="n">Fn</span><span class="p">,</span> <span class="n">e</span><span class="p">)</span> <span class="k">for</span> <span class="n">Fn</span> <span class="ow">in</span> <span class="n">Fs</span><span class="p">]</span>
<span class="k">if</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">n</span><span class="p">,</span> <span class="n">CombinatorJoyType</span><span class="p">):</span>
<span class="n">res</span> <span class="o">=</span> <span class="p">[]</span>
<span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">n</span><span class="o">.</span><span class="n">stack_effects</span><span class="p">:</span>
<span class="n">s</span><span class="p">,</span> <span class="n">e</span> <span class="o">=</span> <span class="n">f</span><span class="p">(</span><span class="n">F</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="n">e</span><span class="p">)</span>
<span class="n">new_F</span> <span class="o">=</span> <span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="n">s</span>
<span class="n">res</span><span class="o">.</span><span class="n">extend</span><span class="p">(</span><span class="n">kav</span><span class="p">(</span><span class="n">new_F</span><span class="p">,</span> <span class="n">e</span><span class="p">))</span>
<span class="k">return</span> <span class="n">res</span>
<span class="n">lit</span> <span class="o">=</span> <span class="n">S</span><span class="p">[</span><span class="mi">0</span><span class="p">],</span> <span class="p">(</span><span class="n">n</span><span class="p">,</span> <span class="n">S</span><span class="p">[</span><span class="mi">0</span><span class="p">])</span>
<span class="k">return</span> <span class="p">[</span><span class="n">kav</span><span class="p">(</span><span class="n">Fn</span><span class="p">,</span> <span class="n">e</span><span class="p">)</span> <span class="k">for</span> <span class="n">Fn</span> <span class="ow">in</span> <span class="n">MC</span><span class="p">([</span><span class="n">F</span><span class="p">],</span> <span class="p">[</span><span class="n">lit</span><span class="p">])]</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">infer</span><span class="p">(</span><span class="n">expression</span><span class="p">)</span>
</pre></div>
</div>
<p>compare, and be amazed:</p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">dip_t</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">expression</span><span class="p">):</span>
<span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">stack</span><span class="p">))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="n">expression</span> <span class="o">=</span> <span class="n">stack_concat</span><span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="n">expression</span><span class="p">))</span>
<span class="k">return</span> <span class="n">stack</span><span class="p">,</span> <span class="n">expression</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">[(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">f1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">i1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))]</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">dip</span><span class="p">(</span><span class="n">stack</span><span class="p">,</span> <span class="n">expression</span><span class="p">,</span> <span class="n">dictionary</span><span class="p">):</span>
<span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">stack</span><span class="p">))</span> <span class="o">=</span> <span class="n">stack</span>
<span class="n">expression</span> <span class="o">=</span> <span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">expression</span><span class="p">)</span>
<span class="k">return</span> <span class="n">stack</span><span class="p">,</span> <span class="n">concat</span><span class="p">(</span><span class="n">quote</span><span class="p">,</span> <span class="n">expression</span><span class="p">),</span> <span class="n">dictionary</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">for</span> <span class="n">stack_effect_comment</span> <span class="ow">in</span> <span class="n">infer</span><span class="p">(</span><span class="n">expression</span><span class="p">):</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">stack_effect_comment</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">--</span> <span class="n">f1</span><span class="p">)</span>
<span class="p">(</span><span class="o">--</span> <span class="n">i1</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">expression</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">n1</span><span class="p">,</span> <span class="p">(</span><span class="n">n2</span><span class="p">,</span> <span class="p">(</span><span class="n">mul</span><span class="p">,</span> <span class="p">())))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">infer</span><span class="p">(</span><span class="n">expression</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">[(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">f1</span><span class="p">,</span> <span class="n">s1</span><span class="p">)),</span> <span class="p">(</span><span class="n">s1</span><span class="p">,</span> <span class="p">(</span><span class="n">i1</span><span class="p">,</span> <span class="n">s1</span><span class="p">))]</span>
</pre></div>
</div>
<p>And that brings us to current Work-In-Progress. Im pretty hopeful that
the mixed-mode inferencer/interpreter <code class="docutils literal notranslate"><span class="pre">kav()</span></code> function along with the
ability to specify multiple implementations for the combinators will
the mixed-mode inferencer/interpreter <code class="docutils literal notranslate"><span class="pre">infer()</span></code> function along with
the ability to specify multiple implementations for the combinators will
permit modelling of the stack effects of e.g. <code class="docutils literal notranslate"><span class="pre">ifte</span></code>. If I can keep up
the pace I should be able to verify that conjecture by the end of June.</p>
</div>
<div class="section" id="conclusion">
<h2>Conclusion<a class="headerlink" href="#conclusion" title="Permalink to this headline"></a></h2>
<p>(for now…)</p>
<p>Work remains to be done:</p>
<ul class="simple">
<li>the rest of the library has to be covered</li>
<li>figure out how to deal with <code class="docutils literal notranslate"><span class="pre">loop</span></code> and <code class="docutils literal notranslate"><span class="pre">genrec</span></code>, etc..</li>
<li>extend the types to check values (see the appendix)</li>
<li>other kinds of “higher order” type variables, OR, AND, etc..</li>
<li>maybe rewrite in Prolog for great good?</li>
<li>definitions</li>
<li>dont permit composition of functions that dont compose</li>
<li>auto-compile compilable functions</li>
<li>Compiling more than just the Yin functions.</li>
<li>getting better visibility (than Python debugger.)</li>
<li>DOOOOCS!!!! Lots of docs!</li>
<li>docstrings all around</li>
<li>improve this notebook (it kinda falls apart at the end narratively. I
went off and just started writing code to see if it would work. It
does, but now I have to come back and describe here what I did.</li>
</ul>
<p>Im starting to realize that, with the inferencer/checker/compiler
coming along, and with the UI ready to be rewritten in Joy, Im close to
a time when my ephasis is going to have to shift from crunchy code stuff
to squishy human stuff. Im going to have to put normal people in front
of this and see if, in fact, they <em>can</em> learn the basics of programming
with it.</p>
<p>The rest of this stuff is junk and/or unfinished material.</p>
</div>
<div class="section" id="appendix-joy-in-the-logical-paradigm">
@ -2312,134 +2293,104 @@ the pace I should be able to verify that conjecture by the end of June.</p>
<p>For this to work the type label classes have to be modified to let
<code class="docutils literal notranslate"><span class="pre">T</span> <span class="pre">&gt;=</span> <span class="pre">t</span></code> succeed, where e.g. <code class="docutils literal notranslate"><span class="pre">T</span></code> is <code class="docutils literal notranslate"><span class="pre">IntJoyType</span></code> and <code class="docutils literal notranslate"><span class="pre">t</span></code> is
<code class="docutils literal notranslate"><span class="pre">int</span></code></p>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span> <span class="o">=</span> <span class="n">reduce</span><span class="p">(</span><span class="n">C</span><span class="p">,</span> <span class="p">(</span><span class="n">pop</span><span class="p">,</span> <span class="n">swap</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">cons</span><span class="p">,</span> <span class="n">cons</span><span class="p">))</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span> <span class="nf">_ge</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">other</span><span class="p">):</span>
<span class="k">return</span> <span class="p">(</span><span class="nb">issubclass</span><span class="p">(</span><span class="n">other</span><span class="o">.</span><span class="vm">__class__</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="vm">__class__</span><span class="p">)</span>
<span class="ow">or</span> <span class="nb">hasattr</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="s1">&#39;accept&#39;</span><span class="p">)</span>
<span class="ow">and</span> <span class="nb">isinstance</span><span class="p">(</span><span class="n">other</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">accept</span><span class="p">))</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">F</span><span class="p">)</span>
<span class="n">AnyJoyType</span><span class="o">.</span><span class="fm">__ge__</span> <span class="o">=</span> <span class="n">_ge</span>
<span class="n">AnyJoyType</span><span class="o">.</span><span class="n">accept</span> <span class="o">=</span> <span class="nb">tuple</span><span class="p">,</span> <span class="nb">int</span><span class="p">,</span> <span class="nb">float</span><span class="p">,</span> <span class="n">long</span><span class="p">,</span> <span class="nb">str</span><span class="p">,</span> <span class="n">unicode</span><span class="p">,</span> <span class="nb">bool</span><span class="p">,</span> <span class="n">Symbol</span>
<span class="n">StackJoyType</span><span class="o">.</span><span class="n">accept</span> <span class="o">=</span> <span class="nb">tuple</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="o">---------------------------------------------------------------------------</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span> <span class="o">=</span> <span class="n">infer</span><span class="p">(</span><span class="n">l2s</span><span class="p">((</span><span class="n">pop</span><span class="p">,</span> <span class="n">swap</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">cons</span><span class="p">,</span> <span class="n">cons</span><span class="p">)))</span>
<span class="ne">TypeError</span> <span class="n">Traceback</span> <span class="p">(</span><span class="n">most</span> <span class="n">recent</span> <span class="n">call</span> <span class="n">last</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">119</span><span class="o">-</span><span class="mi">7</span><span class="n">fde90b4e88f</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="o">&lt;</span><span class="n">module</span><span class="o">&gt;</span><span class="p">()</span>
<span class="mi">1</span> <span class="n">F</span> <span class="o">=</span> <span class="n">reduce</span><span class="p">(</span><span class="n">C</span><span class="p">,</span> <span class="p">(</span><span class="n">pop</span><span class="p">,</span> <span class="n">swap</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">rest</span><span class="p">,</span> <span class="n">cons</span><span class="p">,</span> <span class="n">cons</span><span class="p">))</span>
<span class="mi">2</span>
<span class="o">----&gt;</span> <span class="mi">3</span> <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">F</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">98</span><span class="o">-</span><span class="n">ddee30dbb1a6</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">10</span> <span class="k">def</span> <span class="nf">C</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">11</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span> <span class="o">=</span> <span class="n">relabel</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="o">---&gt;</span> <span class="mi">12</span> <span class="k">for</span> <span class="n">fg</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="mi">13</span> <span class="k">yield</span> <span class="n">delabel</span><span class="p">(</span><span class="n">fg</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">97</span><span class="o">-</span><span class="mi">5</span><span class="n">eb7ac5ad2c2</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="n">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
<span class="mi">1</span> <span class="k">def</span> <span class="nf">compose</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">):</span>
<span class="o">----&gt;</span> <span class="mi">2</span> <span class="p">(</span><span class="n">f_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">),</span> <span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">g_out</span><span class="p">)</span> <span class="o">=</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span>
<span class="mi">3</span> <span class="n">s</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">g_in</span><span class="p">,</span> <span class="n">f_out</span><span class="p">)</span>
<span class="mi">4</span> <span class="k">if</span> <span class="ow">not</span> <span class="n">s</span><span class="p">:</span>
<span class="mi">5</span> <span class="k">raise</span> <span class="ne">TypeError</span><span class="p">(</span><span class="s1">&#39;Cannot unify </span><span class="si">%r</span><span class="s1"> and </span><span class="si">%r</span><span class="s1">.&#39;</span> <span class="o">%</span> <span class="p">(</span><span class="n">f_out</span><span class="p">,</span> <span class="n">g_in</span><span class="p">))</span>
<span class="ne">TypeError</span><span class="p">:</span> <span class="s1">&#39;SymbolJoyType&#39;</span> <span class="nb">object</span> <span class="ow">is</span> <span class="ow">not</span> <span class="n">iterable</span>
<span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">F</span><span class="p">:</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">a4</span> <span class="n">a5</span> <span class="o">.</span><span class="mf">1.</span><span class="p">]</span> <span class="n">a3</span> <span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="p">[</span><span class="n">a2</span> <span class="n">a3</span> <span class="o">.</span><span class="mf">1.</span><span class="p">])</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">joy.parser</span> <span class="k">import</span> <span class="n">text_to_expression</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">s</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;[3 4 ...] 2 1&#39;</span><span class="p">)</span>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span> <span class="o">=</span> <span class="n">infer</span><span class="p">(</span><span class="n">l2s</span><span class="p">((</span><span class="n">pop</span><span class="p">,</span> <span class="n">pop</span><span class="p">,</span> <span class="n">pop</span><span class="p">)))</span>
<span class="k">for</span> <span class="n">f</span> <span class="ow">in</span> <span class="n">F</span><span class="p">:</span>
<span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">f</span><span class="p">)</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a3</span> <span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span><span class="p">)</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">s</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;0 1 2&#39;</span><span class="p">)</span>
<span class="n">s</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">L</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">F</span><span class="p">[</span><span class="mi">1</span><span class="p">],</span> <span class="n">s</span><span class="p">)</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="p">(</span><span class="mi">2</span><span class="p">,</span> <span class="p">())))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">][</span><span class="mi">0</span><span class="p">]</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="n">s1</span><span class="p">)))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">L</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">s</span><span class="p">,</span> <span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">][</span><span class="mi">0</span><span class="p">])</span>
<span class="n">L</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">()</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">s</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;0 1 2 [3 4]&#39;</span><span class="p">)</span>
<span class="n">s</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="p">(</span><span class="mi">2</span><span class="p">,</span> <span class="p">((</span><span class="mi">3</span><span class="p">,</span> <span class="p">(</span><span class="mi">4</span><span class="p">,</span> <span class="p">())),</span> <span class="p">()))))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">][</span><span class="mi">0</span><span class="p">]</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="n">a1</span><span class="p">,</span> <span class="p">(</span><span class="n">a2</span><span class="p">,</span> <span class="p">(</span><span class="n">a3</span><span class="p">,</span> <span class="n">s1</span><span class="p">)))</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">L</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">s</span><span class="p">,</span> <span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">][</span><span class="mi">0</span><span class="p">])</span>
<span class="n">L</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">()</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">L</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">F</span><span class="p">[</span><span class="mi">0</span><span class="p">][</span><span class="mi">0</span><span class="p">],</span> <span class="n">s</span><span class="p">)</span>
<span class="n">L</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">()</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">F</span><span class="p">[</span><span class="mi">1</span><span class="p">][</span><span class="mi">0</span><span class="p">]</span>
</pre></div>
</div>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="o">---------------------------------------------------------------------------</span>
<span class="ne">IndexError</span> <span class="n">Traceback</span> <span class="p">(</span><span class="n">most</span> <span class="n">recent</span> <span class="n">call</span> <span class="n">last</span><span class="p">)</span>
<span class="o">&lt;</span><span class="n">ipython</span><span class="o">-</span><span class="nb">input</span><span class="o">-</span><span class="mi">133</span><span class="o">-</span><span class="mi">58</span><span class="n">a8e44e9cba</span><span class="o">&gt;</span> <span class="ow">in</span> <span class="o">&lt;</span><span class="n">module</span><span class="o">&gt;</span><span class="p">()</span>
<span class="o">----&gt;</span> <span class="mi">1</span> <span class="n">F</span><span class="p">[</span><span class="mi">1</span><span class="p">][</span><span class="mi">0</span><span class="p">]</span>
<span class="ne">IndexError</span><span class="p">:</span> <span class="nb">list</span> <span class="n">index</span> <span class="n">out</span> <span class="n">of</span> <span class="nb">range</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">s</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span>
</pre></div>
</div>
<div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">A</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span> <span class="o">&gt;=</span> <span class="mi">23</span>
</pre></div>
</div>
</div>
<div class="section" id="abstract-interpretation">
<h2><a class="reference external" href="https://en.wikipedia.org/wiki/Abstract_interpretation">Abstract Interpretation</a><a class="headerlink" href="#abstract-interpretation" title="Permalink to this headline"></a></h2>
@ -2637,7 +2588,7 @@ how much information we <em>could</em> retain:</p>
<li><a class="reference internal" href="#pop-swap"><code class="docutils literal notranslate"><span class="pre">pop</span> <span class="pre">swap</span></code></a></li>
<li><a class="reference internal" href="#popswap-roll"><code class="docutils literal notranslate"><span class="pre">pop∘swap</span> <span class="pre">roll&lt;</span></code></a></li>
<li><a class="reference internal" href="#compiling-popswaproll">Compiling <code class="docutils literal notranslate"><span class="pre">pop∘swap∘roll&lt;</span></code></a></li>
<li><a class="reference internal" href="#functions-on-lists">Functions on Lists</a></li>
<li><a class="reference internal" href="#functions-on-stacks">Functions on Stacks</a></li>
<li><a class="reference internal" href="#popswaproll-rest"><code class="docutils literal notranslate"><span class="pre">pop∘swap∘roll&lt;</span> <span class="pre">rest</span></code></a></li>
<li><a class="reference internal" href="#popswaproll-rest-rest"><code class="docutils literal notranslate"><span class="pre">pop∘swap∘roll&lt;∘rest</span> <span class="pre">rest</span></code></a></li>
<li><a class="reference internal" href="#popswaproll-restrest-cons"><code class="docutils literal notranslate"><span class="pre">pop∘swap∘roll&lt;∘rest∘rest</span> <span class="pre">cons</span></code></a></li>
@ -2702,6 +2653,7 @@ how much information we <em>could</em> retain:</p>
</ul>
</li>
<li><a class="reference internal" href="#part-vii-typing-combinators">Part VII: Typing Combinators</a></li>
<li><a class="reference internal" href="#conclusion">Conclusion</a></li>
<li><a class="reference internal" href="#appendix-joy-in-the-logical-paradigm">Appendix: Joy in the Logical Paradigm</a></li>
<li><a class="reference internal" href="#abstract-interpretation">Abstract Interpretation</a></li>
<li><a class="reference internal" href="#junk">Junk</a><ul>

View File

@ -126,6 +126,7 @@
<li class="toctree-l2"><a class="reference internal" href="Types.html#part-v-functions-that-use-the-stack">Part V: Functions that use the Stack</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#part-vi-multiple-stack-effects">Part VI: Multiple Stack Effects</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#part-vii-typing-combinators">Part VII: Typing Combinators</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#conclusion">Conclusion</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#appendix-joy-in-the-logical-paradigm">Appendix: Joy in the Logical Paradigm</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#abstract-interpretation">Abstract Interpretation</a></li>
<li class="toctree-l2"><a class="reference internal" href="Types.html#junk">Junk</a></li>

File diff suppressed because one or more lines are too long

View File

@ -3,42 +3,19 @@ Type Inference
==============
This notebook presents a simple type inferencer for Joy code. It can
infer the stack effect of most Joy expressions. It built largely by
means of existing ideas and research (some of it may be original but I'm
not able to say, as I don't fully understand the all of the source
material in the depth required to make that call.) A great overview of
the existing knowledge is a talk `"Type Inference in Stack-Based
Programming
infer the stack effect of most Joy expressions. It's built largely by
means of existing ideas and research. (A great overview of the existing
knowledge is a talk `"Type Inference in Stack-Based Programming
Languages" <http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/>`__
given by Rob Kleffner on or about 2017-03-10 as part of a course on the
history of programming languages.
history of programming languages.)
The notebook starts with a simple inferencer based on the work of Jaanus
Pöial which we then progressively elaborate to cover more Joy semantics.
Along the way we write a simple "compiler" that emits Python code for
what I like to call Yin functions.
Yin functions are those that only rearrange values in stacks, as opposed
to Yang functions that actually work on the values themselves. It's
interesting to note that a Joy with *only* stacks (no other kinds of
values) can be made and is Turing-complete, therefore all Yang functions
are actually Yin functions, and all computation can be performed by
manipulations of structures of containers, which is a restatement of the
Laws of Form. (Also, this implies that every program can be put into a
form such that it can be computed in a single step, although that step
may be enormous or unending.)
Although I haven't completed it yet, a Joy based on Laws of Form
provides the foundation for a provably correct computing system "down to
the metal". This is my original and still primary motivation for
developing Joy. (I want a proven-correct Operating System for a swarm of
trash-collecting recycler robots. To trust it I have to implementment it
myself from first principles, and I'm not smart enough to truly grok the
existing literature and software, so I had to go look for and find LoF
and Joy. Now that I have the mental tools to build my robot OS I can get
down to it.
Anyhow, here's type inference...
what I like to call Yin functions. (Yin functions are those that only
rearrange values in stacks, as opposed to Yang functions that actually
work on the values themselves.)
Part I: Pöial's Rules
---------------------
@ -235,8 +212,8 @@ function only rearranges the stack and doesn't do any actual processing
on the stack items themselves all the information needed to implement it
is in the stack effect comment.
Functions on Lists
~~~~~~~~~~~~~~~~~~
Functions on Stacks
~~~~~~~~~~~~~~~~~~~
These are slightly tricky.
@ -495,18 +472,12 @@ integers or tuples of type descriptors:
if s is None:
s = {}
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
return False
return s
``update()``
~~~~~~~~~~~~
@ -738,12 +709,6 @@ work:
except Exception, e:
print e
.. parsed-literal::
Cannot unify (1, 2) and (1001, 1002).
``unify()`` version 2
^^^^^^^^^^^^^^^^^^^^^
@ -760,27 +725,24 @@ deal with this recursively:
u = update(s, u)
v = update(s, v)
if u == v:
return s
if isinstance(u, int):
s[u] = v
return s
if isinstance(v, int):
elif isinstance(v, int):
s[v] = u
return s
if isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != len(v) != 2:
raise ValueError(repr((u, v)))
for uu, vv in zip(u, v):
s = unify(uu, vv, s)
if s == False: # (instead of a substitution dict.)
break
return s
return False
elif isinstance(u, tuple) and isinstance(v, tuple):
if len(u) != 2 or len(v) != 2:
# Not a type error, caller passed in a bad value.
raise ValueError(repr((u, v))) # FIXME this message sucks.
(a, b), (c, d) = u, v
s = unify(a, c, s)
if s != False:
s = unify(b, d, s)
return s
.. code:: ipython2
@ -1406,7 +1368,7 @@ of how many labels of each domain it has "seen".
pass
if not isinstance(f, tuple):
seen[f] = f.__class__(c[f.prefix])
seen[f] = f.__class__(c[f.prefix] + 1)
c[f.prefix] += 1
return seen[f]
@ -1421,7 +1383,7 @@ of how many labels of each domain it has "seen".
.. parsed-literal::
(((a0,), (a0, a0)), ((n0, n1), (n2,)))
(((a1,), (a1, a1)), ((n1, n2), (n3,)))
@ -1544,7 +1506,7 @@ Rewrite the stack effect comments:
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1561,13 +1523,13 @@ Rewrite the stack effect comments:
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
succ = (n1 -- n2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1588,7 +1550,7 @@ Compose ``dup`` and ``mul``
.. parsed-literal::
((n0,), (n1,))
((n1,), (n2,))
@ -1604,7 +1566,7 @@ Revisit the ``F`` function, works fine.
.. parsed-literal::
(((a0, (a1, s0)), a2, a3, a4), ((a3, (a2, s0)),))
(((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
@ -1615,7 +1577,7 @@ Revisit the ``F`` function, works fine.
.. parsed-literal::
([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])
([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])
Some otherwise inefficient functions are no longer to be feared. We can
@ -1634,7 +1596,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 -- a1 a0 a2)
(a1 a2 a3 -- a2 a1 a3)
.. code:: ipython2
@ -1645,7 +1607,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 a3 -- a2 a3)
(a1 a2 a3 a4 -- a3 a4)
.. code:: ipython2
@ -1656,7 +1618,7 @@ also get the effect of combinators in some limited cases.
.. parsed-literal::
(a0 a1 a2 -- a2 a1 a0)
(a1 a2 a3 -- a3 a2 a1)
``compile_()`` version 2
@ -1689,9 +1651,9 @@ the ``compile_()`` function doesn't need to generate them anymore:
.. parsed-literal::
def F(stack):
"""([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])"""
(a4, (a3, (a2, ((a0, (a1, s0)), stack)))) = stack
return ((a3, (a2, s0)), stack)
"""([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])"""
(a5, (a4, (a3, ((a1, (a2, s1)), stack)))) = stack
return ((a4, (a3, s1)), stack)
But it cannot magically create new functions that involve e.g. math and
@ -1705,9 +1667,9 @@ such. Note that this is *not* a ``sqr`` function implementation:
.. parsed-literal::
def sqr(stack):
"""(n0 -- n1)"""
(n0, stack) = stack
return (n1, stack)
"""(n1 -- n2)"""
(n1, stack) = stack
return (n2, stack)
(Eventually I should come back around to this becuase it's not tooo
@ -1742,7 +1704,7 @@ comments. We can write a function to check that:
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
dup = (a1 -- a1 a1)
dupd = (a2 a1 -- a2 a2 a1)
@ -1755,11 +1717,11 @@ comments. We can write a function to check that:
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -1849,7 +1811,13 @@ It works.
This function has to be modified to use the new datastructures and it is
no longer recursive, instead recursion happens as part of unification.
Further, the first and second of Pöial's rules are now handled
automatically by the unification algorithm.
automatically by the unification algorithm. (One easy way to see this is
that now an empty stack effect comment is represented by a
``StackJoyType`` instance which is not "falsey" and so neither of the
first two rules' ``if`` clauses will ever be ``True``. Later on I change
the "truthiness" of ``StackJoyType`` to false to let e.g.
``joy.utils.stack.concat`` work with our stack effect comment cons-list
tuples.)
.. code:: ipython2
@ -1886,20 +1854,20 @@ conversion function instead. This is programmer's laziness.
.. parsed-literal::
((a0, s0), (s0, (a0, (a0, s0))))
((a1, s1), (s1, (a1, (a1, s1))))
.. code:: ipython2
C(C(stack, uncons), uncons)
reduce(C, (stack, uncons, uncons))
.. parsed-literal::
((a0, (a1, s0)), (s0, (a1, (a0, (a0, (a1, s0))))))
((a1, (a2, s1)), (s1, (a2, (a1, (a1, (a2, s1))))))
@ -1966,7 +1934,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
cons = (a1 [.1.] -- [a1 .1.])
divmod_ = (n2 n1 -- n4 n3)
dup = (a1 -- a1 a1)
@ -1983,15 +1951,15 @@ Clunky junk, but it will suffice for now.
rest = ([a1 .1.] -- [.1.])
rolldown = (a1 a2 a3 -- a2 a3 a1)
rollup = (a1 a2 a3 -- a3 a1 a2)
rrest = ([a0 a1 .0.] -- [.0.])
second = ([a0 a1 .0.] -- a1)
sqrt = (n0 -- n1)
rrest = ([a1 a2 .1.] -- [.1.])
second = ([a1 a2 .1.] -- a2)
sqrt = (n1 -- n2)
stack = (... -- ... [...])
succ = (n1 -- n2)
swaack = ([.1.] -- [.0.])
swap = (a1 a2 -- a2 a1)
swons = ([.0.] a0 -- [a0 .0.])
third = ([a0 a1 a2 .0.] -- a2)
swons = ([.1.] a1 -- [a1 .1.])
third = ([a1 a2 a3 .1.] -- a3)
tuck = (a2 a1 -- a1 a2 a1)
uncons = ([a1 .1.] -- a1 [.1.])
@ -2000,8 +1968,8 @@ Clunky junk, but it will suffice for now.
print ; print doc_from_stack_effect(*stack)
print ; print doc_from_stack_effect(*C(stack, uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), uncons))
print ; print doc_from_stack_effect(*C(C(stack, uncons), cons))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, uncons)))
print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, cons)))
.. parsed-literal::
@ -2009,11 +1977,11 @@ Clunky junk, but it will suffice for now.
(... -- ... [...])
(... a0 -- ... a0 a0 [...])
(... a1 -- ... a1 a1 [...])
(... a1 a0 -- ... a1 a0 a0 a1 [...])
(... a2 a1 -- ... a2 a1 a1 a2 [...])
(... a0 -- ... a0 [a0 ...])
(... a1 -- ... a1 [a1 ...])
.. code:: ipython2
@ -2023,7 +1991,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])
(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])
.. code:: ipython2
@ -2037,7 +2005,7 @@ Clunky junk, but it will suffice for now.
.. parsed-literal::
((s0, (a0, (a1, s1))), (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1)))
((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
@ -2066,9 +2034,9 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
def Q(stack):
"""(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])"""
(s0, (a0, (a1, s1))) = stack
return (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1))
"""(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])"""
(s1, (a1, (a2, s2))) = stack
return (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2))
.. code:: ipython2
@ -2103,7 +2071,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
(a0 [.0.] -- a0)
(a1 [.1.] -- a1)
.. code:: ipython2
@ -2113,7 +2081,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
(a0 [.0.] -- [[a0 .0.] .1.])
(a1 [.1.] -- [[a1 .1.] .2.])
.. code:: ipython2
@ -2125,7 +2093,7 @@ comments are now already in the form needed for the Python code:
.. parsed-literal::
((s0, (a0, s1)), (a0, s0))
((s1, (a1, s2)), (a1, s1))
@ -2177,8 +2145,8 @@ Part VI: Multiple Stack Effects
.. parsed-literal::
(a1 -- a1 a1) (i1 i2 -- i3) (i0 -- i1)
(a1 -- a1 a1) (f1 f2 -- f3) (f0 -- f1)
(a1 -- a1 a1) (i1 i2 -- i3) (i1 -- i2)
(a1 -- a1 a1) (f1 f2 -- f3) (f1 -- f2)
.. code:: ipython2
@ -2197,18 +2165,6 @@ Part VI: Multiple Stack Effects
def MC(F, G):
return sorted(set(meta_compose(F, G)))
.. code:: ipython2
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
.. parsed-literal::
(f0 -- f1)
(i0 -- i1)
.. code:: ipython2
for f in MC([dup], [mul]):
@ -2217,7 +2173,19 @@ Part VI: Multiple Stack Effects
.. parsed-literal::
(n0 -- n1)
(n1 -- n2)
.. code:: ipython2
for f in MC([dup], muls):
print doc_from_stack_effect(*f)
.. parsed-literal::
(f1 -- f2)
(i1 -- i2)
Representing an Unbounded Sequence of Types
@ -2541,8 +2509,8 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(f0 -- f1)
(i0 -- i1)
(f1 -- f2)
(i1 -- i2)
.. code:: ipython2
@ -2555,7 +2523,7 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
([n0* .0.] -- [n0* .0.] n0)
([n1* .1.] -- [n1* .1.] n1)
.. code:: ipython2
@ -2568,8 +2536,8 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(a0 [.0.] -- n0)
(n0 [n0* .0.] -- n1)
(a1 [.1.] -- n1)
(n1 [n1* .1.] -- n2)
.. code:: ipython2
@ -2584,7 +2552,7 @@ This function has to be modified to yield multiple results.
.. parsed-literal::
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n0 [n0* .0.] -- n1)
(a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n1 [n1* .1.] -- n2)
.. code:: ipython2
@ -2826,6 +2794,19 @@ stack effect we have to "split universes" again and return both.
expression = l2s([n1, n2, mul])
.. code:: ipython2
expression
.. parsed-literal::
(n1, (n2, (mul, ())))
.. code:: ipython2
infer(expression)
@ -2835,74 +2816,97 @@ stack effect we have to "split universes" again and return both.
.. parsed-literal::
[]
[(s1, (f1, s1)), (s1, (i1, s1))]
.. code:: ipython2
class SymbolJoyType(AnyJoyType):
prefix = 'F'
def __init__(self, name, sec, number):
self.name = name
self.stack_effects = sec
self.number = number
class CombinatorJoyType(SymbolJoyType): prefix = 'C'
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
CONS = SymbolJoyType('cons', [cons], 23)
DIP = CombinatorJoyType('dip', [dip_t], 44)
def kav(F, e):
#i, stack = F
if not e:
return [(F, e)]
n, e = e
if isinstance(n, SymbolJoyType):
Fs = []
for sec in n.stack_effects:
Fs.extend(MC([F], sec))
return [kav(Fn, e) for Fn in Fs]
if isinstance(n, CombinatorJoyType):
res = []
for f in n.stack_effects:
s, e = f(F[1], e)
new_F = F[0], s
res.extend(kav(new_F, e))
return res
lit = S[0], (n, S[0])
return [kav(Fn, e) for Fn in MC([F], [lit])]
infer(expression)
.. parsed-literal::
[(s1, (f1, s1)), (s1, (i1, s1))]
compare, and be amazed:
.. code:: ipython2
def dip_t(stack, expression):
(quote, (a1, stack)) = stack
expression = stack_concat(quote, (a1, expression))
return stack, expression
for stack_effect_comment in infer(expression):
print doc_from_stack_effect(*stack_effect_comment)
.. parsed-literal::
(-- f1)
(-- i1)
.. code:: ipython2
def dip(stack, expression, dictionary):
(quote, (x, stack)) = stack
expression = (x, expression)
return stack, concat(quote, expression), dictionary
expression
.. parsed-literal::
(n1, (n2, (mul, ())))
.. code:: ipython2
infer(expression)
.. parsed-literal::
[(s1, (f1, s1)), (s1, (i1, s1))]
And that brings us to current Work-In-Progress. I'm pretty hopeful that
the mixed-mode inferencer/interpreter ``kav()`` function along with the
ability to specify multiple implementations for the combinators will
the mixed-mode inferencer/interpreter ``infer()`` function along with
the ability to specify multiple implementations for the combinators will
permit modelling of the stack effects of e.g. ``ifte``. If I can keep up
the pace I should be able to verify that conjecture by the end of June.
Conclusion
----------
(for now...)
Work remains to be done:
- the rest of the library has to be covered
- figure out how to deal with ``loop`` and ``genrec``, etc..
- extend the types to check values (see the appendix)
- other kinds of "higher order" type variables, OR, AND, etc..
- maybe rewrite in Prolog for great good?
- definitions
- don't permit composition of functions that don't compose
- auto-compile compilable functions
- Compiling more than just the Yin functions.
- getting better visibility (than Python debugger.)
- DOOOOCS!!!! Lots of docs!
- docstrings all around
- improve this notebook (it kinda falls apart at the end narratively. I
went off and just started writing code to see if it would work. It
does, but now I have to come back and describe here what I did.
I'm starting to realize that, with the inferencer/checker/compiler
coming along, and with the UI ready to be rewritten in Joy, I'm close to
a time when my ephasis is going to have to shift from crunchy code stuff
to squishy human stuff. I'm going to have to put normal people in front
of this and see if, in fact, they *can* learn the basics of programming
with it.
The rest of this stuff is junk and/or unfinished material.
Appendix: Joy in the Logical Paradigm
@ -2914,115 +2918,26 @@ For this to work the type label classes have to be modified to let
.. code:: ipython2
F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
def _ge(self, other):
return (issubclass(other.__class__, self.__class__)
or hasattr(self, 'accept')
and isinstance(other, self.accept))
print doc_from_stack_effect(*F)
AnyJoyType.__ge__ = _ge
AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
StackJoyType.accept = tuple
.. code:: ipython2
::
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-119-7fde90b4e88f> in <module>()
1 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
2
----> 3 print doc_from_stack_effect(*F)
F = infer(l2s((pop, swap, rolldown, rest, rest, cons, cons)))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
for f in F:
print doc_from_stack_effect(*f)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
.. parsed-literal::
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
<ipython-input-98-ddee30dbb1a6> in C(f, g)
10 def C(f, g):
11 f, g = relabel(f, g)
---> 12 for fg in compose(f, g):
13 yield delabel(fg)
<ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
1 def compose(f, g):
----> 2 (f_in, f_out), (g_in, g_out) = f, g
3 s = unify(g_in, f_out)
4 if not s:
5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
TypeError: 'SymbolJoyType' object is not iterable
([a4 a5 .1.] a3 a2 a1 -- [a2 a3 .1.])
.. code:: ipython2
@ -3031,26 +2946,140 @@ For this to work the type label classes have to be modified to let
.. code:: ipython2
s = text_to_expression('[3 4 ...] 2 1')
F = infer(l2s((pop, pop, pop)))
for f in F:
print doc_from_stack_effect(*f)
.. parsed-literal::
(a3 a2 a1 --)
.. code:: ipython2
s = text_to_expression('0 1 2')
s
.. parsed-literal::
(0, (1, (2, ())))
.. code:: ipython2
L = unify(F[1], s)
F[0][0]
.. parsed-literal::
(a1, (a2, (a3, s1)))
.. code:: ipython2
L = unify(s, F[0][0])
L
.. parsed-literal::
()
.. code:: ipython2
F[1]
s = text_to_expression('0 1 2 [3 4]')
s
.. parsed-literal::
(0, (1, (2, ((3, (4, ())), ()))))
.. code:: ipython2
F[0][0]
.. parsed-literal::
(a1, (a2, (a3, s1)))
.. code:: ipython2
L = unify(s, F[0][0])
L
.. parsed-literal::
()
.. code:: ipython2
L = unify(F[0][0], s)
L
.. parsed-literal::
()
.. code:: ipython2
F[1][0]
::
---------------------------------------------------------------------------
IndexError Traceback (most recent call last)
<ipython-input-133-58a8e44e9cba> in <module>()
----> 1 F[1][0]
IndexError: list index out of range
.. code:: ipython2
s[0]
.. code:: ipython2
A[1] >= 23
`Abstract Interpretation <https://en.wikipedia.org/wiki/Abstract_interpretation>`__
-----------------------------------------------------------------------------------

View File

@ -53,18 +53,17 @@ class TestCombinators(TestMixin, unittest.TestCase):
]
self.assertEqualTypeStructure(infr(expression), f)
def test_cons_dip(self):
expression = (cons, s0), dip # [cons] dip
# (a2 [...1] a1 -- [a2 ...1] a3)
f = (a1, (s1, (a2, s2))), (a1, ((a2, s1), s2))
# shouldn't a3 be a1?
self.assertEqualTypeStructure(infr(expression), [f])
def test_dip(self):
expression = dip,
f = ((s1, (a1, s2)), (a2, s2)) # (a1 [...1] -- a2)
self.assertEqualTypeStructure(infr(expression), [f])
def test_cons_dip(self):
expression = (cons, s0), dip # [cons] dip
# (a2 [...1] a1 -- [a2 ...1] a1)
f = (a1, (s1, (a2, s2))), (a1, ((a2, s1), s2))
self.assertEqualTypeStructure(infr(expression), [f])
def test_cons_dipd(self):
expression = a1, a3, (cons, s0), dipd
f = ((s0, (a0, s1)), (a1, (a2, ((a0, s0), s1))))
@ -169,4 +168,4 @@ class TestYin(TestMixin, unittest.TestCase):
if __name__ == '__main__':
unittest.main(defaultTest='TestCombinators.test_cons_dip')
unittest.main()