4 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.
6 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.
8 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.)
10 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.
12 Anyhow, here's type inference...
14 ## Part I: Pöial's Rules
16 ["Typing Tools for Typeless Stack Languages" by Jaanus Pöial
17 ](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.212.6026)
19 @INPROCEEDINGS{Pöial06typingtools,
20 author = {Jaanus Pöial},
21 title = {Typing tools for typeless stack languages},
22 booktitle = {In 23rd Euro-Forth Conference},
28 This rule deals with functions (and literals) that put items on the stack `(-- d)`:
36 This rule deals with functions that consume items from the stack `(a --)`:
43 The third rule is actually two rules. These two rules deal with composing functions when the second one will consume one of items the first one produces. The two types must be [*unified*](https://en.wikipedia.org/wiki/Robinson's_unification_algorithm) or a type conflict declared.
45 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
46 -------------------------------
47 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
50 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
51 -------------------------------
52 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
54 Let's work through some examples by hand to develop an intuition for the algorithm.
56 There's a function in one of the other notebooks.
58 F == pop swap roll< rest rest cons cons
60 It's all "stack chatter" and list manipulation so we should be able to deduce its type.
62 ### Stack Effect Comments
63 Joy function types will be represented by Forth-style stack effect comments. I'm going to use numbers instead of names to keep track of the stack arguments. (A little bit like [De Bruijn index](https://en.wikipedia.org/wiki/De_Bruijn_index), at least it reminds me of them):
69 roll< (1 2 3 -- 2 3 1)
71 These commands alter the stack but don't "look at" the values so these numbers represent an "Any type".
77 Here we encounter a complication. The argument numbers need to be made unique among both sides. For this let's change `pop` to use 0:
81 Following the second rule:
87 (1 2 0 -- 2 1) (1 2 3 -- 2 3 1)
91 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
93 Now we follow the rules.
95 We must unify `1a` and `3b`, and `2a` and `2b`, replacing the terms in the forms:
97 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
99 (3b 2a 0a -- 2a ) (1b 2b -- 2b 3b 1b)
101 (3b 2b 0a -- ) (1b -- 2b 3b 1b)
103 Here we must apply the second rule:
105 (3b 2b 0a --) (1b -- 2b 3b 1b)
106 -----------------------------------
107 (1b 3b 2b 0a -- 2b 3b 1b)
109 Now we de-label the type, uh, labels:
111 (1b 3b 2b 0a -- 2b 3b 1b)
122 And now we have the stack effect comment for `pop∘swap∘roll<`.
124 ### Compiling `pop∘swap∘roll<`
125 The simplest way to "compile" this function would be something like:
130 return rolldown(*swap(*pop(s, e, d)))
133 However, internally this function would still be allocating tuples (stack cells) and doing other unnecesssary work.
135 Looking ahead for a moment, from the stack effect comment:
139 We should be able to directly write out a Python function like:
144 (_, (a, (b, (c, stack)))) = stack
145 return (c, (b, (a, stack)))
148 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.
150 ### Functions on Lists
151 These are slightly tricky.
153 rest ( [1 ...] -- [...] )
155 cons ( 1 [...] -- [1 ...] )
157 ### `pop∘swap∘roll< rest`
159 (1 2 3 0 -- 3 2 1) ([1 ...] -- [...])
161 Re-label (instead of adding left and right tags I'm just taking the next available index number for the right-side stack effect comment):
163 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
167 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
169 ([4 ...] 2 3 0 -- 3 2 ) ( -- [...])
171 Apply the first rule:
173 ([4 ...] 2 3 0 -- 3 2) (-- [...])
174 ---------------------------------------
175 ([4 ...] 2 3 0 -- 3 2 [...])
179 ### `pop∘swap∘roll<∘rest rest`
183 ([4 ...] 2 3 0 -- 3 2 [...]) ([1 ...] -- [...])
185 Re-label (the tails of the lists on each side each get their own label):
187 ([4 .0.] 2 3 0 -- 3 2 [.0.]) ([5 .1.] -- [.1.])
189 Unify and update (note the opening square brackets have been omited in the substitution dict, this is deliberate and I'll explain below):
191 ([4 .0.] 2 3 0 -- 3 2 [.0.] ) ([5 .1.] -- [.1.])
193 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
195 How do we find `.0.]` in `[4 .0.]` and replace it with `5 .1.]` getting the result `[4 5 .1.]`? This might seem hard, but because the underlying structure of the Joy list is a cons-list in Python it's actually pretty easy. I'll explain below.
197 Next we unify and find our two terms are the same already: `[5 .1.]`:
199 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
203 ([4 5 .1.] 2 3 0 -- 3 2) (-- [.1.])
205 From here we apply the first rule and get:
207 ([4 5 .1.] 2 3 0 -- 3 2 [.1.])
209 Cleaning up the labels:
211 ([4 5 ...] 2 3 1 -- 3 2 [...])
213 This is the stack effect of `pop∘swap∘roll<∘rest∘rest`.
215 ### `pop∘swap∘roll<∘rest∘rest cons`
217 ([4 5 ...] 2 3 1 -- 3 2 [...]) (1 [...] -- [1 ...])
221 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
225 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
227 ([4 5 .2.] 2 3 1 -- 3 2 ) (6 -- [6 .2.])
229 ([4 5 .2.] 6 3 1 -- 3 ) ( -- [6 .2.])
233 ([4 5 .2.] 6 3 1 -- 3 [6 .2.])
237 ([4 5 ...] 2 3 1 -- 3 [2 ...])
241 ### `pop∘swap∘roll<∘rest∘rest∘cons cons`
244 ([4 5 ...] 2 3 1 -- 3 [2 ...]) (1 [...] -- [1 ...])
248 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.])
252 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.] )
254 ([4 5 .1.] 2 3 1 -- 3 ) (6 -- [6 2 .1.])
256 ([4 5 .1.] 2 6 1 -- ) ( -- [6 2 .1.])
258 First or second rule:
260 ([4 5 .1.] 2 6 1 -- [6 2 .1.])
264 ([4 5 ...] 2 3 1 -- [3 2 ...])
266 And there you have it, the stack effect for `pop∘swap∘roll<∘rest∘rest∘cons∘cons`.
268 ([4 5 ...] 2 3 1 -- [3 2 ...])
270 From this stack effect comment it should be possible to construct the following Python code:
275 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
276 return (d, (c, S0)), stack
279 ## Part II: Implementation
281 ### Representing Stack Effect Comments in Python
283 I'm going to use pairs of tuples of type descriptors, which will be integers or tuples of type descriptors:
287 roll_dn = (1, 2, 3), (2, 3, 1)
291 swap = (1, 2), (2, 1)
300 (f_in, f_out), (g_in, g_out) = f, g
305 # ---------------------
310 fg_in, fg_out = f_in, f_out + g_out
315 # ---------------------
320 fg_in, fg_out = g_in + f_in, g_out
322 else: # Unify, update, recur.
324 fo, gi = f_out[-1], g_in[-1]
328 if s == False: # s can also be the empty dict, which is ok.
329 raise TypeError('Cannot unify %r and %r.' % (fo, gi))
331 f_g = (f_in, f_out[:-1]), (g_in[:-1], g_out)
333 if s: f_g = update(s, f_g)
335 fg_in, fg_out = compose(*f_g)
344 def unify(u, v, s=None):
351 if isinstance(u, int):
355 if isinstance(v, int):
367 if not isinstance(term, tuple):
368 return s.get(term, term)
369 return tuple(update(s, inner) for inner in term)
376 def relabel(left, right):
377 return left, _1000(right)
380 if not isinstance(right, tuple):
382 return tuple(_1000(n) for n in right)
390 (((1,), ()), ((1001, 1002), (1002, 1001)))
399 s = {u: i for i, u in enumerate(sorted(_unique(f)))}
402 def _unique(f, seen=None):
405 if not isinstance(f, tuple):
412 delabel(relabel(pop, swap))
418 (((0,), ()), ((1, 2), (2, 1)))
424 At last we put it all together in a function `C()` that accepts two stack effect comments and returns their composition (or raises and exception if they can't be composed due to type conflicts.)
450 C(C(pop, swap), roll_dn)
456 ((3, 1, 2, 0), (2, 1, 3))
468 ((2, 0, 1), (1, 0, 2))
474 C(pop, C(swap, roll_dn))
480 ((3, 1, 2, 0), (2, 1, 3))
486 poswrd = reduce(C, (pop, swap, roll_dn))
493 ((3, 1, 2, 0), (2, 1, 3))
498 Here's that trick to represent functions like `rest` and `cons` that manipulate stacks. We use a cons-list of tuples and give the tails their own numbers. Then everything above already works.
502 rest = ((1, 2),), (2,)
504 cons = (1, 2), ((1, 2),)
515 (((3, 4), 1, 2, 0), (2, 1, 4))
519 Compare this to the stack effect comment we wrote above:
521 (( (3, 4), 1, 2, 0 ), ( 2, 1, 4 ))
522 ( [4 ...] 2 3 0 -- 3 2 [...])
524 The translation table, if you will, would be:
536 F = reduce(C, (pop, swap, roll_dn, rest, rest, cons, cons))
544 (((3, (4, 5)), 1, 2, 0), ((2, (1, 5)),))
548 Compare with the stack effect comment and you can see it works fine:
550 ([4 5 ...] 2 3 1 -- [3 2 ...])
553 ### Dealing with `cons` and `uncons`
554 However, if we try to compose e.g. `cons` and `uncons` it won't work:
558 uncons = ((1, 2),), (1, 2)
569 Cannot unify (1, 2) and (1001, 1002).
572 #### `unify()` version 2
573 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:
577 def unify(u, v, s=None):
587 if isinstance(u, int):
591 if isinstance(v, int):
595 if isinstance(u, tuple) and isinstance(v, tuple):
596 if len(u) != len(v) != 2:
597 raise ValueError(repr((u, v)))
598 for uu, vv in zip(u, v):
600 if s == False: # (instead of a substitution dict.)
619 ## Part III: Compiling Yin Functions
620 Now consider the Python function we would like to derive:
625 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
626 return (d, (c, S0)), stack
629 And compare it to the input stack effect comment tuple we just computed:
639 ((3, (4, 5)), 1, 2, 0)
643 The stack-de-structuring tuple has nearly the same form as our input stack effect comment tuple, just in the reverse order:
645 (_, (d, (c, ((a, (b, S0)), stack))))
647 Remove the punctuation:
651 Reverse the order and compare:
654 ((3, (4, 5 )), 1, 2, 0)
672 is similar to the output stack effect comment tuple:
674 ((d, (c, S0)), stack)
677 This should make it pretty easy to write a Python function that accepts the stack effect comment tuples and returns a new Python function (either as a string of code or a function object ready to use) that performs the semantics of that Joy function (described by the stack effect.)
679 ### Python Identifiers
680 We want to substitute Python identifiers for the integers. I'm going to repurpose `joy.parser.Symbol` class for this:
684 from collections import defaultdict
685 from joy.parser import Symbol
689 I = iter(xrange(1000))
690 return lambda: Symbol('a%i' % next(I))
693 def identifiers(term, s=None):
695 s = defaultdict(_names_for())
696 if isinstance(term, int):
698 return tuple(identifiers(inner, s) for inner in term)
701 ### `doc_from_stack_effect()`
702 As a convenience I've implemented a function to convert the Python stack effect comment tuples to reasonable text format. There are some details in how this code works that related to stuff later in the notebook, so you should skip it for now and read it later if you're interested.
706 def doc_from_stack_effect(inputs, outputs):
707 return '(%s--%s)' % (
708 ' '.join(map(_to_str, inputs + ('',))),
709 ' '.join(map(_to_str, ('',) + outputs))
714 if not isinstance(term, tuple):
716 t = term.prefix == 's'
717 except AttributeError:
719 return '[.%i.]' % term.number if t else str(term)
722 while term and isinstance(term, tuple):
724 a.append(_to_str(item))
728 except AttributeError:
731 if term.prefix != 's':
732 raise ValueError('Stack label: %s' % (term,))
734 a.append('.%s.' % (n,))
735 return '[%s]' % ' '.join(a)
739 Now we can write a compiler function to emit Python source code. (The underscore suffix distiguishes it from the built-in `compile()` function.)
743 def compile_(name, f, doc=None):
745 doc = doc_from_stack_effect(*f)
746 inputs, outputs = identifiers(f)
747 i = o = Symbol('stack')
752 return '''def %s(stack):
755 return %s''' % (name, doc, i, o)
758 Here it is in action:
762 source = compile_('F', F)
768 """([3 4 .5.] 1 2 0 -- [2 1 .5.])"""
769 (a5, (a4, (a3, ((a0, (a1, a2)), stack)))) = stack
770 return ((a4, (a3, a2)), stack)
778 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
779 return ((d, (c, S0)), stack)
788 eval(compile(source, '__main__', 'single'), {}, L)
804 from notebook_preamble import D, J, V
805 from joy.library import SimpleFunctionWrapper
810 D['F'] = SimpleFunctionWrapper(L['F'])
815 J('[4 5 ...] 2 3 1 F')
821 With this, we have a partial Joy compiler that works on the subset of Joy functions that manipulate stacks (both what I call "stack chatter" and the ones that manipulate stacks on the stack.)
823 I'm probably going to modify the definition wrapper code to detect definitions that can be compiled by this partial compiler and do it automatically. It might be a reasonable idea to detect sequences of compilable functions in definitions that have uncompilable functions in them and just compile those. However, if your library is well-factored this might be less helpful.
825 ### Compiling Library Functions
826 We can use `compile_()` to generate many primitives in the library from their stack effect comments:
832 rolldown = (1, 2, 3), (2, 3, 1)
834 rollup = (1, 2, 3), (3, 1, 2)
838 swap = (1, 2), (2, 1)
840 rest = ((1, 2),), (2,)
842 rrest = C(rest, rest)
844 cons = (1, 2), ((1, 2),)
846 uncons = ((1, 2),), (1, 2)
848 swons = C(swap, cons)
855 for name, stack_effect_comment in sorted(defs().items()):
857 print compile_(name, stack_effect_comment)
863 """(1 2 -- [1 .2.])"""
864 (a1, (a0, stack)) = stack
865 return ((a0, a1), stack)
876 ((a0, a1), stack) = stack
881 """(1 2 3 -- 2 3 1)"""
882 (a2, (a1, (a0, stack))) = stack
883 return (a0, (a2, (a1, stack)))
887 """(1 2 3 -- 3 1 2)"""
888 (a2, (a1, (a0, stack))) = stack
889 return (a1, (a0, (a2, stack)))
893 """([0 1 .2.] -- 2)"""
894 ((a0, (a1, a2)), stack) = stack
900 (a1, (a0, stack)) = stack
901 return (a0, (a1, stack))
905 """(0 1 -- [1 .0.])"""
906 (a1, (a0, stack)) = stack
907 return ((a1, a0), stack)
911 """([1 .2.] -- 1 2)"""
912 ((a0, a1), stack) = stack
913 return (a1, (a0, stack))
917 ## Part IV: Types and Subtypes of Arguments
918 So far we have dealt with types of functions, those dealing with simple stack manipulation. Let's extend our machinery to deal with types of arguments.
922 Consider the definition of `sqr`:
927 The `dup` function accepts one *anything* and returns two of that:
931 And `mul` accepts two "numbers" (we're ignoring ints vs. floats vs. complex, etc., for now) and returns just one:
937 (1 -- 1 1)∘(n n -- n)
939 The rules say we unify 1 with `n`:
941 (1 -- 1 1)∘(n n -- n)
942 --------------------------- w/ {1: n}
945 This involves detecting that "Any type" arguments can accept "numbers". If we were composing these functions the other way round this is still the case:
947 (n n -- n)∘(1 -- 1 1)
948 --------------------------- w/ {1: n}
951 The important thing here is that the mapping is going the same way in both cases, from the "any" integer to the number
953 ### Distinguishing Numbers
954 We should also mind that the number that `mul` produces is not (necessarily) the same as either of its inputs, which are not (necessarily) the same as each other:
959 (1 -- 1 1)∘(n2 n1 -- n3)
960 -------------------------------- w/ {1: n2}
961 (n2 -- n2 )∘(n2 -- n3)
964 (n2 n1 -- n3)∘(1 -- 1 1 )
965 -------------------------------- w/ {1: n3}
966 (n2 n1 -- )∘( -- n3 n3)
970 ### Distinguishing Types
971 So we need separate domains of "any" numbers and "number" numbers, and we need to be able to ask the order of these domains. Now the notes on the right side of rule three make more sense, eh?
973 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
974 -------------------------------
975 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
978 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
979 -------------------------------
980 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
982 The indices `i`, `k`, and `j` are the number part of our labels and `t` and `u` are the domains.
984 By creative use of Python's "double underscore" methods we can define a Python class hierarchy of Joy types and use the `issubclass()` method to establish domain ordering, as well as other handy behaviour that will make it fairly easy to reuse most of the code above.
988 class AnyJoyType(object):
992 def __init__(self, number):
996 return self.prefix + str(self.number)
998 def __eq__(self, other):
1000 isinstance(other, self.__class__)
1001 and other.prefix == self.prefix
1002 and other.number == self.number
1005 def __ge__(self, other):
1006 return issubclass(other.__class__, self.__class__)
1008 def __add__(self, other):
1009 return self.__class__(self.number + other)
1013 return hash(repr(self))
1016 class NumberJoyType(AnyJoyType): prefix = 'n'
1017 class FloatJoyType(NumberJoyType): prefix = 'f'
1018 class IntJoyType(FloatJoyType): prefix = 'i'
1021 class StackJoyType(AnyJoyType):
1026 A = map(AnyJoyType, _R)
1027 N = map(NumberJoyType, _R)
1028 S = map(StackJoyType, _R)
1031 Mess with it a little:
1035 from itertools import permutations
1038 "Any" types can be specialized to numbers and stacks, but not vice versa:
1042 for a, b in permutations((A[0], N[0], S[0]), 2):
1043 print a, '>=', b, '->', a >= b
1054 Our crude [Numerical Tower](https://en.wikipedia.org/wiki/Numerical_tower) of *numbers* > *floats* > *integers* works as well (but we're not going to use it yet):
1058 for a, b in permutations((A[0], N[0], FloatJoyType(0), IntJoyType(0)), 2):
1059 print a, '>=', b, '->', a >= b
1080 dup = (A[1],), (A[1], A[1])
1082 mul = (N[1], N[2]), (N[3],)
1109 ### Modifying the Inferencer
1110 Re-labeling still works fine:
1114 foo = relabel(dup, mul)
1122 (((a1,), (a1, a1)), ((n1001, n1002), (n1003,)))
1126 #### `delabel()` version 2
1127 The `delabel()` function needs an overhaul. It now has to keep track of how many labels of each domain it has "seen".
1131 from collections import Counter
1134 def delabel(f, seen=None, c=None):
1137 seen, c = {}, Counter()
1144 if not isinstance(f, tuple):
1145 seen[f] = f.__class__(c[f.prefix])
1149 return tuple(delabel(inner, seen, c) for inner in f)
1160 (((a0,), (a0, a0)), ((n0, n1), (n2,)))
1164 #### `unify()` version 3
1168 def unify(u, v, s=None):
1178 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
1185 raise TypeError('Cannot unify %r and %r.' % (u, v))
1187 if isinstance(u, tuple) and isinstance(v, tuple):
1188 if len(u) != len(v) != 2:
1189 raise TypeError(repr((u, v)))
1190 for uu, vv in zip(u, v):
1191 s = unify(uu, vv, s)
1192 if s == False: # (instead of a substitution dict.)
1196 if isinstance(v, tuple):
1198 raise TypeError('Cannot unify %r and %r.' % (u, v))
1202 if isinstance(u, tuple):
1204 raise TypeError('Cannot unify %r and %r.' % (v, u))
1212 return thing.__class__ in {AnyJoyType, StackJoyType}
1215 Rewrite the stack effect comments:
1221 rolldown = (A[1], A[2], A[3]), (A[2], A[3], A[1])
1223 rollup = (A[1], A[2], A[3]), (A[3], A[1], A[2])
1227 popop = (A[2], A[1],), ()
1229 popd = (A[2], A[1],), (A[1],)
1231 popdd = (A[3], A[2], A[1],), (A[2], A[1],)
1233 swap = (A[1], A[2]), (A[2], A[1])
1235 rest = ((A[1], S[1]),), (S[1],)
1237 rrest = C(rest, rest)
1239 cons = (A[1], S[1]), ((A[1], S[1]),)
1241 ccons = C(cons, cons)
1243 uncons = ((A[1], S[1]),), (A[1], S[1])
1245 swons = C(swap, cons)
1247 dup = (A[1],), (A[1], A[1])
1249 dupd = (A[2], A[1]), (A[2], A[2], A[1])
1251 mul = (N[1], N[2]), (N[3],)
1255 first = ((A[1], S[1]),), (A[1],)
1257 second = C(rest, first)
1259 third = C(rest, second)
1261 tuck = (A[2], A[1]), (A[1], A[2], A[1])
1263 over = (A[2], A[1]), (A[2], A[1], A[2])
1265 succ = pred = (N[1],), (N[2],)
1267 divmod_ = pm = (N[2], N[1]), (N[4], N[3])
1279 for name, stack_effect_comment in sorted(DEFS.items()):
1280 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1283 ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
1284 cons = (a1 [.1.] -- [a1 .1.])
1285 divmod_ = (n2 n1 -- n4 n3)
1287 dupd = (a2 a1 -- a2 a2 a1)
1288 first = ([a1 .1.] -- a1)
1290 over = (a2 a1 -- a2 a1 a2)
1291 pm = (n2 n1 -- n4 n3)
1293 popd = (a2 a1 -- a1)
1294 popdd = (a3 a2 a1 -- a2 a1)
1297 rest = ([a1 .1.] -- [.1.])
1298 rolldown = (a1 a2 a3 -- a2 a3 a1)
1299 rollup = (a1 a2 a3 -- a3 a1 a2)
1300 rrest = ([a0 a1 .0.] -- [.0.])
1301 second = ([a0 a1 .0.] -- a1)
1304 swap = (a1 a2 -- a2 a1)
1305 swons = ([.0.] a0 -- [a0 .0.])
1306 third = ([a0 a1 a2 .0.] -- a2)
1307 tuck = (a2 a1 -- a1 a2 a1)
1308 uncons = ([a1 .1.] -- a1 [.1.])
1313 globals().update(DEFS)
1316 #### Compose `dup` and `mul`
1330 Revisit the `F` function, works fine.
1334 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
1341 (((a0, (a1, s0)), a2, a3, a4), ((a3, (a2, s0)),))
1347 print doc_from_stack_effect(*F)
1350 ([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])
1353 Some otherwise inefficient functions are no longer to be feared. We can also get the effect of combinators in some limited cases.
1358 print doc_from_stack_effect(*reduce(C, funcs))
1364 neato(rollup, swap, rolldown)
1367 (a0 a1 a2 -- a1 a0 a2)
1373 neato(popdd, rolldown, pop)
1376 (a0 a1 a2 a3 -- a2 a3)
1381 # Reverse the order of the top three items.
1385 (a0 a1 a2 -- a2 a1 a0)
1388 #### `compile_()` version 2
1389 Because the type labels represent themselves as valid Python identifiers the `compile_()` function doesn't need to generate them anymore:
1393 def compile_(name, f, doc=None):
1396 doc = doc_from_stack_effect(inputs, outputs)
1397 i = o = Symbol('stack')
1400 for term in outputs:
1402 return '''def %s(stack):
1405 return %s''' % (name, doc, i, o)
1410 print compile_('F', F)
1414 """([a0 a1 .0.] a2 a3 a4 -- [a3 a2 .0.])"""
1415 (a4, (a3, (a2, ((a0, (a1, s0)), stack)))) = stack
1416 return ((a3, (a2, s0)), stack)
1419 But it cannot magically create new functions that involve e.g. math and such. Note that this is *not* a `sqr` function implementation:
1423 print compile_('sqr', C(dup, mul))
1432 (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.)
1435 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:
1439 from itertools import imap
1443 return isinstance(f, tuple) and all(imap(compilable, f)) or stacky(f)
1448 for name, stack_effect_comment in sorted(defs().items()):
1449 if compilable(stack_effect_comment):
1450 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1453 ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
1454 cons = (a1 [.1.] -- [a1 .1.])
1456 dupd = (a2 a1 -- a2 a2 a1)
1457 first = ([a1 .1.] -- a1)
1458 over = (a2 a1 -- a2 a1 a2)
1460 popd = (a2 a1 -- a1)
1461 popdd = (a3 a2 a1 -- a2 a1)
1463 rest = ([a1 .1.] -- [.1.])
1464 rolldown = (a1 a2 a3 -- a2 a3 a1)
1465 rollup = (a1 a2 a3 -- a3 a1 a2)
1466 rrest = ([a0 a1 .0.] -- [.0.])
1467 second = ([a0 a1 .0.] -- a1)
1468 swap = (a1 a2 -- a2 a1)
1469 swons = ([.0.] a0 -- [a0 .0.])
1470 third = ([a0 a1 a2 .0.] -- a2)
1471 tuck = (a2 a1 -- a1 a2 a1)
1472 uncons = ([a1 .1.] -- a1 [.1.])
1475 ## Part V: Functions that use the Stack
1477 Consider the `stack` function which grabs the whole stack, quotes it, and puts it on itself:
1479 stack (... -- ... [...] )
1480 stack (... a -- ... a [a ...] )
1481 stack (... b a -- ... b a [a b ...])
1483 We would like to represent this in Python somehow.
1484 To do this we use a simple, elegant trick.
1487 stack (a, S) -- ( (a, S), (a, S))
1488 stack (a, (b, S)) -- ( (a, (b, S)), (a, (b, S)))
1490 Instead of representing the stack effect comments as a single tuple (with N items in it) we use the same cons-list structure to hold the sequence and `unify()` the whole comments.
1493 Let's try composing `stack` and `uncons`. We want this result:
1495 stack∘uncons (... a -- ... a a [...])
1497 The stack effects are:
1501 uncons = ((a, Z), S) -- (Z, (a, S))
1505 S -- (S, S) ∘ ((a, Z), S) -- (Z, (a, S ))
1507 (a, Z) -- ∘ -- (Z, (a, (a, Z)))
1511 stack∘uncons == (a, Z) -- (Z, (a, (a, Z)))
1515 ### `stack∘uncons∘uncons`
1516 Let's try `stack∘uncons∘uncons`:
1518 (a, S ) -- (S, (a, (a, S ))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1522 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1524 w/ { S`: (a, (a, (b, Z))) }
1526 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), (a, (a, (b, Z)))) -- (Z, (b, (a, (a, (b, Z)))))
1528 (a, (b, Z)) -- (Z, (b, (a, (a, (b, Z)))))
1532 #### `compose()` version 2
1533 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.
1538 (f_in, f_out), (g_in, g_out) = f, g
1539 s = unify(g_in, f_out)
1540 if s == False: # s can also be the empty dict, which is ok.
1541 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
1542 return update(s, (f_in, g_out))
1545 I don't want to rewrite all the defs myself, so I'll write a little conversion function instead. This is programmer's laziness.
1549 def sequence_to_stack(seq, stack=StackJoyType(23)):
1550 for item in seq: stack = item, stack
1554 name: (sequence_to_stack(i), sequence_to_stack(o))
1555 for name, (i, o) in DEFS.iteritems()
1557 NEW_DEFS['stack'] = S[0], (S[0], S[0])
1558 NEW_DEFS['swaack'] = (S[1], S[0]), (S[0], S[1])
1559 globals().update(NEW_DEFS)
1570 ((a0, s0), (s0, (a0, (a0, s0))))
1576 C(C(stack, uncons), uncons)
1582 ((a0, (a1, s0)), (s0, (a1, (a0, (a0, (a1, s0))))))
1586 The display function should be changed too.
1588 ### `doc_from_stack_effect()` version 2
1589 Clunky junk, but it will suffice for now.
1593 def doc_from_stack_effect(inputs, outputs):
1594 switch = [False] # Do we need to display the '...' for the rest of the main stack?
1595 i, o = _f(inputs, switch), _f(outputs, switch)
1599 return '(%s--%s)' % (
1600 ' '.join(reversed([''] + i)),
1601 ' '.join(reversed(o + [''])),
1605 def _f(term, switch):
1607 while term and isinstance(term, tuple):
1610 assert isinstance(term, StackJoyType), repr(term)
1611 a = [_to_str(i, term, switch) for i in a]
1615 def _to_str(term, stack, switch):
1616 if not isinstance(term, tuple):
1621 '[.%i.]' % term.number
1622 if isinstance(term, StackJoyType)
1627 while term and isinstance(term, tuple):
1629 a.append(_to_str(item, stack, switch))
1630 assert isinstance(term, StackJoyType), repr(term)
1635 end = '.%i.' % term.number
1637 return '[%s]' % ' '.join(a)
1642 for name, stack_effect_comment in sorted(NEW_DEFS.items()):
1643 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1646 ccons = (a0 a1 [.0.] -- [a0 a1 .0.])
1647 cons = (a1 [.1.] -- [a1 .1.])
1648 divmod_ = (n2 n1 -- n4 n3)
1650 dupd = (a2 a1 -- a2 a2 a1)
1651 first = ([a1 .1.] -- a1)
1653 over = (a2 a1 -- a2 a1 a2)
1654 pm = (n2 n1 -- n4 n3)
1656 popd = (a2 a1 -- a1)
1657 popdd = (a3 a2 a1 -- a2 a1)
1660 rest = ([a1 .1.] -- [.1.])
1661 rolldown = (a1 a2 a3 -- a2 a3 a1)
1662 rollup = (a1 a2 a3 -- a3 a1 a2)
1663 rrest = ([a0 a1 .0.] -- [.0.])
1664 second = ([a0 a1 .0.] -- a1)
1666 stack = (... -- ... [...])
1668 swaack = ([.1.] -- [.0.])
1669 swap = (a1 a2 -- a2 a1)
1670 swons = ([.0.] a0 -- [a0 .0.])
1671 third = ([a0 a1 a2 .0.] -- a2)
1672 tuck = (a2 a1 -- a1 a2 a1)
1673 uncons = ([a1 .1.] -- a1 [.1.])
1678 print ; print doc_from_stack_effect(*stack)
1679 print ; print doc_from_stack_effect(*C(stack, uncons))
1680 print ; print doc_from_stack_effect(*C(C(stack, uncons), uncons))
1681 print ; print doc_from_stack_effect(*C(C(stack, uncons), cons))
1687 (... a0 -- ... a0 a0 [...])
1689 (... a1 a0 -- ... a1 a0 a0 a1 [...])
1691 (... a0 -- ... a0 [a0 ...])
1696 print doc_from_stack_effect(*C(ccons, stack))
1699 (... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])
1712 ((s0, (a0, (a1, s1))), (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1)))
1716 #### `compile_()` version 3
1717 This makes the `compile_()` function pretty simple as the stack effect comments are now already in the form needed for the Python code:
1721 def compile_(name, f, doc=None):
1724 doc = doc_from_stack_effect(i, o)
1725 return '''def %s(stack):
1728 return %s''' % (name, doc, i, o)
1733 print compile_('Q', Q)
1737 """(... a1 a0 [.0.] -- ... [a1 a0 .0.] [[a1 a0 .0.] ...])"""
1738 (s0, (a0, (a1, s1))) = stack
1739 return (((a1, (a0, s0)), s1), ((a1, (a0, s0)), s1))
1744 unstack = (S[1], S[0]), S[1]
1745 enstacken = S[0], (S[0], S[1])
1750 print doc_from_stack_effect(*unstack)
1758 print doc_from_stack_effect(*enstacken)
1766 print doc_from_stack_effect(*C(cons, unstack))
1774 print doc_from_stack_effect(*C(cons, enstacken))
1777 (a0 [.0.] -- [[a0 .0.] .1.])
1788 ((s0, (a0, s1)), (a0, s0))
1792 ## Part VI: Multiple Stack Effects
1797 class IntJoyType(NumberJoyType): prefix = 'i'
1800 F = map(FloatJoyType, _R)
1801 I = map(IntJoyType, _R)
1807 ((I[2], (I[1], S[0])), (I[3], S[0])),
1808 ((F[2], (I[1], S[0])), (F[3], S[0])),
1809 ((I[2], (F[1], S[0])), (F[3], S[0])),
1810 ((F[2], (F[1], S[0])), (F[3], S[0])),
1817 print doc_from_stack_effect(*f)
1833 print doc_from_stack_effect(*dup), doc_from_stack_effect(*f), doc_from_stack_effect(*e)
1836 (a1 -- a1 a1) (i1 i2 -- i3) (i0 -- i1)
1837 (a1 -- a1 a1) (f1 f2 -- f3) (f0 -- f1)
1842 from itertools import product
1845 def meta_compose(F, G):
1846 for f, g in product(F, G):
1854 return sorted(set(meta_compose(F, G)))
1859 for f in MC([dup], muls):
1860 print doc_from_stack_effect(*f)
1869 for f in MC([dup], [mul]):
1870 print doc_from_stack_effect(*f)
1876 ### Representing an Unbounded Sequence of Types
1878 We can borrow a trick from [Brzozowski's Derivatives of Regular Expressions](https://en.wikipedia.org/wiki/Brzozowski_derivative) to invent a new type of type variable, a "sequence type" (I think this is what they mean in the literature by that term...) or "[Kleene Star](https://en.wikipedia.org/wiki/Kleene_star)" type. I'm going to represent it as a type letter and the asterix, so a sequence of zero or more `AnyJoyType` variables would be:
1882 The `A*` works by splitting the universe into two alternate histories:
1886 The Kleene star variable disappears in one universe, and in the other it turns into an `AnyJoyType` variable followed by itself again. We have to return all universes (represented by their substitution dicts, the "unifiers") that don't lead to type conflicts.
1888 Consider unifying two stacks (the lowercase letters are any type variables of the kinds we have defined so far):
1890 [a A* b .0.] U [c d .1.]
1892 [ A* b .0.] U [ d .1.]
1894 Now we have to split universes to unify `A*`. In the first universe it disappears:
1900 While in the second it spawns an `A`, which we will label `e`:
1902 [e A* b .0.] U [d .1.]
1904 [ A* b .0.] U [ .1.]
1906 [ A* b .0.] U [ A* b .0.]
1908 Giving us two unifiers:
1910 {c: a, d: b, .1.: .0.}
1911 {c: a, d: e, .1.: A* b .0.}
1915 class KleeneStar(object):
1919 def __init__(self, number):
1920 self.number = number
1922 self.prefix = repr(self)
1925 return '%s%i*' % (self.kind.prefix, self.number)
1929 return self.kind(10000 * self.number + self.count)
1931 def __eq__(self, other):
1933 isinstance(other, self.__class__)
1934 and other.number == self.number
1937 def __ge__(self, other):
1938 return self.kind >= other.kind
1940 def __add__(self, other):
1941 return self.__class__(self.number + other)
1945 return hash(repr(self))
1947 class AnyStarJoyType(KleeneStar): kind = AnyJoyType
1948 class NumberStarJoyType(KleeneStar): kind = NumberJoyType
1949 #class FloatStarJoyType(KleeneStar): kind = FloatJoyType
1950 #class IntStarJoyType(KleeneStar): kind = IntJoyType
1951 class StackStarJoyType(KleeneStar): kind = StackJoyType
1954 As = map(AnyStarJoyType, _R)
1955 Ns = map(NumberStarJoyType, _R)
1956 Ss = map(StackStarJoyType, _R)
1959 #### `unify()` version 4
1960 Can now return multiple results...
1964 def unify(u, v, s=None):
1974 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
1981 raise TypeError('Cannot unify %r and %r.' % (u, v))
1983 if isinstance(u, tuple) and isinstance(v, tuple):
1984 if len(u) != len(v) != 2:
1985 raise TypeError(repr((u, v)))
1988 if isinstance(a, KleeneStar):
1989 # Two universes, in one the Kleene star disappears and unification
1990 # continues without it...
1993 # In the other it spawns a new variable.
1994 s1 = unify(u, (a.another(), v))
2002 if isinstance(a, KleeneStar):
2004 s1 = unify(v, (a.another(), u))
2010 ses = unify(u[0], v[0], s)
2013 results += unify(u[1], v[1], sn)
2016 if isinstance(v, tuple):
2018 raise TypeError('Cannot unify %r and %r.' % (u, v))
2022 if isinstance(u, tuple):
2024 raise TypeError('Cannot unify %r and %r.' % (v, u))
2032 return thing.__class__ in {AnyJoyType, StackJoyType}
2063 for result in unify(b, a):
2064 print result, '->', update(result, a), update(result, b)
2067 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2068 {a1: a10001, s2: (a1*, s1)} -> (a1*, s1) (a10001, (a1*, s1))
2073 for result in unify(a, b):
2074 print result, '->', update(result, a), update(result, b)
2077 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2078 {a1: a10002, s2: (a1*, s1)} -> (a1*, s1) (a10002, (a1*, s1))
2082 (a1*, s1) [a1*] (a1, s2) [a1]
2084 (a1*, (a1, s2)) [a1* a1] (a1, s2) [a1]
2086 (a1*, s1) [a1*] (a2, (a1*, s1)) [a2 a1*]
2090 sum_ = ((Ns[1], S[1]), S[0]), (N[0], S[0])
2092 print doc_from_stack_effect(*sum_)
2100 f = (N[1], (N[2], (N[3], S[1]))), S[0]
2102 print doc_from_stack_effect(S[0], f)
2110 for result in unify(sum_[0], f):
2111 print result, '->', update(result, sum_[1])
2114 {s1: (n1, (n2, (n3, s1)))} -> (n0, s0)
2115 {n1: n10001, s1: (n2, (n3, s1))} -> (n0, s0)
2116 {n1: n10001, s1: (n3, s1), n2: n10002} -> (n0, s0)
2117 {n1: n10001, s1: (n1*, s1), n3: n10003, n2: n10002} -> (n0, s0)
2120 #### `compose()` version 3
2121 This function has to be modified to yield multiple results.
2126 (f_in, f_out), (g_in, g_out) = f, g
2127 s = unify(g_in, f_out)
2129 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2131 yield update(result, (f_in, g_out))
2137 def meta_compose(F, G):
2138 for f, g in product(F, G):
2140 for result in C(f, g):
2147 f, g = relabel(f, g)
2148 for fg in compose(f, g):
2154 for f in MC([dup], muls):
2155 print doc_from_stack_effect(*f)
2166 for f in MC([dup], [sum_]):
2167 print doc_from_stack_effect(*f)
2170 ([n0* .0.] -- [n0* .0.] n0)
2177 for f in MC([cons], [sum_]):
2178 print doc_from_stack_effect(*f)
2182 (n0 [n0* .0.] -- n1)
2187 sum_ = (((N[1], (Ns[1], S[1])), S[0]), (N[0], S[0]))
2188 print doc_from_stack_effect(*cons),
2189 print doc_from_stack_effect(*sum_),
2191 for f in MC([cons], [sum_]):
2192 print doc_from_stack_effect(*f)
2195 (a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n0 [n0* .0.] -- n1)
2200 a = (A[4], (As[1], (A[3], S[1])))
2207 (a4, (a1*, (a3, s1)))
2213 b = (A[1], (A[2], S[2]))
2226 for result in unify(b, a):
2230 {a1: a4, s2: s1, a2: a3}
2231 {a1: a4, s2: (a1*, (a3, s1)), a2: a10003}
2236 for result in unify(a, b):
2240 {s2: s1, a2: a3, a4: a1}
2241 {s2: (a1*, (a3, s1)), a2: a10004, a4: a1}
2244 ## Part VII: Typing Combinators
2246 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:
2248 i (... [.1.] -- ... .1.)
2252 i (... [A* .1.] -- ... A*)
2254 Consider the type of:
2258 Obviously it would be:
2260 (a1 [..1] a2 -- [a1 ..1] a2)
2262 `dip` itself could have:
2264 (a1 [..1] -- ... then what?
2267 Without any information about the contents of the quote we can't say much about the result.
2269 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.
2273 class FunctionJoyType(AnyJoyType):
2275 def __init__(self, name, sec, number):
2277 self.stack_effects = sec
2278 self.number = number
2280 def __add__(self, other):
2288 class SymbolJoyType(FunctionJoyType): prefix = 'F'
2289 class CombinatorJoyType(FunctionJoyType): prefix = 'C'
2298 return list(chain.from_iterable(g))
2301 ID = S[0], S[0] # Identity function.
2310 if isinstance(n, SymbolJoyType):
2311 res = flatten(infer(e, Fn) for Fn in MC([F], n.stack_effects))
2313 elif isinstance(n, CombinatorJoyType):
2315 for combinator in n.stack_effects:
2317 new_fo, ee, _ = combinator(fo, e, {})
2318 ee = update(FUNCTIONS, ee) # Fix Symbols.
2320 res.extend(infer(ee, new_F))
2323 res = flatten(infer(e, Fn) for Fn in MC([F], [lit]))
2332 f0, f1, f2, f3, f4, f5, f6, f7, f8, f9 = F = map(FloatJoyType, _R)
2333 i0, i1, i2, i3, i4, i5, i6, i7, i8, i9 = I = map(IntJoyType, _R)
2334 n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 = N
2335 s0, s1, s2, s3, s4, s5, s6, s7, s8, s9 = S
2342 FNs = '''ccons cons divmod_ dup dupd first
2343 over pm pop popd popdd popop pred
2344 rest rolldown rollup rrest second
2345 sqrt stack succ swaack swap swons
2346 third tuck uncons'''
2349 name: SymbolJoyType(name, [NEW_DEFS[name]], i)
2350 for i, name in enumerate(FNs.strip().split())
2352 FUNCTIONS['sum'] = SymbolJoyType('sum', [(((Ns[1], s1), s0), (n0, s0))], 100)
2353 FUNCTIONS['mul'] = SymbolJoyType('mul', [
2354 ((i2, (i1, s0)), (i3, s0)),
2355 ((f2, (i1, s0)), (f3, s0)),
2356 ((i2, (f1, s0)), (f3, s0)),
2357 ((f2, (f1, s0)), (f3, s0)),
2360 combo.__name__: CombinatorJoyType(combo.__name__, [combo], i)
2361 for i, combo in enumerate((
2373 def branch_true(stack, expression, dictionary):
2374 (then, (else_, (flag, stack))) = stack
2375 return stack, CONCAT(then, expression), dictionary
2377 def branch_false(stack, expression, dictionary):
2378 (then, (else_, (flag, stack))) = stack
2379 return stack, CONCAT(else_, expression), dictionary
2381 FUNCTIONS['branch'] = CombinatorJoyType('branch', [branch_true, branch_false], 100)
2386 globals().update(FUNCTIONS)
2391 from itertools import chain
2392 from joy.utils.stack import list_to_stack as l2s
2397 expression = l2s([n1, n2, (mul, s2), (stack, s3), dip, infra, first])
2408 (n1, (n2, ((mul, s2), ((stack, s3), (dip, (infra, (first, ())))))))
2414 expression = l2s([n1, n2, mul])
2431 class SymbolJoyType(AnyJoyType):
2434 def __init__(self, name, sec, number):
2436 self.stack_effects = sec
2437 self.number = number
2439 class CombinatorJoyType(SymbolJoyType): prefix = 'C'
2441 def dip_t(stack, expression):
2442 (quote, (a1, stack)) = stack
2443 expression = stack_concat(quote, (a1, expression))
2444 return stack, expression
2446 CONS = SymbolJoyType('cons', [cons], 23)
2447 DIP = CombinatorJoyType('dip', [dip_t], 44)
2455 if isinstance(n, SymbolJoyType):
2457 for sec in n.stack_effects:
2458 Fs.extend(MC([F], sec))
2459 return [kav(Fn, e) for Fn in Fs]
2460 if isinstance(n, CombinatorJoyType):
2462 for f in n.stack_effects:
2465 res.extend(kav(new_F, e))
2467 lit = S[0], (n, S[0])
2468 return [kav(Fn, e) for Fn in MC([F], [lit])]
2472 compare, and be amazed:
2476 def dip_t(stack, expression):
2477 (quote, (a1, stack)) = stack
2478 expression = stack_concat(quote, (a1, expression))
2479 return stack, expression
2484 def dip(stack, expression, dictionary):
2485 (quote, (x, stack)) = stack
2486 expression = (x, expression)
2487 return stack, concat(quote, expression), dictionary
2490 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.
2492 The rest of this stuff is junk and/or unfinished material.
2494 ## Appendix: Joy in the Logical Paradigm
2495 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`
2499 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
2501 print doc_from_stack_effect(*F)
2505 ---------------------------------------------------------------------------
2507 TypeError Traceback (most recent call last)
2509 <ipython-input-119-7fde90b4e88f> in <module>()
2510 1 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
2512 ----> 3 print doc_from_stack_effect(*F)
2515 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2517 11 f, g = relabel(f, g)
2518 ---> 12 for fg in compose(f, g):
2519 13 yield delabel(fg)
2522 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2523 1 def compose(f, g):
2524 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2525 3 s = unify(g_in, f_out)
2527 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2530 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2532 11 f, g = relabel(f, g)
2533 ---> 12 for fg in compose(f, g):
2534 13 yield delabel(fg)
2537 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2538 1 def compose(f, g):
2539 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2540 3 s = unify(g_in, f_out)
2542 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2545 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2547 11 f, g = relabel(f, g)
2548 ---> 12 for fg in compose(f, g):
2549 13 yield delabel(fg)
2552 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2553 1 def compose(f, g):
2554 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2555 3 s = unify(g_in, f_out)
2557 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2560 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2562 11 f, g = relabel(f, g)
2563 ---> 12 for fg in compose(f, g):
2564 13 yield delabel(fg)
2567 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2568 1 def compose(f, g):
2569 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2570 3 s = unify(g_in, f_out)
2572 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2575 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2577 11 f, g = relabel(f, g)
2578 ---> 12 for fg in compose(f, g):
2579 13 yield delabel(fg)
2582 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2583 1 def compose(f, g):
2584 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2585 3 s = unify(g_in, f_out)
2587 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2590 <ipython-input-98-ddee30dbb1a6> in C(f, g)
2592 11 f, g = relabel(f, g)
2593 ---> 12 for fg in compose(f, g):
2594 13 yield delabel(fg)
2597 <ipython-input-97-5eb7ac5ad2c2> in compose(f, g)
2598 1 def compose(f, g):
2599 ----> 2 (f_in, f_out), (g_in, g_out) = f, g
2600 3 s = unify(g_in, f_out)
2602 5 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2605 TypeError: 'SymbolJoyType' object is not iterable
2610 from joy.parser import text_to_expression
2615 s = text_to_expression('[3 4 ...] 2 1')
2640 ## [Abstract Interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation)
2641 I *think* this might be sorta what I'm doing above with the `kav()` function...
2642 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.
2649 class SymbolJoyType(AnyJoyType): prefix = 'F'
2651 W = map(SymbolJoyType, _R)
2653 k = S[0], ((W[1], S[2]), S[0])
2655 print doc_from_stack_effect(*k)
2661 dip_a = ((W[1], S[2]), (A[1], S[0]))
2666 d = relabel(S[0], dip_a)
2667 print doc_from_stack_effect(*d)
2672 s = list(unify(d[1], k[1]))[0]
2683 print doc_from_stack_effect(*j)
2698 for f in MC([k], [dup]):
2699 print doc_from_stack_effect(*f)
2704 l = S[0], ((cons, S[2]), (A[1], S[0]))
2709 print doc_from_stack_effect(*l)
2716 (quote, (a1, sec)) = F[1]
2718 P = S[3], (a1, S[3])
2720 while isinstance(quote, tuple):
2733 from joy.utils.stack import iter_stack
2763 kjs = MC(MC([a], [b]), [c])
2769 print doc_from_stack_effect(*kjs[0])
2772 (a0 [.0.] -- [a0 .0.] a1)
2774 a0 [.0.] a1 [cons] dip
2775 ----------------------------
2780 How to deal with `concat`?
2782 concat ([.0.] [.1.] -- [.0. .1.])
2784 We would like to represent this in Python somehow...
2788 concat = (S[0], S[1]), ((S[0], S[1]),)
2791 But this is actually `cons` with the first argument restricted to be a stack:
2793 ([.0.] [.1.] -- [[.0.] .1.])
2795 What we have implemented so far would actually only permit:
2797 ([.0.] [.1.] -- [.2.])
2801 concat = (S[0], S[1]), (S[2],)
2805 Which works but can lose information. Consider `cons concat`, this is how much information we *could* retain:
2807 (1 [.0.] [.1.] -- [1 .0. .1.])
2811 (1 [.0.] [.1.] -- [.2.])
2813 ### represent `concat`
2815 ([.0.] [.1.] -- [A*(.0.) .1.])
2817 Meaning that `A*` on the right-hand side should all the crap from `.0.`.
2819 ([ .0.] [.1.] -- [ A* .1.])
2820 ([a .0.] [.1.] -- [a A* .1.])
2821 ([a b .0.] [.1.] -- [a b A* .1.])
2822 ([a b c .0.] [.1.] -- [a b c A* .1.])
2828 ([ .0.] [.1.] -- [ .1.])
2829 ([a .0.] [.1.] -- [a .1.])
2830 ([a b .0.] [.1.] -- [a b .1.])
2831 ([a b c .0.] [.1.] -- [a b c .1.])
2832 ([a A* c .0.] [.1.] -- [a A* c .1.])
2836 (a, (b, S0)) . S1 = (a, (b, (A*, S1)))
2840 class Astar(object):
2847 while isinstance(s0, tuple):
2850 assert isinstance(s0, StackJoyType), repr(s0)
2852 for term in reversed(a):
2859 a, b = (A[1], S[0]), (A[2], S[1])