docs/TypeChecking.rst

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