Thun/docs/TypeChecking.ipynb

Type Checking

In [1]:

import logging, sys

logging.basicConfig(
  format='%(message)s',
  stream=sys.stdout,
  level=logging.INFO,
  )

In [2]:

from joy.utils.polytypes import (
    doc_from_stack_effect, 
    infer,
    reify,
    unify,
    FUNCTIONS,
    JoyTypeError,
)

In [3]:

D = FUNCTIONS.copy()
del D['product']
globals().update(D)

An Example

In [4]:

fi, fo = infer(pop, swap, rolldown, rrest, ccons)[0]

 25 (--) ∘ pop swap rolldown rrest ccons
 28 (a1 --) ∘ swap rolldown rrest ccons
 31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons
 34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons
 37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons
 40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘ 

In [5]:

print doc_from_stack_effect(fi, fo)

([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1])

In [6]:

from joy.parser import text_to_expression
from joy.utils.stack import stack_to_string

In [7]:

e = text_to_expression('0 1 2 [3 4]')  # reverse order
print stack_to_string(e)

[3 4] 2 1 0

In [8]:

u = unify(e, fi)[0]
u

Out [8]:

{a1: 0, a2: 1, a3: 2, a4: 3, a5: 4, s2: (), s1: ()}

In [9]:

g = reify(u, (fi, fo))
print doc_from_stack_effect(*g)

(... [3 4 ] 2 1 0 -- ... [1 2 ])

Unification Works "in Reverse"

In [10]:

e = text_to_expression('[2 3]')

In [11]:

u = unify(e, fo)[0]  # output side, not input side
u

Out [11]:

{a2: 2, a3: 3, s2: (), s1: ()}

In [12]:

g = reify(u, (fi, fo))
print doc_from_stack_effect(*g)

(... [a4 a5 ] 3 2 a1 -- ... [2 3 ])

Failing a Check

In [13]:

fi, fo = infer(dup, mul)[0]

 25 (--) ∘ dup mul
 28 (a1 -- a1 a1) ∘ mul
 31 (f1 -- f2) ∘ 
 31 (i1 -- i2) ∘ 

In [14]:

e = text_to_expression('"two"')
print stack_to_string(e)

'two'

In [15]:

try:
    unify(e, fi)
except JoyTypeError, err:
    print err

Cannot unify 'two' and f1.