docs/TypeChecking.md

   1 # Type Checking
   2
   3
   4 ```python
   5 import logging, sys
   6
   7 logging.basicConfig(
   8   format='%(message)s',
   9   stream=sys.stdout,
  10   level=logging.INFO,
  11   )
  12 ```
  13
  14
  15 ```python
  16 from joy.utils.types import (
  17     doc_from_stack_effect,
  18     infer,
  19     reify,
  20     unify,
  21     FUNCTIONS,
  22     JoyTypeError,
  23 )
  24 ```
  25
  26
  27 ```python
  28 D = FUNCTIONS.copy()
  29 del D['product']
  30 globals().update(D)
  31 ```
  32
  33 ## An Example
  34
  35
  36 ```python
  37 fi, fo = infer(pop, swap, rolldown, rrest, ccons)[0]
  38 ```
  39
  40      25 (--) ∘ pop swap rolldown rrest ccons
  41      28 (a1 --) ∘ swap rolldown rrest ccons
  42      31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons
  43      34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons
  44      37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons
  45      40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘
  46
  47
  48
  49 ```python
  50 print doc_from_stack_effect(fi, fo)
  51 ```
  52
  53     ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1])
  54
  55
  56
  57 ```python
  58 from joy.parser import text_to_expression
  59 from joy.utils.stack import stack_to_string
  60
  61 ```
  62
  63
  64 ```python
  65 e = text_to_expression('0 1 2 [3 4]')  # reverse order
  66 print stack_to_string(e)
  67 ```
  68
  69     [3 4] 2 1 0
  70
  71
  72
  73 ```python
  74 u = unify(e, fi)[0]
  75 u
  76 ```
  77
  78
  79
  80
  81     {a1: 0, a2: 1, a3: 2, a4: 3, a5: 4, s2: (), s1: ()}
  82
  83
  84
  85
  86 ```python
  87 g = reify(u, (fi, fo))
  88 print doc_from_stack_effect(*g)
  89 ```
  90
  91     (... [3 4 ] 2 1 0 -- ... [1 2 ])
  92
  93
  94 ##  Unification Works "in Reverse"
  95
  96
  97 ```python
  98 e = text_to_expression('[2 3]')
  99 ```
 100
 101
 102 ```python
 103 u = unify(e, fo)[0]  # output side, not input side
 104 u
 105 ```
 106
 107
 108
 109
 110     {a2: 2, a3: 3, s2: (), s1: ()}
 111
 112
 113
 114
 115 ```python
 116 g = reify(u, (fi, fo))
 117 print doc_from_stack_effect(*g)
 118 ```
 119
 120     (... [a4 a5 ] 3 2 a1 -- ... [2 3 ])
 121
 122
 123 ## Failing a Check
 124
 125
 126 ```python
 127 fi, fo = infer(dup, mul)[0]
 128 ```
 129
 130      25 (--) ∘ dup mul
 131      28 (a1 -- a1 a1) ∘ mul
 132      31 (f1 -- f2) ∘
 133      31 (i1 -- i2) ∘
 134
 135
 136
 137 ```python
 138 e = text_to_expression('"two"')
 139 print stack_to_string(e)
 140 ```
 141
 142     'two'
 143
 144
 145
 146 ```python
 147 try:
 148     unify(e, fi)
 149 except JoyTypeError, err:
 150     print err
 151 ```
 152
 153     Cannot unify 'two' and f1.
 154