2 # The Blissful Elegance of Typing Joy
4 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.)
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. (Yin functions are those that only rearrange values in stacks, as opposed to Yang functions that actually work on the values themselves.)
10 ## Part I: Pöial's Rules
12 ["Typing Tools for Typeless Stack Languages" by Jaanus Pöial
13 ](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.212.6026)
15 @INPROCEEDINGS{Pöial06typingtools,
16 author = {Jaanus Pöial},
17 title = {Typing tools for typeless stack languages},
18 booktitle = {In 23rd Euro-Forth Conference},
24 This rule deals with functions (and literals) that put items on the stack `(-- d)`:
32 This rule deals with functions that consume items from the stack `(a --)`:
39 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.
41 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
42 -------------------------------
43 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
46 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
47 -------------------------------
48 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
50 Let's work through some examples by hand to develop an intuition for the algorithm.
52 There's a function in one of the other notebooks.
54 F == pop swap roll< rest rest cons cons
56 It's all "stack chatter" and list manipulation so we should be able to deduce its type.
58 ### Stack Effect Comments
59 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):
65 roll< (1 2 3 -- 2 3 1)
67 These commands alter the stack but don't "look at" the values so these numbers represent an "Any type".
73 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:
77 Following the second rule:
83 (1 2 0 -- 2 1) (1 2 3 -- 2 3 1)
87 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
89 Now we follow the rules.
91 We must unify `1a` and `3b`, and `2a` and `2b`, replacing the terms in the forms:
93 (1a 2a 0a -- 2a 1a) (1b 2b 3b -- 2b 3b 1b)
95 (3b 2a 0a -- 2a ) (1b 2b -- 2b 3b 1b)
97 (3b 2b 0a -- ) (1b -- 2b 3b 1b)
99 Here we must apply the second rule:
101 (3b 2b 0a --) (1b -- 2b 3b 1b)
102 -----------------------------------
103 (1b 3b 2b 0a -- 2b 3b 1b)
105 Now we de-label the type, uh, labels:
107 (1b 3b 2b 0a -- 2b 3b 1b)
118 And now we have the stack effect comment for `pop∘swap∘roll<`.
120 ### Compiling `pop∘swap∘roll<`
121 The simplest way to "compile" this function would be something like:
126 return rolldown(*swap(*pop(s, e, d)))
129 However, internally this function would still be allocating tuples (stack cells) and doing other unnecesssary work.
131 Looking ahead for a moment, from the stack effect comment:
135 We should be able to directly write out a Python function like:
140 (_, (a, (b, (c, stack)))) = stack
141 return (c, (b, (a, stack)))
144 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.
146 ### Functions on Stacks
147 These are slightly tricky.
149 rest ( [1 ...] -- [...] )
151 cons ( 1 [...] -- [1 ...] )
153 ### `pop∘swap∘roll< rest`
155 (1 2 3 0 -- 3 2 1) ([1 ...] -- [...])
157 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):
159 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
163 (1 2 3 0 -- 3 2 1) ([4 ...] -- [...])
165 ([4 ...] 2 3 0 -- 3 2 ) ( -- [...])
167 Apply the first rule:
169 ([4 ...] 2 3 0 -- 3 2) (-- [...])
170 ---------------------------------------
171 ([4 ...] 2 3 0 -- 3 2 [...])
175 ### `pop∘swap∘roll<∘rest rest`
179 ([4 ...] 2 3 0 -- 3 2 [...]) ([1 ...] -- [...])
181 Re-label (the tails of the lists on each side each get their own label):
183 ([4 .0.] 2 3 0 -- 3 2 [.0.]) ([5 .1.] -- [.1.])
185 Unify and update (note the opening square brackets have been omited in the substitution dict, this is deliberate and I'll explain below):
187 ([4 .0.] 2 3 0 -- 3 2 [.0.] ) ([5 .1.] -- [.1.])
189 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
191 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.
193 Next we unify and find our two terms are the same already: `[5 .1.]`:
195 ([4 5 .1.] 2 3 0 -- 3 2 [5 .1.]) ([5 .1.] -- [.1.])
199 ([4 5 .1.] 2 3 0 -- 3 2) (-- [.1.])
201 From here we apply the first rule and get:
203 ([4 5 .1.] 2 3 0 -- 3 2 [.1.])
205 Cleaning up the labels:
207 ([4 5 ...] 2 3 1 -- 3 2 [...])
209 This is the stack effect of `pop∘swap∘roll<∘rest∘rest`.
211 ### `pop∘swap∘roll<∘rest∘rest cons`
213 ([4 5 ...] 2 3 1 -- 3 2 [...]) (1 [...] -- [1 ...])
217 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
221 ([4 5 .1.] 2 3 1 -- 3 2 [.1.]) (6 [.2.] -- [6 .2.])
223 ([4 5 .2.] 2 3 1 -- 3 2 ) (6 -- [6 .2.])
225 ([4 5 .2.] 6 3 1 -- 3 ) ( -- [6 .2.])
229 ([4 5 .2.] 6 3 1 -- 3 [6 .2.])
233 ([4 5 ...] 2 3 1 -- 3 [2 ...])
237 ### `pop∘swap∘roll<∘rest∘rest∘cons cons`
240 ([4 5 ...] 2 3 1 -- 3 [2 ...]) (1 [...] -- [1 ...])
244 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.])
248 ([4 5 .1.] 2 3 1 -- 3 [2 .1.]) (6 [.2.] -- [6 .2.] )
250 ([4 5 .1.] 2 3 1 -- 3 ) (6 -- [6 2 .1.])
252 ([4 5 .1.] 2 6 1 -- ) ( -- [6 2 .1.])
254 First or second rule:
256 ([4 5 .1.] 2 6 1 -- [6 2 .1.])
260 ([4 5 ...] 2 3 1 -- [3 2 ...])
262 And there you have it, the stack effect for `pop∘swap∘roll<∘rest∘rest∘cons∘cons`.
264 ([4 5 ...] 2 3 1 -- [3 2 ...])
266 From this stack effect comment it should be possible to construct the following Python code:
271 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
272 return (d, (c, S0)), stack
275 ## Part II: Implementation
277 ### Representing Stack Effect Comments in Python
279 I'm going to use pairs of tuples of type descriptors, which will be integers or tuples of type descriptors:
283 roll_dn = (1, 2, 3), (2, 3, 1)
287 swap = (1, 2), (2, 1)
296 (f_in, f_out), (g_in, g_out) = f, g
301 # ---------------------
306 fg_in, fg_out = f_in, f_out + g_out
311 # ---------------------
316 fg_in, fg_out = g_in + f_in, g_out
318 else: # Unify, update, recur.
320 fo, gi = f_out[-1], g_in[-1]
324 if s == False: # s can also be the empty dict, which is ok.
325 raise TypeError('Cannot unify %r and %r.' % (fo, gi))
327 f_g = (f_in, f_out[:-1]), (g_in[:-1], g_out)
329 if s: f_g = update(s, f_g)
331 fg_in, fg_out = compose(*f_g)
340 def unify(u, v, s=None):
344 if isinstance(u, int):
346 elif isinstance(v, int):
359 if not isinstance(term, tuple):
360 return s.get(term, term)
361 return tuple(update(s, inner) for inner in term)
368 def relabel(left, right):
369 return left, _1000(right)
372 if not isinstance(right, tuple):
374 return tuple(_1000(n) for n in right)
382 (((1,), ()), ((1001, 1002), (1002, 1001)))
391 s = {u: i for i, u in enumerate(sorted(_unique(f)))}
394 def _unique(f, seen=None):
397 if not isinstance(f, tuple):
404 delabel(relabel(pop, swap))
410 (((0,), ()), ((1, 2), (2, 1)))
416 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.)
442 C(C(pop, swap), roll_dn)
448 ((3, 1, 2, 0), (2, 1, 3))
460 ((2, 0, 1), (1, 0, 2))
466 C(pop, C(swap, roll_dn))
472 ((3, 1, 2, 0), (2, 1, 3))
478 poswrd = reduce(C, (pop, swap, roll_dn))
485 ((3, 1, 2, 0), (2, 1, 3))
490 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.
494 rest = ((1, 2),), (2,)
496 cons = (1, 2), ((1, 2),)
507 (((3, 4), 1, 2, 0), (2, 1, 4))
511 Compare this to the stack effect comment we wrote above:
513 (( (3, 4), 1, 2, 0 ), ( 2, 1, 4 ))
514 ( [4 ...] 2 3 0 -- 3 2 [...])
516 The translation table, if you will, would be:
528 F = reduce(C, (pop, swap, roll_dn, rest, rest, cons, cons))
536 (((3, (4, 5)), 1, 2, 0), ((2, (1, 5)),))
540 Compare with the stack effect comment and you can see it works fine:
542 ([4 5 ...] 2 3 1 -- [3 2 ...])
545 ### Dealing with `cons` and `uncons`
546 However, if we try to compose e.g. `cons` and `uncons` it won't work:
550 uncons = ((1, 2),), (1, 2)
561 Cannot unify (1, 2) and (1001, 1002).
564 #### `unify()` version 2
565 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:
569 def unify(u, v, s=None):
576 if isinstance(u, int):
579 elif isinstance(v, int):
582 elif isinstance(u, tuple) and isinstance(v, tuple):
584 if len(u) != 2 or len(v) != 2:
585 # Not a type error, caller passed in a bad value.
586 raise ValueError(repr((u, v))) # FIXME this message sucks.
588 (a, b), (c, d) = u, v
610 ## Part III: Compiling Yin Functions
611 Now consider the Python function we would like to derive:
616 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
617 return (d, (c, S0)), stack
620 And compare it to the input stack effect comment tuple we just computed:
630 ((3, (4, 5)), 1, 2, 0)
634 The stack-de-structuring tuple has nearly the same form as our input stack effect comment tuple, just in the reverse order:
636 (_, (d, (c, ((a, (b, S0)), stack))))
638 Remove the punctuation:
642 Reverse the order and compare:
645 ((3, (4, 5 )), 1, 2, 0)
663 is similar to the output stack effect comment tuple:
665 ((d, (c, S0)), stack)
668 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.)
670 ### Python Identifiers
671 We want to substitute Python identifiers for the integers. I'm going to repurpose `joy.parser.Symbol` class for this:
675 from collections import defaultdict
676 from joy.parser import Symbol
680 I = iter(xrange(1000))
681 return lambda: Symbol('a%i' % next(I))
684 def identifiers(term, s=None):
686 s = defaultdict(_names_for())
687 if isinstance(term, int):
689 return tuple(identifiers(inner, s) for inner in term)
692 ### `doc_from_stack_effect()`
693 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.
697 def doc_from_stack_effect(inputs, outputs):
698 return '(%s--%s)' % (
699 ' '.join(map(_to_str, inputs + ('',))),
700 ' '.join(map(_to_str, ('',) + outputs))
705 if not isinstance(term, tuple):
707 t = term.prefix == 's'
708 except AttributeError:
710 return '[.%i.]' % term.number if t else str(term)
713 while term and isinstance(term, tuple):
715 a.append(_to_str(item))
719 except AttributeError:
722 if term.prefix != 's':
723 raise ValueError('Stack label: %s' % (term,))
725 a.append('.%s.' % (n,))
726 return '[%s]' % ' '.join(a)
730 Now we can write a compiler function to emit Python source code. (The underscore suffix distiguishes it from the built-in `compile()` function.)
734 def compile_(name, f, doc=None):
736 doc = doc_from_stack_effect(*f)
737 inputs, outputs = identifiers(f)
738 i = o = Symbol('stack')
743 return '''def %s(stack):
746 return %s''' % (name, doc, i, o)
749 Here it is in action:
753 source = compile_('F', F)
759 """([3 4 .5.] 1 2 0 -- [2 1 .5.])"""
760 (a5, (a4, (a3, ((a0, (a1, a2)), stack)))) = stack
761 return ((a4, (a3, a2)), stack)
769 (_, (d, (c, ((a, (b, S0)), stack)))) = stack
770 return ((d, (c, S0)), stack)
779 eval(compile(source, '__main__', 'single'), {}, L)
795 from notebook_preamble import D, J, V
796 from joy.library import SimpleFunctionWrapper
801 D['F'] = SimpleFunctionWrapper(L['F'])
806 J('[4 5 ...] 2 3 1 F')
812 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.)
814 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.
816 ### Compiling Library Functions
817 We can use `compile_()` to generate many primitives in the library from their stack effect comments:
823 rolldown = (1, 2, 3), (2, 3, 1)
825 rollup = (1, 2, 3), (3, 1, 2)
829 swap = (1, 2), (2, 1)
831 rest = ((1, 2),), (2,)
833 rrest = C(rest, rest)
835 cons = (1, 2), ((1, 2),)
837 uncons = ((1, 2),), (1, 2)
839 swons = C(swap, cons)
846 for name, stack_effect_comment in sorted(defs().items()):
848 print compile_(name, stack_effect_comment)
854 """(1 2 -- [1 .2.])"""
855 (a1, (a0, stack)) = stack
856 return ((a0, a1), stack)
867 ((a0, a1), stack) = stack
872 """(1 2 3 -- 2 3 1)"""
873 (a2, (a1, (a0, stack))) = stack
874 return (a0, (a2, (a1, stack)))
878 """(1 2 3 -- 3 1 2)"""
879 (a2, (a1, (a0, stack))) = stack
880 return (a1, (a0, (a2, stack)))
884 """([0 1 .2.] -- 2)"""
885 ((a0, (a1, a2)), stack) = stack
891 (a1, (a0, stack)) = stack
892 return (a0, (a1, stack))
896 """(0 1 -- [1 .0.])"""
897 (a1, (a0, stack)) = stack
898 return ((a1, a0), stack)
902 """([1 .2.] -- 1 2)"""
903 ((a0, a1), stack) = stack
904 return (a1, (a0, stack))
908 ## Part IV: Types and Subtypes of Arguments
909 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.
913 Consider the definition of `sqr`:
918 The `dup` function accepts one *anything* and returns two of that:
922 And `mul` accepts two "numbers" (we're ignoring ints vs. floats vs. complex, etc., for now) and returns just one:
928 (1 -- 1 1)∘(n n -- n)
930 The rules say we unify 1 with `n`:
932 (1 -- 1 1)∘(n n -- n)
933 --------------------------- w/ {1: n}
936 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:
938 (n n -- n)∘(1 -- 1 1)
939 --------------------------- w/ {1: n}
942 The important thing here is that the mapping is going the same way in both cases, from the "any" integer to the number
944 ### Distinguishing Numbers
945 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:
950 (1 -- 1 1)∘(n2 n1 -- n3)
951 -------------------------------- w/ {1: n2}
952 (n2 -- n2 )∘(n2 -- n3)
955 (n2 n1 -- n3)∘(1 -- 1 1 )
956 -------------------------------- w/ {1: n3}
957 (n2 n1 -- )∘( -- n3 n3)
961 ### Distinguishing Types
962 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?
964 (a -- b t[i])∘(c u[j] -- d) t <= u (t is subtype of u)
965 -------------------------------
966 (a -- b )∘(c -- d) t[i] == t[k] == u[j]
969 (a -- b t[i])∘(c u[j] -- d) u <= t (u is subtype of t)
970 -------------------------------
971 (a -- b )∘(c -- d) t[i] == u[k] == u[j]
973 The indices `i`, `k`, and `j` are the number part of our labels and `t` and `u` are the domains.
975 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.
979 class AnyJoyType(object):
983 def __init__(self, number):
987 return self.prefix + str(self.number)
989 def __eq__(self, other):
991 isinstance(other, self.__class__)
992 and other.prefix == self.prefix
993 and other.number == self.number
996 def __ge__(self, other):
997 return issubclass(other.__class__, self.__class__)
999 def __add__(self, other):
1000 return self.__class__(self.number + other)
1004 return hash(repr(self))
1007 class NumberJoyType(AnyJoyType): prefix = 'n'
1008 class FloatJoyType(NumberJoyType): prefix = 'f'
1009 class IntJoyType(FloatJoyType): prefix = 'i'
1012 class StackJoyType(AnyJoyType):
1017 A = map(AnyJoyType, _R)
1018 N = map(NumberJoyType, _R)
1019 S = map(StackJoyType, _R)
1022 Mess with it a little:
1026 from itertools import permutations
1029 "Any" types can be specialized to numbers and stacks, but not vice versa:
1033 for a, b in permutations((A[0], N[0], S[0]), 2):
1034 print a, '>=', b, '->', a >= b
1045 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):
1049 for a, b in permutations((A[0], N[0], FloatJoyType(0), IntJoyType(0)), 2):
1050 print a, '>=', b, '->', a >= b
1071 dup = (A[1],), (A[1], A[1])
1073 mul = (N[1], N[2]), (N[3],)
1100 ### Modifying the Inferencer
1101 Re-labeling still works fine:
1105 foo = relabel(dup, mul)
1113 (((a1,), (a1, a1)), ((n1001, n1002), (n1003,)))
1117 #### `delabel()` version 2
1118 The `delabel()` function needs an overhaul. It now has to keep track of how many labels of each domain it has "seen".
1122 from collections import Counter
1125 def delabel(f, seen=None, c=None):
1128 seen, c = {}, Counter()
1135 if not isinstance(f, tuple):
1136 seen[f] = f.__class__(c[f.prefix] + 1)
1140 return tuple(delabel(inner, seen, c) for inner in f)
1151 (((a1,), (a1, a1)), ((n1, n2), (n3,)))
1155 #### `unify()` version 3
1159 def unify(u, v, s=None):
1169 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
1176 raise TypeError('Cannot unify %r and %r.' % (u, v))
1178 if isinstance(u, tuple) and isinstance(v, tuple):
1179 if len(u) != len(v) != 2:
1180 raise TypeError(repr((u, v)))
1181 for uu, vv in zip(u, v):
1182 s = unify(uu, vv, s)
1183 if s == False: # (instead of a substitution dict.)
1187 if isinstance(v, tuple):
1189 raise TypeError('Cannot unify %r and %r.' % (u, v))
1193 if isinstance(u, tuple):
1195 raise TypeError('Cannot unify %r and %r.' % (v, u))
1203 return thing.__class__ in {AnyJoyType, StackJoyType}
1206 Rewrite the stack effect comments:
1212 rolldown = (A[1], A[2], A[3]), (A[2], A[3], A[1])
1214 rollup = (A[1], A[2], A[3]), (A[3], A[1], A[2])
1218 popop = (A[2], A[1],), ()
1220 popd = (A[2], A[1],), (A[1],)
1222 popdd = (A[3], A[2], A[1],), (A[2], A[1],)
1224 swap = (A[1], A[2]), (A[2], A[1])
1226 rest = ((A[1], S[1]),), (S[1],)
1228 rrest = C(rest, rest)
1230 cons = (A[1], S[1]), ((A[1], S[1]),)
1232 ccons = C(cons, cons)
1234 uncons = ((A[1], S[1]),), (A[1], S[1])
1236 swons = C(swap, cons)
1238 dup = (A[1],), (A[1], A[1])
1240 dupd = (A[2], A[1]), (A[2], A[2], A[1])
1242 mul = (N[1], N[2]), (N[3],)
1246 first = ((A[1], S[1]),), (A[1],)
1248 second = C(rest, first)
1250 third = C(rest, second)
1252 tuck = (A[2], A[1]), (A[1], A[2], A[1])
1254 over = (A[2], A[1]), (A[2], A[1], A[2])
1256 succ = pred = (N[1],), (N[2],)
1258 divmod_ = pm = (N[2], N[1]), (N[4], N[3])
1270 for name, stack_effect_comment in sorted(DEFS.items()):
1271 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1274 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1275 cons = (a1 [.1.] -- [a1 .1.])
1276 divmod_ = (n2 n1 -- n4 n3)
1278 dupd = (a2 a1 -- a2 a2 a1)
1279 first = ([a1 .1.] -- a1)
1281 over = (a2 a1 -- a2 a1 a2)
1282 pm = (n2 n1 -- n4 n3)
1284 popd = (a2 a1 -- a1)
1285 popdd = (a3 a2 a1 -- a2 a1)
1288 rest = ([a1 .1.] -- [.1.])
1289 rolldown = (a1 a2 a3 -- a2 a3 a1)
1290 rollup = (a1 a2 a3 -- a3 a1 a2)
1291 rrest = ([a1 a2 .1.] -- [.1.])
1292 second = ([a1 a2 .1.] -- a2)
1295 swap = (a1 a2 -- a2 a1)
1296 swons = ([.1.] a1 -- [a1 .1.])
1297 third = ([a1 a2 a3 .1.] -- a3)
1298 tuck = (a2 a1 -- a1 a2 a1)
1299 uncons = ([a1 .1.] -- a1 [.1.])
1304 globals().update(DEFS)
1307 #### Compose `dup` and `mul`
1321 Revisit the `F` function, works fine.
1325 F = reduce(C, (pop, swap, rolldown, rest, rest, cons, cons))
1332 (((a1, (a2, s1)), a3, a4, a5), ((a4, (a3, s1)),))
1338 print doc_from_stack_effect(*F)
1341 ([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])
1344 Some otherwise inefficient functions are no longer to be feared. We can also get the effect of combinators in some limited cases.
1349 print doc_from_stack_effect(*reduce(C, funcs))
1355 neato(rollup, swap, rolldown)
1358 (a1 a2 a3 -- a2 a1 a3)
1364 neato(popdd, rolldown, pop)
1367 (a1 a2 a3 a4 -- a3 a4)
1372 # Reverse the order of the top three items.
1376 (a1 a2 a3 -- a3 a2 a1)
1379 #### `compile_()` version 2
1380 Because the type labels represent themselves as valid Python identifiers the `compile_()` function doesn't need to generate them anymore:
1384 def compile_(name, f, doc=None):
1387 doc = doc_from_stack_effect(inputs, outputs)
1388 i = o = Symbol('stack')
1391 for term in outputs:
1393 return '''def %s(stack):
1396 return %s''' % (name, doc, i, o)
1401 print compile_('F', F)
1405 """([a1 a2 .1.] a3 a4 a5 -- [a4 a3 .1.])"""
1406 (a5, (a4, (a3, ((a1, (a2, s1)), stack)))) = stack
1407 return ((a4, (a3, s1)), stack)
1410 But it cannot magically create new functions that involve e.g. math and such. Note that this is *not* a `sqr` function implementation:
1414 print compile_('sqr', C(dup, mul))
1423 (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.)
1426 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:
1430 from itertools import imap
1434 return isinstance(f, tuple) and all(imap(compilable, f)) or stacky(f)
1439 for name, stack_effect_comment in sorted(defs().items()):
1440 if compilable(stack_effect_comment):
1441 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1444 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1445 cons = (a1 [.1.] -- [a1 .1.])
1447 dupd = (a2 a1 -- a2 a2 a1)
1448 first = ([a1 .1.] -- a1)
1449 over = (a2 a1 -- a2 a1 a2)
1451 popd = (a2 a1 -- a1)
1452 popdd = (a3 a2 a1 -- a2 a1)
1454 rest = ([a1 .1.] -- [.1.])
1455 rolldown = (a1 a2 a3 -- a2 a3 a1)
1456 rollup = (a1 a2 a3 -- a3 a1 a2)
1457 rrest = ([a1 a2 .1.] -- [.1.])
1458 second = ([a1 a2 .1.] -- a2)
1459 swap = (a1 a2 -- a2 a1)
1460 swons = ([.1.] a1 -- [a1 .1.])
1461 third = ([a1 a2 a3 .1.] -- a3)
1462 tuck = (a2 a1 -- a1 a2 a1)
1463 uncons = ([a1 .1.] -- a1 [.1.])
1466 ## Part V: Functions that use the Stack
1468 Consider the `stack` function which grabs the whole stack, quotes it, and puts it on itself:
1470 stack (... -- ... [...] )
1471 stack (... a -- ... a [a ...] )
1472 stack (... b a -- ... b a [a b ...])
1474 We would like to represent this in Python somehow.
1475 To do this we use a simple, elegant trick.
1478 stack (a, S) -- ( (a, S), (a, S))
1479 stack (a, (b, S)) -- ( (a, (b, S)), (a, (b, S)))
1481 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.
1484 Let's try composing `stack` and `uncons`. We want this result:
1486 stack∘uncons (... a -- ... a a [...])
1488 The stack effects are:
1492 uncons = ((a, Z), S) -- (Z, (a, S))
1496 S -- (S, S) ∘ ((a, Z), S) -- (Z, (a, S ))
1498 (a, Z) -- ∘ -- (Z, (a, (a, Z)))
1502 stack∘uncons == (a, Z) -- (Z, (a, (a, Z)))
1506 ### `stack∘uncons∘uncons`
1507 Let's try `stack∘uncons∘uncons`:
1509 (a, S ) -- (S, (a, (a, S ))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1513 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), S` ) -- (Z, (b, S` ))
1515 w/ { S`: (a, (a, (b, Z))) }
1517 (a, (b, Z)) -- ((b, Z), (a, (a, (b, Z)))) ∘ ((b, Z), (a, (a, (b, Z)))) -- (Z, (b, (a, (a, (b, Z)))))
1519 (a, (b, Z)) -- (Z, (b, (a, (a, (b, Z)))))
1523 #### `compose()` version 2
1524 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.)
1529 (f_in, f_out), (g_in, g_out) = f, g
1530 s = unify(g_in, f_out)
1531 if s == False: # s can also be the empty dict, which is ok.
1532 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
1533 return update(s, (f_in, g_out))
1536 I don't want to rewrite all the defs myself, so I'll write a little conversion function instead. This is programmer's laziness.
1540 def sequence_to_stack(seq, stack=StackJoyType(23)):
1541 for item in seq: stack = item, stack
1545 name: (sequence_to_stack(i), sequence_to_stack(o))
1546 for name, (i, o) in DEFS.iteritems()
1548 NEW_DEFS['stack'] = S[0], (S[0], S[0])
1549 NEW_DEFS['swaack'] = (S[1], S[0]), (S[0], S[1])
1550 globals().update(NEW_DEFS)
1561 ((a1, s1), (s1, (a1, (a1, s1))))
1567 reduce(C, (stack, uncons, uncons))
1573 ((a1, (a2, s1)), (s1, (a2, (a1, (a1, (a2, s1))))))
1577 The display function should be changed too.
1579 ### `doc_from_stack_effect()` version 2
1580 Clunky junk, but it will suffice for now.
1584 def doc_from_stack_effect(inputs, outputs):
1585 switch = [False] # Do we need to display the '...' for the rest of the main stack?
1586 i, o = _f(inputs, switch), _f(outputs, switch)
1590 return '(%s--%s)' % (
1591 ' '.join(reversed([''] + i)),
1592 ' '.join(reversed(o + [''])),
1596 def _f(term, switch):
1598 while term and isinstance(term, tuple):
1601 assert isinstance(term, StackJoyType), repr(term)
1602 a = [_to_str(i, term, switch) for i in a]
1606 def _to_str(term, stack, switch):
1607 if not isinstance(term, tuple):
1612 '[.%i.]' % term.number
1613 if isinstance(term, StackJoyType)
1618 while term and isinstance(term, tuple):
1620 a.append(_to_str(item, stack, switch))
1621 assert isinstance(term, StackJoyType), repr(term)
1626 end = '.%i.' % term.number
1628 return '[%s]' % ' '.join(a)
1633 for name, stack_effect_comment in sorted(NEW_DEFS.items()):
1634 print name, '=', doc_from_stack_effect(*stack_effect_comment)
1637 ccons = (a1 a2 [.1.] -- [a1 a2 .1.])
1638 cons = (a1 [.1.] -- [a1 .1.])
1639 divmod_ = (n2 n1 -- n4 n3)
1641 dupd = (a2 a1 -- a2 a2 a1)
1642 first = ([a1 .1.] -- a1)
1644 over = (a2 a1 -- a2 a1 a2)
1645 pm = (n2 n1 -- n4 n3)
1647 popd = (a2 a1 -- a1)
1648 popdd = (a3 a2 a1 -- a2 a1)
1651 rest = ([a1 .1.] -- [.1.])
1652 rolldown = (a1 a2 a3 -- a2 a3 a1)
1653 rollup = (a1 a2 a3 -- a3 a1 a2)
1654 rrest = ([a1 a2 .1.] -- [.1.])
1655 second = ([a1 a2 .1.] -- a2)
1657 stack = (... -- ... [...])
1659 swaack = ([.1.] -- [.0.])
1660 swap = (a1 a2 -- a2 a1)
1661 swons = ([.1.] a1 -- [a1 .1.])
1662 third = ([a1 a2 a3 .1.] -- a3)
1663 tuck = (a2 a1 -- a1 a2 a1)
1664 uncons = ([a1 .1.] -- a1 [.1.])
1669 print ; print doc_from_stack_effect(*stack)
1670 print ; print doc_from_stack_effect(*C(stack, uncons))
1671 print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, uncons)))
1672 print ; print doc_from_stack_effect(*reduce(C, (stack, uncons, cons)))
1678 (... a1 -- ... a1 a1 [...])
1680 (... a2 a1 -- ... a2 a1 a1 a2 [...])
1682 (... a1 -- ... a1 [a1 ...])
1687 print doc_from_stack_effect(*C(ccons, stack))
1690 (... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])
1703 ((s1, (a1, (a2, s2))), (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2)))
1707 #### `compile_()` version 3
1708 This makes the `compile_()` function pretty simple as the stack effect comments are now already in the form needed for the Python code:
1712 def compile_(name, f, doc=None):
1715 doc = doc_from_stack_effect(i, o)
1716 return '''def %s(stack):
1719 return %s''' % (name, doc, i, o)
1724 print compile_('Q', Q)
1728 """(... a2 a1 [.1.] -- ... [a2 a1 .1.] [[a2 a1 .1.] ...])"""
1729 (s1, (a1, (a2, s2))) = stack
1730 return (((a2, (a1, s1)), s2), ((a2, (a1, s1)), s2))
1735 unstack = (S[1], S[0]), S[1]
1736 enstacken = S[0], (S[0], S[1])
1741 print doc_from_stack_effect(*unstack)
1749 print doc_from_stack_effect(*enstacken)
1757 print doc_from_stack_effect(*C(cons, unstack))
1765 print doc_from_stack_effect(*C(cons, enstacken))
1768 (a1 [.1.] -- [[a1 .1.] .2.])
1779 ((s1, (a1, s2)), (a1, s1))
1783 ## Part VI: Multiple Stack Effects
1788 class IntJoyType(NumberJoyType): prefix = 'i'
1791 F = map(FloatJoyType, _R)
1792 I = map(IntJoyType, _R)
1798 ((I[2], (I[1], S[0])), (I[3], S[0])),
1799 ((F[2], (I[1], S[0])), (F[3], S[0])),
1800 ((I[2], (F[1], S[0])), (F[3], S[0])),
1801 ((F[2], (F[1], S[0])), (F[3], S[0])),
1808 print doc_from_stack_effect(*f)
1824 print doc_from_stack_effect(*dup), doc_from_stack_effect(*f), doc_from_stack_effect(*e)
1827 (a1 -- a1 a1) (i1 i2 -- i3) (i1 -- i2)
1828 (a1 -- a1 a1) (f1 f2 -- f3) (f1 -- f2)
1833 from itertools import product
1836 def meta_compose(F, G):
1837 for f, g in product(F, G):
1845 return sorted(set(meta_compose(F, G)))
1850 for f in MC([dup], [mul]):
1851 print doc_from_stack_effect(*f)
1859 for f in MC([dup], muls):
1860 print doc_from_stack_effect(*f)
1867 ### Representing an Unbounded Sequence of Types
1869 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:
1873 The `A*` works by splitting the universe into two alternate histories:
1877 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.
1879 Consider unifying two stacks (the lowercase letters are any type variables of the kinds we have defined so far):
1881 [a A* b .0.] U [c d .1.]
1883 [ A* b .0.] U [ d .1.]
1885 Now we have to split universes to unify `A*`. In the first universe it disappears:
1891 While in the second it spawns an `A`, which we will label `e`:
1893 [e A* b .0.] U [d .1.]
1895 [ A* b .0.] U [ .1.]
1897 [ A* b .0.] U [ A* b .0.]
1899 Giving us two unifiers:
1901 {c: a, d: b, .1.: .0.}
1902 {c: a, d: e, .1.: A* b .0.}
1906 class KleeneStar(object):
1910 def __init__(self, number):
1911 self.number = number
1913 self.prefix = repr(self)
1916 return '%s%i*' % (self.kind.prefix, self.number)
1920 return self.kind(10000 * self.number + self.count)
1922 def __eq__(self, other):
1924 isinstance(other, self.__class__)
1925 and other.number == self.number
1928 def __ge__(self, other):
1929 return self.kind >= other.kind
1931 def __add__(self, other):
1932 return self.__class__(self.number + other)
1936 return hash(repr(self))
1938 class AnyStarJoyType(KleeneStar): kind = AnyJoyType
1939 class NumberStarJoyType(KleeneStar): kind = NumberJoyType
1940 #class FloatStarJoyType(KleeneStar): kind = FloatJoyType
1941 #class IntStarJoyType(KleeneStar): kind = IntJoyType
1942 class StackStarJoyType(KleeneStar): kind = StackJoyType
1945 As = map(AnyStarJoyType, _R)
1946 Ns = map(NumberStarJoyType, _R)
1947 Ss = map(StackStarJoyType, _R)
1950 #### `unify()` version 4
1951 Can now return multiple results...
1955 def unify(u, v, s=None):
1965 if isinstance(u, AnyJoyType) and isinstance(v, AnyJoyType):
1972 raise TypeError('Cannot unify %r and %r.' % (u, v))
1974 if isinstance(u, tuple) and isinstance(v, tuple):
1975 if len(u) != len(v) != 2:
1976 raise TypeError(repr((u, v)))
1979 if isinstance(a, KleeneStar):
1980 # Two universes, in one the Kleene star disappears and unification
1981 # continues without it...
1984 # In the other it spawns a new variable.
1985 s1 = unify(u, (a.another(), v))
1993 if isinstance(a, KleeneStar):
1995 s1 = unify(v, (a.another(), u))
2001 ses = unify(u[0], v[0], s)
2004 results += unify(u[1], v[1], sn)
2007 if isinstance(v, tuple):
2009 raise TypeError('Cannot unify %r and %r.' % (u, v))
2013 if isinstance(u, tuple):
2015 raise TypeError('Cannot unify %r and %r.' % (v, u))
2023 return thing.__class__ in {AnyJoyType, StackJoyType}
2054 for result in unify(b, a):
2055 print result, '->', update(result, a), update(result, b)
2058 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2059 {a1: a10001, s2: (a1*, s1)} -> (a1*, s1) (a10001, (a1*, s1))
2064 for result in unify(a, b):
2065 print result, '->', update(result, a), update(result, b)
2068 {s1: (a1, s2)} -> (a1*, (a1, s2)) (a1, s2)
2069 {a1: a10002, s2: (a1*, s1)} -> (a1*, s1) (a10002, (a1*, s1))
2073 (a1*, s1) [a1*] (a1, s2) [a1]
2075 (a1*, (a1, s2)) [a1* a1] (a1, s2) [a1]
2077 (a1*, s1) [a1*] (a2, (a1*, s1)) [a2 a1*]
2081 sum_ = ((Ns[1], S[1]), S[0]), (N[0], S[0])
2083 print doc_from_stack_effect(*sum_)
2091 f = (N[1], (N[2], (N[3], S[1]))), S[0]
2093 print doc_from_stack_effect(S[0], f)
2101 for result in unify(sum_[0], f):
2102 print result, '->', update(result, sum_[1])
2105 {s1: (n1, (n2, (n3, s1)))} -> (n0, s0)
2106 {n1: n10001, s1: (n2, (n3, s1))} -> (n0, s0)
2107 {n1: n10001, s1: (n3, s1), n2: n10002} -> (n0, s0)
2108 {n1: n10001, s1: (n1*, s1), n3: n10003, n2: n10002} -> (n0, s0)
2111 #### `compose()` version 3
2112 This function has to be modified to yield multiple results.
2117 (f_in, f_out), (g_in, g_out) = f, g
2118 s = unify(g_in, f_out)
2120 raise TypeError('Cannot unify %r and %r.' % (f_out, g_in))
2122 yield update(result, (f_in, g_out))
2128 def meta_compose(F, G):
2129 for f, g in product(F, G):
2131 for result in C(f, g):
2138 f, g = relabel(f, g)
2139 for fg in compose(f, g):
2145 for f in MC([dup], muls):
2146 print doc_from_stack_effect(*f)
2157 for f in MC([dup], [sum_]):
2158 print doc_from_stack_effect(*f)
2161 ([n1* .1.] -- [n1* .1.] n1)
2168 for f in MC([cons], [sum_]):
2169 print doc_from_stack_effect(*f)
2173 (n1 [n1* .1.] -- n2)
2178 sum_ = (((N[1], (Ns[1], S[1])), S[0]), (N[0], S[0]))
2179 print doc_from_stack_effect(*cons),
2180 print doc_from_stack_effect(*sum_),
2182 for f in MC([cons], [sum_]):
2183 print doc_from_stack_effect(*f)
2186 (a1 [.1.] -- [a1 .1.]) ([n1 n1* .1.] -- n0) (n1 [n1* .1.] -- n2)
2191 a = (A[4], (As[1], (A[3], S[1])))
2198 (a4, (a1*, (a3, s1)))
2204 b = (A[1], (A[2], S[2]))
2217 for result in unify(b, a):
2221 {a1: a4, s2: s1, a2: a3}
2222 {a1: a4, s2: (a1*, (a3, s1)), a2: a10003}
2227 for result in unify(a, b):
2231 {s2: s1, a2: a3, a4: a1}
2232 {s2: (a1*, (a3, s1)), a2: a10004, a4: a1}
2235 ## Part VII: Typing Combinators
2237 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:
2239 i (... [.1.] -- ... .1.)
2243 i (... [A* .1.] -- ... A*)
2245 Consider the type of:
2249 Obviously it would be:
2251 (a1 [..1] a2 -- [a1 ..1] a2)
2253 `dip` itself could have:
2255 (a1 [..1] -- ... then what?
2258 Without any information about the contents of the quote we can't say much about the result.
2260 ### Hybrid Inferencer/Interpreter
2261 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.
2263 #### Joy Types for Functions
2264 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.
2268 class FunctionJoyType(AnyJoyType):
2270 def __init__(self, name, sec, number):
2272 self.stack_effects = sec
2273 self.number = number
2275 def __add__(self, other):
2283 #### Specialized for Simple Functions and Combinators
2284 For non-combinator functions the stack effects list contains stack effect comments (represented by pairs of cons-lists as described above.)
2288 class SymbolJoyType(FunctionJoyType):
2292 For combinators the list contains Python functions.
2296 class CombinatorJoyType(FunctionJoyType):
2300 def __init__(self, name, sec, number, expect=None):
2301 super(CombinatorJoyType, self).__init__(name, sec, number)
2302 self.expect = expect
2304 def enter_guard(self, f):
2305 if self.expect is None:
2307 g = self.expect, self.expect
2308 new_f = list(compose(f, g, ()))
2309 assert len(new_f) == 1, repr(new_f)
2313 For simple combinators that have only one effect (like ``dip``) you only need one function and it can be the combinator itself.
2319 dip = CombinatorJoyType('dip', [joy.library.dip], 23)
2322 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.
2326 def branch_true(stack, expression, dictionary):
2327 (then, (else_, (flag, stack))) = stack
2328 return stack, concat(then, expression), dictionary
2330 def branch_false(stack, expression, dictionary):
2331 (then, (else_, (flag, stack))) = stack
2332 return stack, concat(else_, expression), dictionary
2334 branch = CombinatorJoyType('branch', [branch_true, branch_false], 100)
2337 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.
2340 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.
2342 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.
2346 ID = S[0], S[0] # Identity function.
2349 def infer(*expression):
2350 return sorted(set(_infer(list_to_stack(expression))))
2353 def _infer(e, F=ID):
2360 if isinstance(n, SymbolJoyType):
2361 eFG = meta_compose([F], n.stack_effects, e)
2362 res = flatten(_infer(e, Fn) for e, Fn in eFG)
2364 elif isinstance(n, CombinatorJoyType):
2365 fi, fo = n.enter_guard(F)
2366 res = flatten(_interpret(f, fi, fo, e) for f in n.stack_effects)
2368 elif isinstance(n, Symbol):
2369 assert n not in FUNCTIONS, repr(n)
2370 func = joy.library._dictionary[n]
2371 res = _interpret(func, F[0], F[1], e)
2375 res = _infer(e, (fi, (n, fo)))
2380 def _interpret(f, fi, fo, e):
2381 new_fo, ee, _ = f(fo, e, {})
2382 ee = update(FUNCTIONS, ee) # Fix Symbols.
2384 return _infer(ee, new_F)
2390 len(inspect_stack()),
2391 doc_from_stack_effect(*F),
2392 expression_to_string(e),
2396 #### Work in Progress
2397 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 "polytypes" 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 :
2401 1/0 # (Don't try to run this cell! It's not going to work. This is "read only" code heh..)
2403 logging.basicConfig(format='%(message)s', stream=sys.stdout, level=logging.INFO)
2405 globals().update(FUNCTIONS)
2407 h = infer((pred, s2), (mul, s3), (div, s4), (nullary, (bool, s5)), dipd, branch)
2412 print doc_from_stack_effect(fi, fo)
2415 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.)
2417 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.
2419 7 (--) ∘ [pred] [mul] [div] [nullary bool] dipd branch
2420 8 (-- [pred ...2]) ∘ [mul] [div] [nullary bool] dipd branch
2421 9 (-- [pred ...2] [mul ...3]) ∘ [div] [nullary bool] dipd branch
2422 10 (-- [pred ...2] [mul ...3] [div ...4]) ∘ [nullary bool] dipd branch
2423 11 (-- [pred ...2] [mul ...3] [div ...4] [nullary bool ...5]) ∘ dipd branch
2424 15 (-- [pred ...5]) ∘ nullary bool [mul] [div] branch
2425 19 (-- [pred ...2]) ∘ [stack] dinfrirst bool [mul] [div] branch
2426 20 (-- [pred ...2] [stack ]) ∘ dinfrirst bool [mul] [div] branch
2427 22 (-- [pred ...2] [stack ]) ∘ dip infra first bool [mul] [div] branch
2428 26 (--) ∘ stack [pred] infra first bool [mul] [div] branch
2429 29 (... -- ... [...]) ∘ [pred] infra first bool [mul] [div] branch
2430 30 (... -- ... [...] [pred ...1]) ∘ infra first bool [mul] [div] branch
2431 34 (--) ∘ pred s1 swaack first bool [mul] [div] branch
2432 37 (n1 -- n2) ∘ [n1] swaack first bool [mul] [div] branch
2433 38 (... n1 -- ... n2 [n1 ...]) ∘ swaack first bool [mul] [div] branch
2434 41 (... n1 -- ... n1 [n2 ...]) ∘ first bool [mul] [div] branch
2435 44 (n1 -- n1 n2) ∘ bool [mul] [div] branch
2436 47 (n1 -- n1 b1) ∘ [mul] [div] branch
2437 48 (n1 -- n1 b1 [mul ...1]) ∘ [div] branch
2438 49 (n1 -- n1 b1 [mul ...1] [div ...2]) ∘ branch
2449 ----------------------------------------
2457 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
2459 Work remains to be done:
2461 - the rest of the library has to be covered
2462 - figure out how to deal with `loop` and `genrec`, etc..
2463 - extend the types to check values (see the appendix)
2464 - other kinds of "higher order" type variables, OR, AND, etc..
2465 - maybe rewrite in Prolog for great good?
2467 - don't permit composition of functions that don't compose
2468 - auto-compile compilable functions
2469 - Compiling more than just the Yin functions.
2470 - getting better visibility (than Python debugger.)
2471 - DOOOOCS!!!! Lots of docs!
2472 - docstrings all around
2473 - 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.
2475 ## Appendix: Joy in the Logical Paradigm
2477 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 `polytypes` module. But if you're interested in all that you should just use Prolog!
2479 Anyhow, type *checking* is a few easy steps away.
2483 def _ge(self, other):
2484 return (issubclass(other.__class__, self.__class__)
2485 or hasattr(self, 'accept')
2486 and isinstance(other, self.accept))
2488 AnyJoyType.__ge__ = _ge
2489 AnyJoyType.accept = tuple, int, float, long, str, unicode, bool, Symbol
2490 StackJoyType.accept = tuple