1 # The Blissful Elegance of Typing Joy
3 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.)
5 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.)
9 ## Part I: Pöial's Rules
11 ["Typing Tools for Typeless Stack Languages" by Jaanus Pöial
12 ](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.212.6026)
14 @INPROCEEDINGS{Pöial06typingtools,
15 author = {Jaanus Pöial},
16 title = {Typing tools for typeless stack languages},
17 booktitle = {In 23rd Euro-Forth Conference},
23 This rule deals with functions (and literals) that put items on the stack `(-- d)`:
31 This rule deals with functions that consume items from the stack `(a --)`:
38 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.
40 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
41 -------------------------------
42 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
45 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
46 -------------------------------
47 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
49 Let's work through some examples by hand to develop an intuition for the algorithm.
51 There's a function in one of the other notebooks.
53 F == pop swap roll< rest rest cons cons
55 It's all "stack chatter" and list manipulation so we should be able to deduce its type.
57 ### Stack Effect Comments
58 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):
64 roll< (1 2 3 -- 2 3 1)
66 These commands alter the stack but don't "look at" the values so these numbers represent an "Any type".
72 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:
76 Following the second rule:
82 (1 2 0 -- 2 1) (1 2 3 -- 2 3 1)
86 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
88 Now we follow the rules.
90 We must unify `1a` and `3b`, and `2a` and `2b`, replacing the terms in the forms:
92 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
94 (3b 2a 0a -- 2a ) (1b 2b -- 2b 3b 1b)
96 (3b 2b 0a -- ) (1b -- 2b 3b 1b)
98 Here we must apply the second rule:
100 (3b 2b 0a --) (1b -- 2b 3b 1b)
101 -----------------------------------
102 (1b 3b 2b 0a -- 2b 3b 1b)
104 Now we de-label the type, uh, labels:
106 (1b 3b 2b 0a -- 2b 3b 1b)
117 And now we have the stack effect comment for `pop∘swap∘roll<`.
119 ### Compiling `pop∘swap∘roll<`
120 The simplest way to "compile" this function would be something like:
125 return rolldown(*swap(*pop(s, e, d)))
128 However, internally this function would still be allocating tuples (stack cells) and doing other unnecesssary work.
130 Looking ahead for a moment, from the stack effect comment:
134 We should be able to directly write out a Python function like:
139 (_, (a, (b, (c, stack)))) = stack
140 return (c, (b, (a, stack)))
143 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.
145 ### Functions on Stacks
146 These are slightly tricky.
148 rest ( [1 ...] -- [...] )
150 cons ( 1 [...] -- [1 ...] )
152 ### `pop∘swap∘roll< rest`
154 (1 2 3 0 -- 3 2 1) ([1 ...] -- [...])
156 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):
158 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
162 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
164 ([4 ...] 2 3 0 -- 3 2 ) ( -- [...])
166 Apply the first rule:
168 ([4 ...] 2 3 0 -- 3 2) (-- [...])
169 ---------------------------------------
170 ([4 ...] 2 3 0 -- 3 2 [...])
174 ### `pop∘swap∘roll<∘rest rest`
178 ([4 ...] 2 3 0 -- 3 2 [...]) ([1 ...] -- [...])
180 Re-label (the tails of the lists on each side each get their own label):
182 ([4 .0.] 2 3 0 -- 3 2 [.0.]) ([5 .1.] -- [.1.])
184 Unify and update (note the opening square brackets have been omited in the substitution dict, this is deliberate and I'll explain below):
186 ([4 .0.] 2 3 0 -- 3 2 [.0.] ) ([5 .1.] -- [.1.])
188 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
190 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.
192 Next we unify and find our two terms are the same already: `[5 .1.]`:
194 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
198 ([4 5 .1.] 2 3 0 -- 3 2) (-- [.1.])
200 From here we apply the first rule and get:
202 ([4 5 .1.] 2 3 0 -- 3 2 [.1.])
204 Cleaning up the labels:
206 ([4 5 ...] 2 3 1 -- 3 2 [...])
208 This is the stack effect of `pop∘swap∘roll<∘rest∘rest`.
210 ### `pop∘swap∘roll<∘rest∘rest cons`
212 ([4 5 ...] 2 3 1 -- 3 2 [...]) (1 [...] -- [1 ...])
216 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
220 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
222 ([4 5 .2.] 2 3 1 -- 3 2 ) (6 -- [6 .2.])
224 ([4 5 .2.] 6 3 1 -- 3 ) ( -- [6 .2.])
228 ([4 5 .2.] 6 3 1 -- 3 [6 .2.])
232 ([4 5 ...] 2 3 1 -- 3 [2 ...])
236 ### `pop∘swap∘roll<∘rest∘rest∘cons cons`
239 ([4 5 ...] 2 3 1 -- 3 [2 ...]) (1 [...] -- [1 ...])
243 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.])
247 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.] )
249 ([4 5 .1.] 2 3 1 -- 3 ) (6 -- [6 2 .1.])
251 ([4 5 .1.] 2 6 1 -- ) ( -- [6 2 .1.])
253 First or second rule:
255 ([4 5 .1.] 2 6 1 -- [6 2 .1.])
259 ([4 5 ...] 2 3 1 -- [3 2 ...])
261 And there you have it, the stack effect for `pop∘swap∘roll<∘rest∘rest∘cons∘cons`.
263 ([4 5 ...] 2 3 1 -- [3 2 ...])
265 From this stack effect comment it should be possible to construct the following Python code:
270 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
271 return (d, (c, S0)), stack
274 ## Part II: Implementation
276 ### Representing Stack Effect Comments in Python
278 I'm going to use pairs of tuples of type descriptors, which will be integers or tuples of type descriptors:
282 roll_dn = (1, 2, 3), (2, 3, 1)
286 swap = (1, 2), (2, 1)
295 (f_in, f_out), (g_in, g_out) = f, g
300 # ---------------------
305 fg_in, fg_out = f_in, f_out + g_out
310 # ---------------------
315 fg_in, fg_out = g_in + f_in, g_out
317 else: # Unify, update, recur.
319 fo, gi = f_out[-1], g_in[-1]
323 if s == False: # s can also be the empty dict, which is ok.
324 raise TypeError('Cannot unify %r and %r.' % (fo, gi))
326 f_g = (f_in, f_out[:-1]), (g_in[:-1], g_out)
328 if s: f_g = update(s, f_g)
330 fg_in, fg_out = compose(*f_g)
339 def unify(u, v, s=None):
343 if isinstance(u, int):
345 elif isinstance(v, int):
358 if not isinstance(term, tuple):
359 return s.get(term, term)
360 return tuple(update(s, inner) for inner in term)
367 def relabel(left, right):
368 return left, _1000(right)
371 if not isinstance(right, tuple):
373 return tuple(_1000(n) for n in right)
381 (((1,), ()), ((1001, 1002), (1002, 1001)))
390 s = {u: i for i, u in enumerate(sorted(_unique(f)))}
393 def _unique(f, seen=None):
396 if not isinstance(f, tuple):
403 delabel(relabel(pop, swap))
409 (((0,), ()), ((1, 2), (2, 1)))
415 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.)
441 C(C(pop, swap), roll_dn)
447 ((3, 1, 2, 0), (2, 1, 3))
459 ((2, 0, 1), (1, 0, 2))
465 C(pop, C(swap, roll_dn))
471 ((3, 1, 2, 0), (2, 1, 3))
477 poswrd = reduce(C, (pop, swap, roll_dn))
484 ((3, 1, 2, 0), (2, 1, 3))
489 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.
493 rest = ((1, 2),), (2,)
495 cons = (1, 2), ((1, 2),)
506 (((3, 4), 1, 2, 0), (2, 1, 4))
510 Compare this to the stack effect comment we wrote above:
512 (( (3, 4), 1, 2, 0 ), ( 2, 1, 4 ))
513 ( [4 ...] 2 3 0 -- 3 2 [...])
515 The translation table, if you will, would be:
527 F = reduce(C, (pop, swap, roll_dn, rest, rest, cons, cons))
535 (((3, (4, 5)), 1, 2, 0), ((2, (1, 5)),))
539 Compare with the stack effect comment and you can see it works fine:
541 ([4 5 ...] 2 3 1 -- [3 2 ...])
544 ### Dealing with `cons` and `uncons`
545 However, if we try to compose e.g. `cons` and `uncons` it won't work:
549 uncons = ((1, 2),), (1, 2)
560 Cannot unify (1, 2) and (1001, 1002).
563 #### `unify()` version 2
564 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:
568 def unify(u, v, s=None):
575 if isinstance(u, int):
578 elif isinstance(v, int):
581 elif isinstance(u, tuple) and isinstance(v, tuple):
583 if len(u) != 2 or len(v) != 2:
584 # Not a type error, caller passed in a bad value.
585 raise ValueError(repr((u, v))) # FIXME this message sucks.
587 (a, b), (c, d) = u, v
609 ## Part III: Compiling Yin Functions
610 Now consider the Python function we would like to derive:
615 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
616 return (d, (c, S0)), stack
619 And compare it to the input stack effect comment tuple we just computed:
629 ((3, (4, 5)), 1, 2, 0)
633 The stack-de-structuring tuple has nearly the same form as our input stack effect comment tuple, just in the reverse order:
635 (_, (d, (c, ((a, (b, S0)), stack))))
637 Remove the punctuation:
641 Reverse the order and compare:
644 ((3, (4, 5 )), 1, 2, 0)
662 is similar to the output stack effect comment tuple:
664 ((d, (c, S0)), stack)
667 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.)
669 ### Python Identifiers
670 We want to substitute Python identifiers for the integers. I'm going to repurpose `joy.parser.Symbol` class for this:
674 from collections import defaultdict
675 from joy.parser import Symbol
679 I = iter(xrange(1000))
680 return lambda: Symbol('a%i' % next(I))
683 def identifiers(term, s=None):
685 s = defaultdict(_names_for())
686 if isinstance(term, int):
688 return tuple(identifiers(inner, s) for inner in term)
691 ### `doc_from_stack_effect()`
692 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.
696 def doc_from_stack_effect(inputs, outputs):
697 return '(%s--%s)' % (
698 ' '.join(map(_to_str, inputs + ('',))),
699 ' '.join(map(_to_str, ('',) + outputs))
704 if not isinstance(term, tuple):
706 t = term.prefix == 's'
707 except AttributeError:
709 return '[.%i.]' % term.number if t else str(term)
712 while term and isinstance(term, tuple):
714 a.append(_to_str(item))
718 except AttributeError:
721 if term.prefix != 's':
722 raise ValueError('Stack label: %s' % (term,))
724 a.append('.%s.' % (n,))
725 return '[%s]' % ' '.join(a)
729 Now we can write a compiler function to emit Python source code. (The underscore suffix distiguishes it from the built-in `compile()` function.)
733 def compile_(name, f, doc=None):
735 doc = doc_from_stack_effect(*f)
736 inputs, outputs = identifiers(f)
737 i = o = Symbol('stack')
742 return '''def %s(stack):
745 return %s''' % (name, doc, i, o)
748 Here it is in action:
752 source = compile_('F', F)
758 """([3 4 .5.] 1 2 0 -- [2 1 .5.])"""
759 (a5, (a4, (a3, ((a0, (a1, a2)), stack)))) = stack
760 return ((a4, (a3, a2)), stack)
768 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
769 return ((d, (c, S0)), stack)
778 eval(compile(source, '__main__', 'single'), {}, L)
794 from notebook_preamble import D, J, V
795 from joy.library import SimpleFunctionWrapper
800 D['F'] = SimpleFunctionWrapper(L['F'])
805 J('[4 5 ...] 2 3 1 F')
811 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.)
813 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.
815 ### Compiling Library Functions
816 We can use `compile_()` to generate many primitives in the library from their stack effect comments:
822 rolldown = (1, 2, 3), (2, 3, 1)
824 rollup = (1, 2, 3), (3, 1, 2)
828 swap = (1, 2), (2, 1)
830 rest = ((1, 2),), (2,)
832 rrest = C(rest, rest)
834 cons = (1, 2), ((1, 2),)
836 uncons = ((1, 2),), (1, 2)
838 swons = C(swap, cons)
845 for name, stack_effect_comment in sorted(defs().items()):
847 print compile_(name, stack_effect_comment)
853 """(1 2 -- [1 .2.])"""
854 (a1, (a0, stack)) = stack
855 return ((a0, a1), stack)
866 ((a0, a1), stack) = stack
871 """(1 2 3 -- 2 3 1)"""
872 (a2, (a1, (a0, stack))) = stack
873 return (a0, (a2, (a1, stack)))
877 """(1 2 3 -- 3 1 2)"""
878 (a2, (a1, (a0, stack))) = stack
879 return (a1, (a0, (a2, stack)))
883 """([0 1 .2.] -- 2)"""
884 ((a0, (a1, a2)), stack) = stack
890 (a1, (a0, stack)) = stack
891 return (a0, (a1, stack))
895 """(0 1 -- [1 .0.])"""
896 (a1, (a0, stack)) = stack
897 return ((a1, a0), stack)
901 """([1 .2.] -- 1 2)"""
902 ((a0, a1), stack) = stack
903 return (a1, (a0, stack))
907 ## Part IV: Types and Subtypes of Arguments
908 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.
912 Consider the definition of `sqr`:
917 The `dup` function accepts one *anything* and returns two of that:
921 And `mul` accepts two "numbers" (we're ignoring ints vs. floats vs. complex, etc., for now) and returns just one:
927 (1 -- 1 1)∘(n n -- n)
929 The rules say we unify 1 with `n`:
931 (1 -- 1 1)∘(n n -- n)
932 --------------------------- w/ {1: n}
935 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:
937 (n n -- n)∘(1 -- 1 1)
938 --------------------------- w/ {1: n}
941 The important thing here is that the mapping is going the same way in both cases, from the "any" integer to the number
943 ### Distinguishing Numbers
944 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:
949 (1 -- 1 1)∘(n2 n1 -- n3)
950 -------------------------------- w/ {1: n2}
951 (n2 -- n2 )∘(n2 -- n3)
954 (n2 n1 -- n3)∘(1 -- 1 1 )
955 -------------------------------- w/ {1: n3}
956 (n2 n1 -- )∘( -- n3 n3)
960 ### Distinguishing Types
961 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?
963 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
964 -------------------------------
965 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
968 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
969 -------------------------------
970 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
972 The indices `i`, `k`, and `j` are the number part of our labels and `t` and `u` are the domains.
974 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.
978 class AnyJoyType(object):
982 def __init__(self, number):
986 return self.prefix + str(self.number)
988 def __eq__(self, other):
990 isinstance(other, self.__class__)
991 and other.prefix == self.prefix
992 and other.number == self.number
995 def __ge__(self, other):
996 return issubclass(other.__class__, self.__class__)
998 def __add__(self, other):
999 return self.__class__(self.number + other)
1003 return hash(repr(self))
1006 class NumberJoyType(AnyJoyType): prefix = 'n'
1007 class FloatJoyType(NumberJoyType): prefix = 'f'
1008 class IntJoyType(FloatJoyType): prefix = 'i'
1011 class StackJoyType(AnyJoyType):
1016 A = map(AnyJoyType, _R)
1017 N = map(NumberJoyType, _R)
1018 S = map(StackJoyType, _R)
1021 Mess with it a little:
1025 from itertools import permutations
1028 "Any" types can be specialized to numbers and stacks, but not vice versa:
1032 for a, b in permutations((A[0], N[0], S[0]), 2):
1033 print a, '>=', b, '->', a >= b
1044 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):
1048 for a, b in permutations((A[0], N[0], FloatJoyType(0), IntJoyType(0)), 2):
1049 print a, '>=', b, '->', a >= b
1070 dup = (A[1],), (A[1], A[1])
1072 mul = (N[1], N[2]), (N[3],)
1099 ### Modifying the Inferencer
1100 Re-labeling still works fine:
1104 foo = relabel(dup, mul)
1112 (((a1,), (a1, a1)), ((n1001, n1002), (n1003,)))
1116 #### `delabel()` version 2
1117 The `delabel()` function needs an overhaul. It now has to keep track of how many labels of each domain it has "seen".
1121 from collections import Counter
1124 def delabel(f, seen=None, c=None):
1127 seen, c = {}, Counter()
1134 if not isinstance(f, tuple):
1135 seen[f] = f.__class__(c[f.prefix] + 1)
1139 return tuple(delabel(inner, seen, c) for inner in f)
1150 (((a1,), (a1, a1)), ((n1, n2), (n3,)))
1154 #### `unify()` version 3
1158 def unify(u, v, s=None):
1168 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
1175 raise TypeError('Cannot unify %r and %r.' % (u, v))
1177 if isinstance(u, tuple) and isinstance(v, tuple):
1178 if len(u) != len(v) != 2:
1179 raise TypeError(repr((u, v)))
1180 for uu, vv in zip(u, v):
1181 s = unify(uu, vv, s)
1182 if s == False: # (instead of a substitution dict.)
1186 if isinstance(v, tuple):
1188 raise TypeError('Cannot unify %r and %r.' % (u, v))
1192 if isinstance(u, tuple):
1194 raise TypeError('Cannot unify %r and %r.' % (v, u))
1202 return thing.__class__ in {AnyJoyType, StackJoyType}
1205 Rewrite the stack effect comments:
1211 rolldown = (A[1], A[2], A[3]), (A[2], A[3], A[1])
1213 rollup = (A[1], A[2], A[3]), (A[3], A[1], A[2])
1217 popop = (A[2], A[1],), ()
1219 popd = (A[2], A[1],), (A[1],)
1221 popdd = (A[3], A[2], A[1],), (A[2], A[1],)
1223 swap = (A[1], A[2]), (A[2], A[1])
1225 rest = ((A[1], S[1]),), (S[1],)
1227 rrest = C(rest, rest)
1229 cons = (A[1], S[1]), ((A[1], S[1]),)
1231 ccons = C(cons, cons)
1233 uncons = ((A[1], S[1]),), (A[1], S[1])
1235 swons = C(swap, cons)
1237 dup = (A[1],), (A[1], A[1])
1239 dupd = (A[2], A[1]), (A[2], A[2], A[1])
1241 mul = (N[1], N[2]), (N[3],)
1245 first = ((A[1], S[1]),), (A[1],)
1247 second = C(rest, first)
1249 third = C(rest, second)
1251 tuck = (A[2], A[1]), (A[1], A[2], A[1])
1253 over = (A[2], A[1]), (A[2], A[1], A[2])
1255 succ = pred = (N[1],), (N[2],)
1257 divmod_ = pm = (N[2], N[1]), (N[4], N[3])
1269 for name, stack_effect_comment in sorted(DEFS.items()):
1270 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1273 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1274 cons = (a1 [.1.] -- [a1 .1.])
1275 divmod_ = (n2 n1 -- n4 n3)
1277 dupd = (a2 a1 -- a2 a2 a1)
1278 first = ([a1 .1.] -- a1)
1280 over = (a2 a1 -- a2 a1 a2)
1281 pm = (n2 n1 -- n4 n3)
1283 popd = (a2 a1 -- a1)
1284 popdd = (a3 a2 a1 -- a2 a1)
1287 rest = ([a1 .1.] -- [.1.])
1288 rolldown = (a1 a2 a3 -- a2 a3 a1)
1289 rollup = (a1 a2 a3 -- a3 a1 a2)
1290 rrest = ([a1 a2 .1.] -- [.1.])
1291 second = ([a1 a2 .1.] -- a2)
1294 swap = (a1 a2 -- a2 a1)
1295 swons = ([.1.] a1 -- [a1 .1.])
1296 third = ([a1 a2 a3 .1.] -- a3)
1297 tuck = (a2 a1 -- a1 a2 a1)
1298 uncons = ([a1 .1.] -- a1 [.1.])
1303 globals().update(DEFS)
1306 #### Compose `dup` and `mul`
1320 Revisit the `F` function, works fine.
1324 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
1331 (((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
1337 print doc_from_stack_effect(*F)
1340 ([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])
1343 Some otherwise inefficient functions are no longer to be feared. We can also get the effect of combinators in some limited cases.
1348 print doc_from_stack_effect(*reduce(C, funcs))
1354 neato(rollup, swap, rolldown)
1357 (a1 a2 a3 -- a2 a1 a3)
1363 neato(popdd, rolldown, pop)
1366 (a1 a2 a3 a4 -- a3 a4)
1371 # Reverse the order of the top three items.
1375 (a1 a2 a3 -- a3 a2 a1)
1378 #### `compile_()` version 2
1379 Because the type labels represent themselves as valid Python identifiers the `compile_()` function doesn't need to generate them anymore:
1383 def compile_(name, f, doc=None):
1386 doc = doc_from_stack_effect(inputs, outputs)
1387 i = o = Symbol('stack')
1390 for term in outputs:
1392 return '''def %s(stack):
1395 return %s''' % (name, doc, i, o)
1400 print compile_('F', F)
1404 """([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])"""
1405 (a5, (a4, (a3, ((a1, (a2, s1)), stack)))) = stack
1406 return ((a4, (a3, s1)), stack)
1409 But it cannot magically create new functions that involve e.g. math and such. Note that this is *not* a `sqr` function implementation:
1413 print compile_('sqr', C(dup, mul))
1422 (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.)
1425 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:
1429 from itertools import imap
1433 return isinstance(f, tuple) and all(imap(compilable, f)) or stacky(f)
1438 for name, stack_effect_comment in sorted(defs().items()):
1439 if compilable(stack_effect_comment):
1440 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1443 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1444 cons = (a1 [.1.] -- [a1 .1.])
1446 dupd = (a2 a1 -- a2 a2 a1)
1447 first = ([a1 .1.] -- a1)
1448 over = (a2 a1 -- a2 a1 a2)
1450 popd = (a2 a1 -- a1)
1451 popdd = (a3 a2 a1 -- a2 a1)
1453 rest = ([a1 .1.] -- [.1.])
1454 rolldown = (a1 a2 a3 -- a2 a3 a1)
1455 rollup = (a1 a2 a3 -- a3 a1 a2)
1456 rrest = ([a1 a2 .1.] -- [.1.])
1457 second = ([a1 a2 .1.] -- a2)
1458 swap = (a1 a2 -- a2 a1)
1459 swons = ([.1.] a1 -- [a1 .1.])
1460 third = ([a1 a2 a3 .1.] -- a3)
1461 tuck = (a2 a1 -- a1 a2 a1)
1462 uncons = ([a1 .1.] -- a1 [.1.])
1465 ## Part V: Functions that use the Stack
1467 Consider the `stack` function which grabs the whole stack, quotes it, and puts it on itself:
1469 stack (... -- ... [...] )
1470 stack (... a -- ... a [a ...] )
1471 stack (... b a -- ... b a [a b ...])
1473 We would like to represent this in Python somehow.
1474 To do this we use a simple, elegant trick.
1477 stack (a, S) -- ( (a, S), (a, S))
1478 stack (a, (b, S)) -- ( (a, (b, S)), (a, (b, S)))
1480 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.
1483 Let's try composing `stack` and `uncons`. We want this result:
1485 stack∘uncons (... a -- ... a a [...])
1487 The stack effects are:
1491 uncons = ((a, Z), S) -- (Z, (a, S))
1495 S -- (S, S) ∘ ((a, Z), S) -- (Z, (a, S ))
1497 (a, Z) -- ∘ -- (Z, (a, (a, Z)))
1501 stack∘uncons == (a, Z) -- (Z, (a, (a, Z)))
1505 ### `stack∘uncons∘uncons`
1506 Let's try `stack∘uncons∘uncons`:
1508 (a, S ) -- (S, (a, (a, S ))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1512 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1514 w/ { S`: (a, (a, (b, Z))) }
1516 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), (a, (a, (b, Z)))) -- (Z, (b, (a, (a, (b, Z)))))
1518 (a, (b, Z)) -- (Z, (b, (a, (a, (b, Z)))))
1522 #### `compose()` version 2
1523 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.)
1528 (f_in, f_out), (g_in, g_out) = f, g
1529 s = unify(g_in, f_out)
1530 if s == False: # s can also be the empty dict, which is ok.
1531 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
1532 return update(s, (f_in, g_out))
1535 I don't want to rewrite all the defs myself, so I'll write a little conversion function instead. This is programmer's laziness.
1539 def sequence_to_stack(seq, stack=StackJoyType(23)):
1540 for item in seq: stack = item, stack
1544 name: (sequence_to_stack(i), sequence_to_stack(o))
1545 for name, (i, o) in DEFS.iteritems()
1547 NEW_DEFS['stack'] = S[0], (S[0], S[0])
1548 NEW_DEFS['swaack'] = (S[1], S[0]), (S[0], S[1])
1549 globals().update(NEW_DEFS)
1560 ((a1, s1), (s1, (a1, (a1, s1))))
1566 reduce(C, (stack, uncons, uncons))
1572 ((a1, (a2, s1)), (s1, (a2, (a1, (a1, (a2, s1))))))
1576 The display function should be changed too.
1578 ### `doc_from_stack_effect()` version 2
1579 Clunky junk, but it will suffice for now.
1583 def doc_from_stack_effect(inputs, outputs):
1584 switch = [False] # Do we need to display the '...' for the rest of the main stack?
1585 i, o = _f(inputs, switch), _f(outputs, switch)
1589 return '(%s--%s)' % (
1590 ' '.join(reversed([''] + i)),
1591 ' '.join(reversed(o + [''])),
1595 def _f(term, switch):
1597 while term and isinstance(term, tuple):
1600 assert isinstance(term, StackJoyType), repr(term)
1601 a = [_to_str(i, term, switch) for i in a]
1605 def _to_str(term, stack, switch):
1606 if not isinstance(term, tuple):
1611 '[.%i.]' % term.number
1612 if isinstance(term, StackJoyType)
1617 while term and isinstance(term, tuple):
1619 a.append(_to_str(item, stack, switch))
1620 assert isinstance(term, StackJoyType), repr(term)
1625 end = '.%i.' % term.number
1627 return '[%s]' % ' '.join(a)
1632 for name, stack_effect_comment in sorted(NEW_DEFS.items()):
1633 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1636 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1637 cons = (a1 [.1.] -- [a1 .1.])
1638 divmod_ = (n2 n1 -- n4 n3)
1640 dupd = (a2 a1 -- a2 a2 a1)
1641 first = ([a1 .1.] -- a1)
1643 over = (a2 a1 -- a2 a1 a2)
1644 pm = (n2 n1 -- n4 n3)
1646 popd = (a2 a1 -- a1)
1647 popdd = (a3 a2 a1 -- a2 a1)
1650 rest = ([a1 .1.] -- [.1.])
1651 rolldown = (a1 a2 a3 -- a2 a3 a1)
1652 rollup = (a1 a2 a3 -- a3 a1 a2)
1653 rrest = ([a1 a2 .1.] -- [.1.])
1654 second = ([a1 a2 .1.] -- a2)
1656 stack = (... -- ... [...])
1658 swaack = ([.1.] -- [.0.])
1659 swap = (a1 a2 -- a2 a1)
1660 swons = ([.1.] a1 -- [a1 .1.])
1661 third = ([a1 a2 a3 .1.] -- a3)
1662 tuck = (a2 a1 -- a1 a2 a1)
1663 uncons = ([a1 .1.] -- a1 [.1.])
1668 print ; print doc_from_stack_effect(*stack)
1669 print ; print doc_from_stack_effect(*C(stack, uncons))
1670 print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, uncons)))
1671 print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, cons)))
1677 (... a1 -- ... a1 a1 [...])
1679 (... a2 a1 -- ... a2 a1 a1 a2 [...])
1681 (... a1 -- ... a1 [a1 ...])
1686 print doc_from_stack_effect(*C(ccons, stack))
1689 (... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])
1702 ((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
1706 #### `compile_()` version 3
1707 This makes the `compile_()` function pretty simple as the stack effect comments are now already in the form needed for the Python code:
1711 def compile_(name, f, doc=None):
1714 doc = doc_from_stack_effect(i, o)
1715 return '''def %s(stack):
1718 return %s''' % (name, doc, i, o)
1723 print compile_('Q', Q)
1727 """(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])"""
1728 (s1, (a1, (a2, s2))) = stack
1729 return (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2))
1759 unstack = (S[1], S[0]), S[1]
1760 enstacken = S[0], (S[0], S[1])
1765 print doc_from_stack_effect(*unstack)
1773 print doc_from_stack_effect(*enstacken)
1781 print doc_from_stack_effect(*C(cons, unstack))
1789 print doc_from_stack_effect(*C(cons, enstacken))
1792 (a1 [.1.] -- [[a1 .1.] .2.])
1803 ((s1, (a1, s2)), (a1, s1))
1812 ## Part VI: Multiple Stack Effects
1817 class IntJoyType(NumberJoyType): prefix = 'i'
1820 F = map(FloatJoyType, _R)
1821 I = map(IntJoyType, _R)
1827 ((I[2], (I[1], S[0])), (I[3], S[0])),
1828 ((F[2], (I[1], S[0])), (F[3], S[0])),
1829 ((I[2], (F[1], S[0])), (F[3], S[0])),
1830 ((F[2], (F[1], S[0])), (F[3], S[0])),
1837 print doc_from_stack_effect(*f)
1853 print doc_from_stack_effect(*dup), doc_from_stack_effect(*f), doc_from_stack_effect(*e)
1856 (a1 -- a1 a1) (i1 i2 -- i3) (i1 -- i2)
1857 (a1 -- a1 a1) (f1 f2 -- f3) (f1 -- f2)
1862 from itertools import product
1865 def meta_compose(F, G):
1866 for f, g in product(F, G):
1874 return sorted(set(meta_compose(F, G)))
1879 for f in MC([dup], [mul]):
1880 print doc_from_stack_effect(*f)
1888 for f in MC([dup], muls):
1889 print doc_from_stack_effect(*f)
1896 ### Representing an Unbounded Sequence of Types
1898 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:
1902 The `A*` works by splitting the universe into two alternate histories:
1906 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.
1908 Consider unifying two stacks (the lowercase letters are any type variables of the kinds we have defined so far):
1910 [a A* b .0.] U [c d .1.]
1912 [ A* b .0.] U [ d .1.]
1914 Now we have to split universes to unify `A*`. In the first universe it disappears:
1920 While in the second it spawns an `A`, which we will label `e`:
1922 [e A* b .0.] U [d .1.]
1924 [ A* b .0.] U [ .1.]
1926 [ A* b .0.] U [ A* b .0.]
1928 Giving us two unifiers:
1930 {c: a, d: b, .1.: .0.}
1931 {c: a, d: e, .1.: A* b .0.}
1935 class KleeneStar(object):
1939 def __init__(self, number):
1940 self.number = number
1942 self.prefix = repr(self)
1945 return '%s%i*' % (self.kind.prefix, self.number)
1949 return self.kind(10000 * self.number + self.count)
1951 def __eq__(self, other):
1953 isinstance(other, self.__class__)
1954 and other.number == self.number
1957 def __ge__(self, other):
1958 return self.kind >= other.kind
1960 def __add__(self, other):
1961 return self.__class__(self.number + other)
1965 return hash(repr(self))
1967 class AnyStarJoyType(KleeneStar): kind = AnyJoyType
1968 class NumberStarJoyType(KleeneStar): kind = NumberJoyType
1969 #class FloatStarJoyType(KleeneStar): kind = FloatJoyType
1970 #class IntStarJoyType(KleeneStar): kind = IntJoyType
1971 class StackStarJoyType(KleeneStar): kind = StackJoyType
1974 As = map(AnyStarJoyType, _R)
1975 Ns = map(NumberStarJoyType, _R)
1976 Ss = map(StackStarJoyType, _R)
1979 #### `unify()` version 4
1980 Can now return multiple results...
1984 def unify(u, v, s=None):
1994 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
2001 raise TypeError('Cannot unify %r and %r.' % (u, v))
2003 if isinstance(u, tuple) and isinstance(v, tuple):
2004 if len(u) != len(v) != 2:
2005 raise TypeError(repr((u, v)))
2008 if isinstance(a, KleeneStar):
2009 # Two universes, in one the Kleene star disappears and unification
2010 # continues without it...
2013 # In the other it spawns a new variable.
2014 s1 = unify(u, (a.another(), v))
2022 if isinstance(a, KleeneStar):
2024 s1 = unify(v, (a.another(), u))
2030 ses = unify(u[0], v[0], s)
2033 results += unify(u[1], v[1], sn)
2036 if isinstance(v, tuple):
2038 raise TypeError('Cannot unify %r and %r.' % (u, v))
2042 if isinstance(u, tuple):
2044 raise TypeError('Cannot unify %r and %r.' % (v, u))
2052 return thing.__class__ in {AnyJoyType, StackJoyType}
2083 for result in unify(b, a):
2084 print result, '->', update(result, a), update(result, b)
2087 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2088 {a1: a10001, s2: (a1*, s1)} -> (a1*, s1) (a10001, (a1*, s1))
2093 for result in unify(a, b):
2094 print result, '->', update(result, a), update(result, b)
2097 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2098 {a1: a10002, s2: (a1*, s1)} -> (a1*, s1) (a10002, (a1*, s1))
2102 (a1*, s1) [a1*] (a1, s2) [a1]
2104 (a1*, (a1, s2)) [a1* a1] (a1, s2) [a1]
2106 (a1*, s1) [a1*] (a2, (a1*, s1)) [a2 a1*]
2110 sum_ = ((Ns[1], S[1]), S[0]), (N[0], S[0])
2112 print doc_from_stack_effect(*sum_)
2120 f = (N[1], (N[2], (N[3], S[1]))), S[0]
2122 print doc_from_stack_effect(S[0], f)
2130 for result in unify(sum_[0], f):
2131 print result, '->', update(result, sum_[1])
2134 {s1: (n1, (n2, (n3, s1)))} -> (n0, s0)
2135 {n1: n10001, s1: (n2, (n3, s1))} -> (n0, s0)
2136 {n1: n10001, s1: (n3, s1), n2: n10002} -> (n0, s0)
2137 {n1: n10001, s1: (n1*, s1), n3: n10003, n2: n10002} -> (n0, s0)
2140 #### `compose()` version 3
2141 This function has to be modified to yield multiple results.
2146 (f_in, f_out), (g_in, g_out) = f, g
2147 s = unify(g_in, f_out)
2149 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2151 yield update(result, (f_in, g_out))
2162 def meta_compose(F, G):
2163 for f, g in product(F, G):
2165 for result in C(f, g):
2172 f, g = relabel(f, g)
2173 for fg in compose(f, g):
2179 for f in MC([dup], muls):
2180 print doc_from_stack_effect(*f)
2191 for f in MC([dup], [sum_]):
2192 print doc_from_stack_effect(*f)
2195 ([n1* .1.] -- [n1* .1.] n1)
2202 for f in MC([cons], [sum_]):
2203 print doc_from_stack_effect(*f)
2207 (n1 [n1* .1.] -- n2)
2212 sum_ = (((N[1], (Ns[1], S[1])), S[0]), (N[0], S[0]))
2213 print doc_from_stack_effect(*cons),
2214 print doc_from_stack_effect(*sum_),
2216 for f in MC([cons], [sum_]):
2217 print doc_from_stack_effect(*f)
2220 (a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n1 [n1* .1.] -- n2)
2225 a = (A[4], (As[1], (A[3], S[1])))
2232 (a4, (a1*, (a3, s1)))
2238 b = (A[1], (A[2], S[2]))
2251 for result in unify(b, a):
2255 {a1: a4, s2: s1, a2: a3}
2256 {a1: a4, s2: (a1*, (a3, s1)), a2: a10003}
2261 for result in unify(a, b):
2265 {s2: s1, a2: a3, a4: a1}
2266 {s2: (a1*, (a3, s1)), a2: a10004, a4: a1}
2269 ## Part VII: Typing Combinators
2271 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:
2273 i (... [.1.] -- ... .1.)
2277 i (... [A* .1.] -- ... A*)
2279 Consider the type of:
2283 Obviously it would be:
2285 (a1 [..1] a2 -- [a1 ..1] a2)
2287 `dip` itself could have:
2289 (a1 [..1] -- ... then what?
2292 Without any information about the contents of the quote we can't say much about the result.
2294 ### Hybrid Inferencer/Interpreter
2295 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.
2297 #### Joy Types for Functions
2298 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.
2302 class FunctionJoyType(AnyJoyType):
2304 def __init__(self, name, sec, number):
2306 self.stack_effects = sec
2307 self.number = number
2309 def __add__(self, other):
2317 #### Specialized for Simple Functions and Combinators
2318 For non-combinator functions the stack effects list contains stack effect comments (represented by pairs of cons-lists as described above.)
2322 class SymbolJoyType(FunctionJoyType):
2326 For combinators the list contains Python functions.
2330 class CombinatorJoyType(FunctionJoyType):
2334 def __init__(self, name, sec, number, expect=None):
2335 super(CombinatorJoyType, self).__init__(name, sec, number)
2336 self.expect = expect
2338 def enter_guard(self, f):
2339 if self.expect is None:
2341 g = self.expect, self.expect
2342 new_f = list(compose(f, g, ()))
2343 assert len(new_f) == 1, repr(new_f)
2347 For simple combinators that have only one effect (like ``dip``) you only need one function and it can be the combinator itself.
2353 dip = CombinatorJoyType('dip', [joy.library.dip], 23)
2356 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.
2360 def branch_true(stack, expression, dictionary):
2361 (then, (else_, (flag, stack))) = stack
2362 return stack, concat(then, expression), dictionary
2364 def branch_false(stack, expression, dictionary):
2365 (then, (else_, (flag, stack))) = stack
2366 return stack, concat(else_, expression), dictionary
2368 branch = CombinatorJoyType('branch', [branch_true, branch_false], 100)
2371 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.
2374 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.
2376 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.
2380 ID = S[0], S[0] # Identity function.
2383 def infer(*expression):
2384 return sorted(set(_infer(list_to_stack(expression))))
2387 def _infer(e, F=ID):
2394 if isinstance(n, SymbolJoyType):
2395 eFG = meta_compose([F], n.stack_effects, e)
2396 res = flatten(_infer(e, Fn) for e, Fn in eFG)
2398 elif isinstance(n, CombinatorJoyType):
2399 fi, fo = n.enter_guard(F)
2400 res = flatten(_interpret(f, fi, fo, e) for f in n.stack_effects)
2402 elif isinstance(n, Symbol):
2403 assert n not in FUNCTIONS, repr(n)
2404 func = joy.library._dictionary[n]
2405 res = _interpret(func, F[0], F[1], e)
2409 res = _infer(e, (fi, (n, fo)))
2414 def _interpret(f, fi, fo, e):
2415 new_fo, ee, _ = f(fo, e, {})
2416 ee = update(FUNCTIONS, ee) # Fix Symbols.
2418 return _infer(ee, new_F)
2424 len(inspect_stack()),
2425 doc_from_stack_effect(*F),
2426 expression_to_string(e),
2430 #### Work in Progress
2431 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 :
2435 1/0 # (Don't try to run this cell! It's not going to work. This is "read only" code heh..)
2437 logging.basicConfig(format='%(message)s', stream=sys.stdout, level=logging.INFO)
2439 globals().update(FUNCTIONS)
2441 h = infer((pred, s2), (mul, s3), (div, s4), (nullary, (bool, s5)), dipd, branch)
2446 print doc_from_stack_effect(fi, fo)
2450 ---------------------------------------------------------------------------
2452 ZeroDivisionError Traceback (most recent call last)
2454 <ipython-input-1-9a9d60354c35> in <module>()
2455 ----> 1 1/0 # (Don't try to run this cell! It's not going to work. This is "read only" code heh..)
2457 3 logging.basicConfig(format='%(message)s', stream=sys.stdout, level=logging.INFO)
2459 5 globals().update(FUNCTIONS)
2462 ZeroDivisionError: integer division or modulo by zero
2465 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.)
2467 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.
2469 7 (--) ∘ [pred] [mul] [div] [nullary bool] dipd branch
2470 8 (-- [pred ...2]) ∘ [mul] [div] [nullary bool] dipd branch
2471 9 (-- [pred ...2] [mul ...3]) ∘ [div] [nullary bool] dipd branch
2472 10 (-- [pred ...2] [mul ...3] [div ...4]) ∘ [nullary bool] dipd branch
2473 11 (-- [pred ...2] [mul ...3] [div ...4] [nullary bool ...5]) ∘ dipd branch
2474 15 (-- [pred ...5]) ∘ nullary bool [mul] [div] branch
2475 19 (-- [pred ...2]) ∘ [stack] dinfrirst bool [mul] [div] branch
2476 20 (-- [pred ...2] [stack ]) ∘ dinfrirst bool [mul] [div] branch
2477 22 (-- [pred ...2] [stack ]) ∘ dip infra first bool [mul] [div] branch
2478 26 (--) ∘ stack [pred] infra first bool [mul] [div] branch
2479 29 (... -- ... [...]) ∘ [pred] infra first bool [mul] [div] branch
2480 30 (... -- ... [...] [pred ...1]) ∘ infra first bool [mul] [div] branch
2481 34 (--) ∘ pred s1 swaack first bool [mul] [div] branch
2482 37 (n1 -- n2) ∘ [n1] swaack first bool [mul] [div] branch
2483 38 (... n1 -- ... n2 [n1 ...]) ∘ swaack first bool [mul] [div] branch
2484 41 (... n1 -- ... n1 [n2 ...]) ∘ first bool [mul] [div] branch
2485 44 (n1 -- n1 n2) ∘ bool [mul] [div] branch
2486 47 (n1 -- n1 b1) ∘ [mul] [div] branch
2487 48 (n1 -- n1 b1 [mul ...1]) ∘ [div] branch
2488 49 (n1 -- n1 b1 [mul ...1] [div ...2]) ∘ branch
2499 ----------------------------------------
2507 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
2509 Work remains to be done:
2511 - the rest of the library has to be covered
2512 - figure out how to deal with `loop` and `genrec`, etc..
2513 - extend the types to check values (see the appendix)
2514 - other kinds of "higher order" type variables, OR, AND, etc..
2515 - maybe rewrite in Prolog for great good?
2517 - don't permit composition of functions that don't compose
2518 - auto-compile compilable functions
2519 - Compiling more than just the Yin functions.
2520 - getting better visibility (than Python debugger.)
2521 - DOOOOCS!!!! Lots of docs!
2522 - docstrings all around
2523 - 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.
2525 ## Appendix: Joy in the Logical Paradigm
2527 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!
2529 Anyhow, type *checking* is a few easy steps away.
2533 def _ge(self, other):
2534 return (issubclass(other.__class__, self.__class__)
2535 or hasattr(self, 'accept')
2536 and isinstance(other, self.accept))
2538 AnyJoyType.__ge__ = _ge
2539 AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
2540 StackJoyType.accept = tuple