docs/sphinx_docs/_build/html/notebooks/TypeChecking.html

   1
   2 <!DOCTYPE html>
   3
   4 <html>
   5   <head>
   6     <meta charset="utf-8" />
   7     <meta name="viewport" content="width=device-width, initial-scale=1.0" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
   8
   9     <title>Type Checking &#8212; Thun 0.4.1 documentation</title>
  10     <link rel="stylesheet" type="text/css" href="../_static/pygments.css" />
  11     <link rel="stylesheet" type="text/css" href="../_static/alabaster.css" />
  12     <script data-url_root="../" id="documentation_options" src="../_static/documentation_options.js"></script>
  13     <script src="../_static/jquery.js"></script>
  14     <script src="../_static/underscore.js"></script>
  15     <script src="../_static/doctools.js"></script>
  16     <link rel="index" title="Index" href="../genindex.html" />
  17     <link rel="search" title="Search" href="../search.html" />
  18     <link rel="next" title="No Updates" href="NoUpdates.html" />
  19     <link rel="prev" title="The Blissful Elegance of Typing Joy" href="Types.html" />
  20
  21   <link rel="stylesheet" href="../_static/custom.css" type="text/css" />
  22
  23
  24   <meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9" />
  25
  26   </head><body>
  27
  28
  29     <div class="document">
  30       <div class="documentwrapper">
  31         <div class="bodywrapper">
  32
  33
  34           <div class="body" role="main">
  35
  36   <section id="type-checking">
  37 <h1>Type Checking<a class="headerlink" href="#type-checking" title="Permalink to this headline">¶</a></h1>
  38 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="kn">import</span> <span class="nn">logging</span><span class="o">,</span> <span class="nn">sys</span>
  39
  40 <span class="n">logging</span><span class="o">.</span><span class="n">basicConfig</span><span class="p">(</span>
  41   <span class="nb">format</span><span class="o">=</span><span class="s1">&#39;</span><span class="si">%(message)s</span><span class="s1">&#39;</span><span class="p">,</span>
  42   <span class="n">stream</span><span class="o">=</span><span class="n">sys</span><span class="o">.</span><span class="n">stdout</span><span class="p">,</span>
  43   <span class="n">level</span><span class="o">=</span><span class="n">logging</span><span class="o">.</span><span class="n">INFO</span><span class="p">,</span>
  44   <span class="p">)</span>
  45 </pre></div>
  46 </div>
  47 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">joy.utils.types</span> <span class="kn">import</span> <span class="p">(</span>
  48     <span class="n">doc_from_stack_effect</span><span class="p">,</span>
  49     <span class="n">infer</span><span class="p">,</span>
  50     <span class="n">reify</span><span class="p">,</span>
  51     <span class="n">unify</span><span class="p">,</span>
  52     <span class="n">FUNCTIONS</span><span class="p">,</span>
  53     <span class="n">JoyTypeError</span><span class="p">,</span>
  54 <span class="p">)</span>
  55 </pre></div>
  56 </div>
  57 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">D</span> <span class="o">=</span> <span class="n">FUNCTIONS</span><span class="o">.</span><span class="n">copy</span><span class="p">()</span>
  58 <span class="k">del</span> <span class="n">D</span><span class="p">[</span><span class="s1">&#39;product&#39;</span><span class="p">]</span>
  59 <span class="nb">globals</span><span class="p">()</span><span class="o">.</span><span class="n">update</span><span class="p">(</span><span class="n">D</span><span class="p">)</span>
  60 </pre></div>
  61 </div>
  62 <section id="an-example">
  63 <h2>An Example<a class="headerlink" href="#an-example" title="Permalink to this headline">¶</a></h2>
  64 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">fi</span><span class="p">,</span> <span class="n">fo</span> <span class="o">=</span> <span class="n">infer</span><span class="p">(</span><span class="n">pop</span><span class="p">,</span> <span class="n">swap</span><span class="p">,</span> <span class="n">rolldown</span><span class="p">,</span> <span class="n">rrest</span><span class="p">,</span> <span class="n">ccons</span><span class="p">)[</span><span class="mi">0</span><span class="p">]</span>
  65 </pre></div>
  66 </div>
  67 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span>25 (--) ∘ pop swap rolldown rrest ccons
  68 28 (a1 --) ∘ swap rolldown rrest ccons
  69 31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons
  70 34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons
  71 37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons
  72 40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘
  73 </pre></div>
  74 </div>
  75 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="n">fi</span><span class="p">,</span> <span class="n">fo</span><span class="p">)</span>
  76 </pre></div>
  77 </div>
  78 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">([</span><span class="n">a4</span> <span class="n">a5</span> <span class="o">...</span><span class="mi">1</span><span class="p">]</span> <span class="n">a3</span> <span class="n">a2</span> <span class="n">a1</span> <span class="o">--</span> <span class="p">[</span><span class="n">a2</span> <span class="n">a3</span> <span class="o">...</span><span class="mi">1</span><span class="p">])</span>
  79 </pre></div>
  80 </div>
  81 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">joy.parser</span> <span class="kn">import</span> <span class="n">text_to_expression</span>
  82 <span class="kn">from</span> <span class="nn">joy.utils.stack</span> <span class="kn">import</span> <span class="n">stack_to_string</span>
  83 </pre></div>
  84 </div>
  85 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">e</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;0 1 2 [3 4]&#39;</span><span class="p">)</span>  <span class="c1"># reverse order</span>
  86 <span class="nb">print</span> <span class="n">stack_to_string</span><span class="p">(</span><span class="n">e</span><span class="p">)</span>
  87 </pre></div>
  88 </div>
  89 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">[</span><span class="mi">3</span> <span class="mi">4</span><span class="p">]</span> <span class="mi">2</span> <span class="mi">1</span> <span class="mi">0</span>
  90 </pre></div>
  91 </div>
  92 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">u</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">e</span><span class="p">,</span> <span class="n">fi</span><span class="p">)[</span><span class="mi">0</span><span class="p">]</span>
  93 <span class="n">u</span>
  94 </pre></div>
  95 </div>
  96 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">{</span><span class="n">a1</span><span class="p">:</span> <span class="mi">0</span><span class="p">,</span> <span class="n">a2</span><span class="p">:</span> <span class="mi">1</span><span class="p">,</span> <span class="n">a3</span><span class="p">:</span> <span class="mi">2</span><span class="p">,</span> <span class="n">a4</span><span class="p">:</span> <span class="mi">3</span><span class="p">,</span> <span class="n">a5</span><span class="p">:</span> <span class="mi">4</span><span class="p">,</span> <span class="n">s2</span><span class="p">:</span> <span class="p">(),</span> <span class="n">s1</span><span class="p">:</span> <span class="p">()}</span>
  97 </pre></div>
  98 </div>
  99 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">g</span> <span class="o">=</span> <span class="n">reify</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="p">(</span><span class="n">fi</span><span class="p">,</span> <span class="n">fo</span><span class="p">))</span>
 100 <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">g</span><span class="p">)</span>
 101 </pre></div>
 102 </div>
 103 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">...</span> <span class="p">[</span><span class="mi">3</span> <span class="mi">4</span> <span class="p">]</span> <span class="mi">2</span> <span class="mi">1</span> <span class="mi">0</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="mi">1</span> <span class="mi">2</span> <span class="p">])</span>
 104 </pre></div>
 105 </div>
 106 </section>
 107 <section id="unification-works-in-reverse">
 108 <h2>Unification Works “in Reverse”<a class="headerlink" href="#unification-works-in-reverse" title="Permalink to this headline">¶</a></h2>
 109 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">e</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;[2 3]&#39;</span><span class="p">)</span>
 110 </pre></div>
 111 </div>
 112 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">u</span> <span class="o">=</span> <span class="n">unify</span><span class="p">(</span><span class="n">e</span><span class="p">,</span> <span class="n">fo</span><span class="p">)[</span><span class="mi">0</span><span class="p">]</span>  <span class="c1"># output side, not input side</span>
 113 <span class="n">u</span>
 114 </pre></div>
 115 </div>
 116 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">{</span><span class="n">a2</span><span class="p">:</span> <span class="mi">2</span><span class="p">,</span> <span class="n">a3</span><span class="p">:</span> <span class="mi">3</span><span class="p">,</span> <span class="n">s2</span><span class="p">:</span> <span class="p">(),</span> <span class="n">s1</span><span class="p">:</span> <span class="p">()}</span>
 117 </pre></div>
 118 </div>
 119 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">g</span> <span class="o">=</span> <span class="n">reify</span><span class="p">(</span><span class="n">u</span><span class="p">,</span> <span class="p">(</span><span class="n">fi</span><span class="p">,</span> <span class="n">fo</span><span class="p">))</span>
 120 <span class="nb">print</span> <span class="n">doc_from_stack_effect</span><span class="p">(</span><span class="o">*</span><span class="n">g</span><span class="p">)</span>
 121 </pre></div>
 122 </div>
 123 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="p">(</span><span class="o">...</span> <span class="p">[</span><span class="n">a4</span> <span class="n">a5</span> <span class="p">]</span> <span class="mi">3</span> <span class="mi">2</span> <span class="n">a1</span> <span class="o">--</span> <span class="o">...</span> <span class="p">[</span><span class="mi">2</span> <span class="mi">3</span> <span class="p">])</span>
 124 </pre></div>
 125 </div>
 126 </section>
 127 <section id="failing-a-check">
 128 <h2>Failing a Check<a class="headerlink" href="#failing-a-check" title="Permalink to this headline">¶</a></h2>
 129 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">fi</span><span class="p">,</span> <span class="n">fo</span> <span class="o">=</span> <span class="n">infer</span><span class="p">(</span><span class="n">dup</span><span class="p">,</span> <span class="n">mul</span><span class="p">)[</span><span class="mi">0</span><span class="p">]</span>
 130 </pre></div>
 131 </div>
 132 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span>25 (--) ∘ dup mul
 133 28 (a1 -- a1 a1) ∘ mul
 134 31 (f1 -- f2) ∘
 135 31 (i1 -- i2) ∘
 136 </pre></div>
 137 </div>
 138 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="n">e</span> <span class="o">=</span> <span class="n">text_to_expression</span><span class="p">(</span><span class="s1">&#39;&quot;two&quot;&#39;</span><span class="p">)</span>
 139 <span class="nb">print</span> <span class="n">stack_to_string</span><span class="p">(</span><span class="n">e</span><span class="p">)</span>
 140 </pre></div>
 141 </div>
 142 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="s1">&#39;two&#39;</span>
 143 </pre></div>
 144 </div>
 145 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span><span class="k">try</span><span class="p">:</span>
 146     <span class="n">unify</span><span class="p">(</span><span class="n">e</span><span class="p">,</span> <span class="n">fi</span><span class="p">)</span>
 147 <span class="k">except</span> <span class="n">JoyTypeError</span><span class="p">,</span> <span class="n">err</span><span class="p">:</span>
 148     <span class="nb">print</span> <span class="n">err</span>
 149 </pre></div>
 150 </div>
 151 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">Cannot</span> <span class="n">unify</span> <span class="s1">&#39;two&#39;</span> <span class="ow">and</span> <span class="n">f1</span><span class="o">.</span>
 152 </pre></div>
 153 </div>
 154 </section>
 155 </section>
 156
 157
 158           </div>
 159
 160         </div>
 161       </div>
 162       <div class="sphinxsidebar" role="navigation" aria-label="main navigation">
 163         <div class="sphinxsidebarwrapper">
 164 <h1 class="logo"><a href="../index.html">Thun</a></h1>
 165
 166
 167
 168
 169
 170
 171
 172
 173 <h3>Navigation</h3>
 174 <ul class="current">
 175 <li class="toctree-l1"><a class="reference internal" href="Intro.html">Thun: Joy in Python</a></li>
 176 <li class="toctree-l1"><a class="reference internal" href="../joy.html">Joy Interpreter</a></li>
 177 <li class="toctree-l1"><a class="reference internal" href="../stack.html">Stack or Quote or Sequence or List…</a></li>
 178 <li class="toctree-l1"><a class="reference internal" href="../parser.html">Parsing Text into Joy Expressions</a></li>
 179 <li class="toctree-l1"><a class="reference internal" href="../pretty.html">Tracing Joy Execution</a></li>
 180 <li class="toctree-l1"><a class="reference internal" href="../library.html">Function Reference</a></li>
 181 <li class="toctree-l1"><a class="reference internal" href="../lib.html">Functions Grouped by, er, Function with Examples</a></li>
 182 <li class="toctree-l1"><a class="reference internal" href="../types.html">Type Inference of Joy Expressions</a></li>
 183 <li class="toctree-l1 current"><a class="reference internal" href="index.html">Essays about Programming in Joy</a><ul class="current">
 184 <li class="toctree-l2"><a class="reference internal" href="Developing.html">Developing a Program in Joy</a></li>
 185 <li class="toctree-l2"><a class="reference internal" href="Quadratic.html">Quadratic formula</a></li>
 186 <li class="toctree-l2"><a class="reference internal" href="Replacing.html">Replacing Functions in the Dictionary</a></li>
 187 <li class="toctree-l2"><a class="reference internal" href="Recursion_Combinators.html">Recursion Combinators</a></li>
 188 <li class="toctree-l2"><a class="reference internal" href="Ordered_Binary_Trees.html">Treating Trees I: Ordered Binary Trees</a></li>
 189 <li class="toctree-l2"><a class="reference internal" href="Treestep.html">Treating Trees II: <code class="docutils literal notranslate"><span class="pre">treestep</span></code></a></li>
 190 <li class="toctree-l2"><a class="reference internal" href="Generator_Programs.html">Using <code class="docutils literal notranslate"><span class="pre">x</span></code> to Generate Values</a></li>
 191 <li class="toctree-l2"><a class="reference internal" href="Newton-Raphson.html">Newton’s method</a></li>
 192 <li class="toctree-l2"><a class="reference internal" href="Square_Spiral.html">Square Spiral Example Joy Code</a></li>
 193 <li class="toctree-l2"><a class="reference internal" href="Zipper.html">Traversing Datastructures with Zippers</a></li>
 194 <li class="toctree-l2"><a class="reference internal" href="Types.html">The Blissful Elegance of Typing Joy</a></li>
 195 <li class="toctree-l2 current"><a class="current reference internal" href="#">Type Checking</a></li>
 196 <li class="toctree-l2"><a class="reference internal" href="NoUpdates.html">No Updates</a></li>
 197 <li class="toctree-l2"><a class="reference internal" href="Categorical.html">Categorical Programming</a></li>
 198 <li class="toctree-l2"><a class="reference internal" href="The_Four_Operations.html">The Four Fundamental Operations of Definite Action</a></li>
 199 <li class="toctree-l2"><a class="reference internal" href="Derivatives_of_Regular_Expressions.html">∂RE</a></li>
 200 </ul>
 201 </li>
 202 </ul>
 203
 204 <div class="relations">
 205 <h3>Related Topics</h3>
 206 <ul>
 207   <li><a href="../index.html">Documentation overview</a><ul>
 208   <li><a href="index.html">Essays about Programming in Joy</a><ul>
 209       <li>Previous: <a href="Types.html" title="previous chapter">The Blissful Elegance of Typing Joy</a></li>
 210       <li>Next: <a href="NoUpdates.html" title="next chapter">No Updates</a></li>
 211   </ul></li>
 212   </ul></li>
 213 </ul>
 214 </div>
 215 <div id="searchbox" style="display: none" role="search">
 216   <h3 id="searchlabel">Quick search</h3>
 217     <div class="searchformwrapper">
 218     <form class="search" action="../search.html" method="get">
 219       <input type="text" name="q" aria-labelledby="searchlabel" autocomplete="off" autocorrect="off" autocapitalize="off" spellcheck="false"/>
 220       <input type="submit" value="Go" />
 221     </form>
 222     </div>
 223 </div>
 224 <script>$('#searchbox').show(0);</script>
 225
 226
 227
 228
 229
 230
 231
 232
 233         </div>
 234       </div>
 235       <div class="clearer"></div>
 236     </div>
 237     <div class="footer" role="contentinfo">
 238 <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">
 239 <img alt="Creative Commons License" style="border-width:0" src="https://i.creativecommons.org/l/by-nc-sa/4.0/88x31.png" />
 240 </a>
 241 <br />
 242 <span xmlns:dct="http://purl.org/dc/terms/" property="dct:title">Thun Documentation</span> by <a xmlns:cc="http://creativecommons.org/ns#" href="https://joypy.osdn.io/" property="cc:attributionName" rel="cc:attributionURL">Simon Forman</a> is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License</a>.<br />Based on a work at <a xmlns:dct="http://purl.org/dc/terms/" href="https://osdn.net/projects/joypy/" rel="dct:source">https://osdn.net/projects/joypy/</a>.
 243       Created using <a href="http://sphinx-doc.org/">Sphinx</a> 4.3.0.
 244     </div>
 245
 246   </body>
 247 </html>