sforman/Thun
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A bit more text in the Types notebook.

Browse Source 
It's still pretty drafty.  I'm working on the code and then I'll write up
the last bit of docs.
This commit is contained in:
Simon Forman
2018-06-25 11:32:27 -07:00
parent f1979f35ce
commit 41d979b233
7 changed files with 1907 additions and 2348 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/Types.md
+243 -310
View File
@@ -1,7 +1,15 @@
# Type Inference
Cf. ["Type Inference in Stack-Based Programming Languages"](http://prl.ccs.neu.edu/blog/2017/03/10/type-inference-in-stack-based-programming-languages/) by Rob Kleffner, 2017-03-10.
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. 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
@@ -608,7 +616,7 @@ C(cons, uncons)
## Part III: Compiling Stack Functions
## Part III: Compiling Yin Functions
Now consider the Python function we would like to derive:
@@ -1361,7 +1369,7 @@ neato(roll_up, swap, roll_down)
```python
# e.g. [popop] dip
# e.g. [popop] dipd
neato(popdd, roll_down, pop)
```
@@ -1421,6 +1429,8 @@ print compile_('sqr', C(dup, mul))
return (n1, 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.)
#### `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:
@@ -1895,7 +1905,7 @@ While in the second it spawns an `A`, which we will label `e`:
w/ {d: e}
[ A* b .0.] U [ .1.]
w/ {.1.: A* b .0.}
[ A* b .0.] U [ .1.]
[ A* b .0.] U [ A* b .0.]
Giving us two unifiers:
@@ -2235,15 +2245,13 @@ for result in unify(a, b):
## Part VII: Typing Combinators
TBD
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:
This is an open subject.
i (... [.1.] -- ... .1.)
The obvious thing is that you now need two pairs of tuples to describe the combinators' effects, a stack effect comment and an expression effect comment:
Or
dip (a [F] --)--(-- F a)
One thing that might help is...
i (... [A* .1.] -- ... A*)
Consider the type of:
@@ -2258,210 +2266,9 @@ Obviously it would be:
(a1 [..1] -- ... then what?
Without any information about the contents of the quote we can't say much about the result.
```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)
```
(-- [F1 .2.])
```python
dip_a = ((W[1], S[2]), (A[1], S[0]))
```
```python
d = relabel(S[0], dip_a)
print doc_from_stack_effect(*d)
```
(-- a1001 [F1001 .1002.])
```python
s = list(unify(d[1], k[1]))[0]
s
```
{s0: (a1001, s1000), s1002: s2, F1001: F1}
```python
j = update(s, k)
```
```python
print doc_from_stack_effect(*j)
```
(a1001 -- a1001 [F1 .2.])
```python
j
```
((a1001, s1000), ((F1, s2), (a1001, s1000)))
```python
cons
```
((s1, (a1, s23)), ((a1, s1), s23))
```python
for f in MC([k], [dup]):
print doc_from_stack_effect(*f)
```
(-- [F0 .1.] [F0 .1.])
```python
l = S[0], ((cons, S[2]), (A[1], S[0]))
```
```python
print doc_from_stack_effect(*l)
```
(-- a1 [[[[.1.] a1 .23.] [a1 .1.] .23.] .2.])
```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]
```
```python
from joy.utils.stack import iter_stack
```
```python
a, b, c = dip_t(l)
```
```python
a
```
(s0, s0)
```python
b
```
((s1, (a1, s23)), ((a1, s1), s23))
```python
c
```
(s3, (a1, s3))
```python
MC([a], [b])
```
[((s0, (a0, s1)), ((a0, s0), s1))]
```python
kjs = MC(MC([a], [b]), [c])
kjs
```
[((s0, (a0, s1)), (a1, ((a0, s0), s1)))]
```python
print doc_from_stack_effect(*kjs[0])
```
(a0 [.0.] -- [a0 .0.] a1)
(a0 [.0.] -- [a0 .0.] a1)
a0 [.0.] a1 [cons] dip
----------------------------
[a0 .0.] a1
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. (Note: bug! If one branch doesn't type check the currect code ignores it, so you can think things are okay but have a type error waiting in the faled branch, I think... D'oh! FIXME!!!)
```python
@@ -2533,102 +2340,6 @@ And that brings us to current Work-In-Progress. I'm pretty hopeful that the mix
The rest of this stuff is junk and/or unfinished material.
### `concat`
How to deal with `concat`?
concat ([.0.] [.1.] -- [.0. .1.])
We would like to represent this in Python somehow...
```python
concat = (S[0], S[1]), ((S[0], S[1]),)
```
But this is actually `cons` with the first argument restricted to be a stack:
([.0.] [.1.] -- [[.0.] .1.])
What we have implemented so far would actually only permit:
([.0.] [.1.] -- [.2.])
```python
concat = (S[0], S[1]), (S[2],)
```
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)))
```python
class Astar(object):
def __repr__(self):
return 'A*'
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
```
```python
a, b = (A[1], S[0]), (A[2], S[1])
```
```python
concat(a, b)
```
(a1, (A*, (a2, s1)))
## 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`
@@ -2644,7 +2355,7 @@ print doc_from_stack_effect(*F)
ValueError Traceback (most recent call last)
<ipython-input-137-4b4cb6ff86e5> in <module>()
<ipython-input-112-4b4cb6ff86e5> in <module>()
1 F = reduce(C, (pop, swap, roll_down, rest, rest, cons, cons))
2
----> 3 print doc_from_stack_effect(*F)
@@ -2764,3 +2475,225 @@ s[0]
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]))
```
```python
d = relabel(S[0], dip_a)
print doc_from_stack_effect(*d)
```
```python
s = list(unify(d[1], k[1]))[0]
s
```
```python
j = update(s, k)
```
```python
print doc_from_stack_effect(*j)
```
```python
j
```
```python
cons
```
```python
for f in MC([k], [dup]):
print doc_from_stack_effect(*f)
```
```python
l = S[0], ((cons, S[2]), (A[1], S[0]))
```
```python
print doc_from_stack_effect(*l)
```
```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]
```
```python
from joy.utils.stack import iter_stack
```
```python
a, b, c = dip_t(l)
```
```python
a
```
```python
b
```
```python
c
```
```python
MC([a], [b])
```
```python
kjs = MC(MC([a], [b]), [c])
kjs
```
```python
print doc_from_stack_effect(*kjs[0])
```
(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...
```python
concat = (S[0], S[1]), ((S[0], S[1]),)
```
But this is actually `cons` with the first argument restricted to be a stack:
([.0.] [.1.] -- [[.0.] .1.])
What we have implemented so far would actually only permit:
([.0.] [.1.] -- [.2.])
```python
concat = (S[0], S[1]), (S[2],)
```
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)))
```python
class Astar(object):
def __repr__(self):
return 'A*'
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
```
```python
a, b = (A[1], S[0]), (A[2], S[1])
```
```python
concat(a, b)
```