+# The Blissful Elegance of Typing Joy
-# Type Inference
+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.)
-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.
+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.)
-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...
## Part I: Pöial's Rules
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 ...] -- [...] )
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
+ else:
+ s = False
- return False
+ return s
```
### `update()`
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)
+ else:
+ s = False
+
+ return s
```
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]
- (((a0,), (a0, a0)), ((n0, n1), (n2,)))
+ (((a1,), (a1, a1)), ((n1, n2), (n3,)))
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)
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.])
- ((n0,), (n1,))
+ ((n1,), (n2,))
- (((a0, (a1, s0)), a2, a3, a4), ((a3, (a2, s0)),))
+ (((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
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.
neato(rollup, swap, rolldown)
```
- (a0 a1 a2 -- a1 a0 a2)
+ (a1 a2 a3 -- a2 a1 a3)
neato(popdd, rolldown, pop)
```
- (a0 a1 a2 a3 -- a2 a3)
+ (a1 a2 a3 a4 -- a3 a4)
neato(rollup, swap)
```
- (a0 a1 a2 -- a2 a1 a0)
+ (a1 a2 a3 -- a3 a2 a1)
#### `compile_()` version 2
```
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:
```
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.)
+(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. `n2 = mul(n1, n1)` for `mul` with the right variable names and insert it in the right place. 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.)
#### `compilable()`
The functions that *can* be compiled are the ones that have only `AnyJoyType` and `StackJoyType` labels in their stack effect comments. We can write a function to check that:
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)
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.])
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
- ((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))))))
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)
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.])
```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 ...])
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.] ...])
- ((s0, (a0, (a1, s1))), (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1)))
+ ((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
```
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))
```python
+
+```
+
+
+```python
+
+```
+
+
+```python
+
+```
+
+
+```python
+
+```
+
+
+```python
+
+```
+
+
+```python
unstack = (S[1], S[0]), S[1]
enstacken = S[0], (S[0], S[1])
```
print doc_from_stack_effect(*C(cons, unstack))
```
- (a0 [.0.] -- a0)
+ (a1 [.1.] -- a1)
print doc_from_stack_effect(*C(cons, enstacken))
```
- (a0 [.0.] -- [[a0 .0.] .1.])
+ (a1 [.1.] -- [[a1 .1.] .2.])
- ((s0, (a0, s1)), (a0, s0))
+ ((s1, (a1, s2)), (a1, s1))
+
+```python
+
+```
+
## Part VI: Multiple Stack Effects
...
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)
```python
-for f in MC([dup], muls):
+for f in MC([dup], [mul]):
print doc_from_stack_effect(*f)
```
- (f0 -- f1)
- (i0 -- i1)
+ (n1 -- n2)
```python
-for f in MC([dup], [mul]):
+for f in MC([dup], muls):
print doc_from_stack_effect(*f)
```
- (n0 -- n1)
+ (f1 -- f2)
+ (i1 -- i2)
### Representing an Unbounded Sequence of Types
```python
+
+```
+
+
+```python
def meta_compose(F, G):
for f, g in product(F, G):
try:
print doc_from_stack_effect(*f)
```
- (f0 -- f1)
- (i0 -- i1)
+ (f1 -- f2)
+ (i1 -- i2)
print doc_from_stack_effect(*f)
```
- ([n0* .0.] -- [n0* .0.] n0)
+ ([n1* .1.] -- [n1* .1.] n1)
print doc_from_stack_effect(*f)
```
- (a0 [.0.] -- n0)
- (n0 [n0* .0.] -- n1)
+ (a1 [.1.] -- n1)
+ (n1 [n1* .1.] -- n2)
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)
## Part VII: Typing Combinators
-In order to compute the stack effect of combinators you kinda have to have the quoted programs they expect available. In the most general case, the `i` combinator, you can't say anything about it's stack effect other than it expects one quote:
+In order to compute the stack effect of combinators you kinda have to have the quoted programs they expect available. In the most general case, the `i` combinator, you can't say anything about its stack effect other than it expects one quote:
i (... [.1.] -- ... .1.)
Without any information about the contents of the quote we can't say much about the result.
-I think there's a way forward. If we convert our list of terms we are composing into a stack structure we can use it as a *Joy expression*, then we can treat the *output half* of a function's stack effect comment as a Joy interpreter stack, and just execute combinators directly. We can hybridize the compostition function with an interpreter to evaluate combinators, compose non-combinator functions, and put type variables on the stack. For combinators like `branch` that can have more than one stack effect we have to "split universes" again and return both.
+### Hybrid Inferencer/Interpreter
+I think there's a way forward. If we convert our list (of terms we are composing) into a stack structure we can use it as a *Joy expression*, then we can treat the *output half* of a function's stack effect comment as a Joy interpreter stack, and just execute combinators directly. We can hybridize the compostition function with an interpreter to evaluate combinators, compose non-combinator functions, and put type variables on the stack. For combinators like `branch` that can have more than one stack effect we have to "split universes" again and return both.
+
+#### Joy Types for Functions
+We need a type variable for Joy functions that can go in our expressions and be used by the hybrid inferencer/interpreter. They have to store a name and a list of stack effects.
```python
def __repr__(self):
return self.name
-
-
-class SymbolJoyType(FunctionJoyType): prefix = 'F'
-class CombinatorJoyType(FunctionJoyType): prefix = 'C'
-
-
-
-```
-
-
-```python
-def flatten(g):
- return list(chain.from_iterable(g))
-
-
-ID = S[0], S[0] # Identity function.
-
-
-def infer(e, F=ID):
- if not e:
- return [F]
-
- n, e = e
-
- if isinstance(n, SymbolJoyType):
- res = flatten(infer(e, Fn) for Fn in MC([F], n.stack_effects))
-
- elif isinstance(n, CombinatorJoyType):
- res = []
- for combinator in n.stack_effects:
- fi, fo = F
- new_fo, ee, _ = combinator(fo, e, {})
- ee = update(FUNCTIONS, ee) # Fix Symbols.
- new_F = fi, new_fo
- res.extend(infer(ee, new_F))
- else:
- lit = s9, (n, s9)
- res = flatten(infer(e, Fn) for Fn in MC([F], [lit]))
-
- return res
-
-
```
-
-```python
-f0, f1, f2, f3, f4, f5, f6, f7, f8, f9 = F = map(FloatJoyType, _R)
-i0, i1, i2, i3, i4, i5, i6, i7, i8, i9 = I = map(IntJoyType, _R)
-n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 = N
-s0, s1, s2, s3, s4, s5, s6, s7, s8, s9 = S
-```
+#### Specialized for Simple Functions and Combinators
+For non-combinator functions the stack effects list contains stack effect comments (represented by pairs of cons-lists as described above.)
```python
-import joy.library
-
-FNs = '''ccons cons divmod_ dup dupd first
- over pm pop popd popdd popop pred
- rest rolldown rollup rrest second
- sqrt stack succ swaack swap swons
- third tuck uncons'''
-
-FUNCTIONS = {
- name: SymbolJoyType(name, [NEW_DEFS[name]], i)
- for i, name in enumerate(FNs.strip().split())
- }
-FUNCTIONS['sum'] = SymbolJoyType('sum', [(((Ns[1], s1), s0), (n0, s0))], 100)
-FUNCTIONS['mul'] = SymbolJoyType('mul', [
- ((i2, (i1, s0)), (i3, s0)),
- ((f2, (i1, s0)), (f3, s0)),
- ((i2, (f1, s0)), (f3, s0)),
- ((f2, (f1, s0)), (f3, s0)),
-], 101)
-FUNCTIONS.update({
- combo.__name__: CombinatorJoyType(combo.__name__, [combo], i)
- for i, combo in enumerate((
- joy.library.i,
- joy.library.dip,
- joy.library.dipd,
- joy.library.dipdd,
- joy.library.dupdip,
- joy.library.b,
- joy.library.x,
- joy.library.infra,
- ))
- })
-
-def branch_true(stack, expression, dictionary):
- (then, (else_, (flag, stack))) = stack
- return stack, CONCAT(then, expression), dictionary
-
-def branch_false(stack, expression, dictionary):
- (then, (else_, (flag, stack))) = stack
- return stack, CONCAT(else_, expression), dictionary
-
-FUNCTIONS['branch'] = CombinatorJoyType('branch', [branch_true, branch_false], 100)
-```
-
-
-```python
-globals().update(FUNCTIONS)
-```
-
-
-```python
-from itertools import chain
-from joy.utils.stack import list_to_stack as l2s
-```
-
-
-```python
-expression = l2s([n1, n2, (mul, s2), (stack, s3), dip, infra, first])
-```
-
-
-```python
-expression
-```
-
-
-
-
- (n1, (n2, ((mul, s2), ((stack, s3), (dip, (infra, (first, ())))))))
-
-
-
-
-```python
-expression = l2s([n1, n2, mul])
-```
-
-
-```python
-infer(expression)
-```
-
-
-
-
- []
-
-
-
-
-```python
-class SymbolJoyType(AnyJoyType):
+class SymbolJoyType(FunctionJoyType):
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])]
-
-```
-
-compare, and be amazed:
-
-
-```python
-def dip_t(stack, expression):
- (quote, (a1, stack)) = stack
- expression = stack_concat(quote, (a1, expression))
- return stack, expression
-```
-
-
-```python
-def dip(stack, expression, dictionary):
- (quote, (x, stack)) = stack
- expression = (x, expression)
- return stack, concat(quote, expression), dictionary
-```
-
-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.
-
-The rest of this stuff is junk and/or unfinished material.
-
-## Appendix: Joy in the Logical Paradigm
-For this to work the type label classes have to be modified to let `T >= t` succeed, where e.g. `T` is `IntJoyType` and `t` is `int`
-
-
-```python
-F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
-
-print doc_from_stack_effect(*F)
```
-
- ---------------------------------------------------------------------------
-
- 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)
-
-
- <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
-
-
-
-```python
-from joy.parser import text_to_expression
-```
-
-
-```python
-s = text_to_expression('[3 4 ...] 2 1')
-s
-```
-
-
-```python
-L = unify(F[1], s)
-L
-```
-
-
-```python
-F[1]
-```
-
-
-```python
-F[1][0]
-```
-
-
-```python
-s[0]
-```
-
-## [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.
-
-
-## Junk
-
-
-```python
-class SymbolJoyType(AnyJoyType): prefix = 'F'
-
-W = map(SymbolJoyType, _R)
-
-k = S[0], ((W[1], S[2]), S[0])
-Symbol('cons')
-print doc_from_stack_effect(*k)
-
-```
-
-
-```python
-dip_a = ((W[1], S[2]), (A[1], S[0]))
-```
+For combinators the list contains Python functions.
```python
-d = relabel(S[0], dip_a)
-print doc_from_stack_effect(*d)
-```
-
+class CombinatorJoyType(FunctionJoyType):
-```python
-s = list(unify(d[1], k[1]))[0]
-s
-```
+ prefix = 'C'
+ def __init__(self, name, sec, number, expect=None):
+ super(CombinatorJoyType, self).__init__(name, sec, number)
+ self.expect = expect
-```python
-j = update(s, k)
+ def enter_guard(self, f):
+ if self.expect is None:
+ return f
+ g = self.expect, self.expect
+ new_f = list(compose(f, g, ()))
+ assert len(new_f) == 1, repr(new_f)
+ return new_f[0][1]
```
-
-```python
-print doc_from_stack_effect(*j)
-```
+For simple combinators that have only one effect (like ``dip``) you only need one function and it can be the combinator itself.
```python
-j
-```
-
+import joy.library
-```python
-cons
+dip = CombinatorJoyType('dip', [joy.library.dip], 23)
```
-
-```python
-for f in MC([k], [dup]):
- print doc_from_stack_effect(*f)
-```
+For combinators that can have more than one effect (like ``branch``) you have to write functions that each implement the action of one of the effects.
```python
-l = S[0], ((cons, S[2]), (A[1], S[0]))
-```
+def branch_true(stack, expression, dictionary):
+ (then, (else_, (flag, stack))) = stack
+ return stack, concat(then, expression), dictionary
+def branch_false(stack, expression, dictionary):
+ (then, (else_, (flag, stack))) = stack
+ return stack, concat(else_, expression), dictionary
-```python
-print doc_from_stack_effect(*l)
+branch = CombinatorJoyType('branch', [branch_true, branch_false], 100)
```
+You can also provide an optional stack effect, input-side only, that will then be used as an identity function (that accepts and returns stacks that match the "guard" stack effect) which will be used to guard against type mismatches going into the evaluation of the combinator.
-```python
-
-def dip_t(F):
- (quote, (a1, sec)) = F[1]
- G = F[0], sec
- P = S[3], (a1, S[3])
- a = [P]
- while isinstance(quote, tuple):
- term, quote = quote
- a.append(term)
- a.append(G)
- return a[::-1]
-
+#### `infer()`
+With those in place, we can define a function that accepts a sequence of Joy type variables, including ones representing functions (not just values), and attempts to grind out all the possible stack effects of that expression.
-
-
-```
+One tricky thing is that type variables *in the expression* have to be updated along with the stack effects after doing unification or we risk losing useful information. This was a straightforward, if awkward, modification to the call structure of `meta_compose()` et. al.
```python
-from joy.utils.stack import iter_stack
-```
+ID = S[0], S[0] # Identity function.
-```python
-a, b, c = dip_t(l)
-```
+def infer(*expression):
+ return sorted(set(_infer(list_to_stack(expression))))
-```python
-a
-```
+def _infer(e, F=ID):
+ _log_it(e, F)
+ if not e:
+ return [F]
+ n, e = e
-```python
-b
-```
+ if isinstance(n, SymbolJoyType):
+ eFG = meta_compose([F], n.stack_effects, e)
+ res = flatten(_infer(e, Fn) for e, Fn in eFG)
+ elif isinstance(n, CombinatorJoyType):
+ fi, fo = n.enter_guard(F)
+ res = flatten(_interpret(f, fi, fo, e) for f in n.stack_effects)
-```python
-c
-```
+ elif isinstance(n, Symbol):
+ assert n not in FUNCTIONS, repr(n)
+ func = joy.library._dictionary[n]
+ res = _interpret(func, F[0], F[1], e)
+ else:
+ fi, fo = F
+ res = _infer(e, (fi, (n, fo)))
-```python
-MC([a], [b])
-```
+ return res
-```python
-kjs = MC(MC([a], [b]), [c])
-kjs
-```
+def _interpret(f, fi, fo, e):
+ new_fo, ee, _ = f(fo, e, {})
+ ee = update(FUNCTIONS, ee) # Fix Symbols.
+ new_F = fi, new_fo
+ return _infer(ee, new_F)
-```python
-print doc_from_stack_effect(*kjs[0])
+def _log_it(e, F):
+ _log.info(
+ u'%3i %s ∘ %s',
+ len(inspect_stack()),
+ doc_from_stack_effect(*F),
+ expression_to_string(e),
+ )
```
- (a0 [.0.] -- [a0 .0.] a1)
-
- a0 [.0.] a1 [cons] dip
- ----------------------------
- [a0 .0.] a1
-
-### `concat`
-
-How to deal with `concat`?
-
- concat ([.0.] [.1.] -- [.0. .1.])
-
-We would like to represent this in Python somehow...
+#### Work in Progress
+And that brings us to current Work-In-Progress. The mixed-mode inferencer/interpreter `infer()` function seems to work well. There are details I should document, and the rest of the code in the `types` module (FIXME link to its docs here!) should be explained... There is cruft to convert the definitions in `DEFS` to the new `SymbolJoyType` objects, and some combinators. Here is an example of output from the current code :
```python
-concat = (S[0], S[1]), ((S[0], S[1]),)
-```
+1/0 # (Don't try to run this cell! It's not going to work. This is "read only" code heh..)
-But this is actually `cons` with the first argument restricted to be a stack:
+logging.basicConfig(format='%(message)s', stream=sys.stdout, level=logging.INFO)
- ([.0.] [.1.] -- [[.0.] .1.])
-
-What we have implemented so far would actually only permit:
+globals().update(FUNCTIONS)
- ([.0.] [.1.] -- [.2.])
+h = infer((pred, s2), (mul, s3), (div, s4), (nullary, (bool, s5)), dipd, branch)
+print '-' * 40
-```python
-concat = (S[0], S[1]), (S[2],)
+for fi, fo in h:
+ print doc_from_stack_effect(fi, fo)
```
-
-Which works but can lose information. Consider `cons concat`, this is how much information we *could* retain:
-
- (1 [.0.] [.1.] -- [1 .0. .1.])
-As opposed to just:
-
- (1 [.0.] [.1.] -- [.2.])
-
-### represent `concat`
-
- ([.0.] [.1.] -- [A*(.0.) .1.])
-
-Meaning that `A*` on the right-hand side should all the crap from `.0.`.
-
- ([ .0.] [.1.] -- [ A* .1.])
- ([a .0.] [.1.] -- [a A* .1.])
- ([a b .0.] [.1.] -- [a b A* .1.])
- ([a b c .0.] [.1.] -- [a b c A* .1.])
-
-
-
-or...
-
- ([ .0.] [.1.] -- [ .1.])
- ([a .0.] [.1.] -- [a .1.])
- ([a b .0.] [.1.] -- [a b .1.])
- ([a b c .0.] [.1.] -- [a b c .1.])
- ([a A* c .0.] [.1.] -- [a A* c .1.])
-
-
+ ---------------------------------------------------------------------------
- (a, (b, S0)) . S1 = (a, (b, (A*, S1)))
+ ZeroDivisionError Traceback (most recent call last)
+ <ipython-input-1-9a9d60354c35> in <module>()
+ ----> 1 1/0 # (Don't try to run this cell! It's not going to work. This is "read only" code heh..)
+ 2
+ 3 logging.basicConfig(format='%(message)s', stream=sys.stdout, level=logging.INFO)
+ 4
+ 5 globals().update(FUNCTIONS)
+
+
+ ZeroDivisionError: integer division or modulo by zero
+
+
+The numbers at the start of the lines are the current depth of the Python call stack. They're followed by the current computed stack effect (initialized to `ID`) then the pending expression (the inference of the stack effect of which is the whole object of the current example.)
+
+In this example we are implementing (and inferring) `ifte` as `[nullary bool] dipd branch` which shows off a lot of the current implementation in action.
+
+ 7 (--) ∘ [pred] [mul] [div] [nullary bool] dipd branch
+ 8 (-- [pred ...2]) ∘ [mul] [div] [nullary bool] dipd branch
+ 9 (-- [pred ...2] [mul ...3]) ∘ [div] [nullary bool] dipd branch
+ 10 (-- [pred ...2] [mul ...3] [div ...4]) ∘ [nullary bool] dipd branch
+ 11 (-- [pred ...2] [mul ...3] [div ...4] [nullary bool ...5]) ∘ dipd branch
+ 15 (-- [pred ...5]) ∘ nullary bool [mul] [div] branch
+ 19 (-- [pred ...2]) ∘ [stack] dinfrirst bool [mul] [div] branch
+ 20 (-- [pred ...2] [stack ]) ∘ dinfrirst bool [mul] [div] branch
+ 22 (-- [pred ...2] [stack ]) ∘ dip infra first bool [mul] [div] branch
+ 26 (--) ∘ stack [pred] infra first bool [mul] [div] branch
+ 29 (... -- ... [...]) ∘ [pred] infra first bool [mul] [div] branch
+ 30 (... -- ... [...] [pred ...1]) ∘ infra first bool [mul] [div] branch
+ 34 (--) ∘ pred s1 swaack first bool [mul] [div] branch
+ 37 (n1 -- n2) ∘ [n1] swaack first bool [mul] [div] branch
+ 38 (... n1 -- ... n2 [n1 ...]) ∘ swaack first bool [mul] [div] branch
+ 41 (... n1 -- ... n1 [n2 ...]) ∘ first bool [mul] [div] branch
+ 44 (n1 -- n1 n2) ∘ bool [mul] [div] branch
+ 47 (n1 -- n1 b1) ∘ [mul] [div] branch
+ 48 (n1 -- n1 b1 [mul ...1]) ∘ [div] branch
+ 49 (n1 -- n1 b1 [mul ...1] [div ...2]) ∘ branch
+ 53 (n1 -- n1) ∘ div
+ 56 (f2 f1 -- f3) ∘
+ 56 (i1 f1 -- f2) ∘
+ 56 (f1 i1 -- f2) ∘
+ 56 (i2 i1 -- f1) ∘
+ 53 (n1 -- n1) ∘ mul
+ 56 (f2 f1 -- f3) ∘
+ 56 (i1 f1 -- f2) ∘
+ 56 (f1 i1 -- f2) ∘
+ 56 (i2 i1 -- i3) ∘
+ ----------------------------------------
+ (f2 f1 -- f3)
+ (i1 f1 -- f2)
+ (f1 i1 -- f2)
+ (i2 i1 -- f1)
+ (i2 i1 -- i3)
+
+## Conclusion
+We built a simple type inferencer, and a kind of crude "compiler" for a subset of Joy functions. Then we built a more powerful inferencer that actually does some evaluation and explores branching code paths
+
+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.
-```python
-class Astar(object):
- def __repr__(self):
- return 'A*'
+## Appendix: Joy in the Logical Paradigm
+For *type checking* to work the type label classes have to be modified to let `T >= t` succeed, where e.g. `T` is `IntJoyType` and `t` is `int`. If you do that you can take advantage of the *logical relational* nature of the stack effect comments to "compute in reverse" as it were. There's a working demo of this at the end of the `types` module. But if you're interested in all that you should just use Prolog!
-def concat(s0, s1):
- a = []
- while isinstance(s0, tuple):
- term, s0 = s0
- a.append(term)
- assert isinstance(s0, StackJoyType), repr(s0)
- s1 = Astar(), s1
- for term in reversed(a):
- s1 = term, s1
- return s1
-```
+Anyhow, type *checking* is a few easy steps away.
```python
-a, b = (A[1], S[0]), (A[2], S[1])
-```
+def _ge(self, other):
+ return (issubclass(other.__class__, self.__class__)
+ or hasattr(self, 'accept')
+ and isinstance(other, self.accept))
-
-```python
-concat(a, b)
+AnyJoyType.__ge__ = _ge
+AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
+StackJoyType.accept = tuple
```
OSDN Git Service
