docs/sphinx_docs/notebooks/TypeChecking.rst

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