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

   1
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
   3   "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   4
   5 <html xmlns="http://www.w3.org/1999/xhtml">
   6   <head>
   7     <meta http-equiv="X-UA-Compatible" content="IE=Edge" />
   8     <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
   9     <title>Type Checking &#8212; Thun 0.4.1 documentation</title>
  10     <link rel="stylesheet" href="../_static/alabaster.css" type="text/css" />
  11     <link rel="stylesheet" href="../_static/pygments.css" type="text/css" />
  12     <script type="text/javascript" src="../_static/documentation_options.js"></script>
  13     <script type="text/javascript" src="../_static/jquery.js"></script>
  14     <script type="text/javascript" src="../_static/underscore.js"></script>
  15     <script type="text/javascript" src="../_static/doctools.js"></script>
  16     <script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
  17     <link rel="index" title="Index" href="../genindex.html" />
  18     <link rel="search" title="Search" href="../search.html" />
  19     <link rel="next" title="No Updates" href="NoUpdates.html" />
  20     <link rel="prev" title="The Blissful Elegance of Typing Joy" href="Types.html" />
  21
  22   <link rel="stylesheet" href="../_static/custom.css" type="text/css" />
  23
  24
  25   <meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9" />
  26
  27   </head><body>
  28
  29
  30     <div class="document">
  31       <div class="documentwrapper">
  32         <div class="bodywrapper">
  33           <div class="body" role="main">
  34
  35   <div class="section" id="type-checking">
  36 <h1>Type Checking<a class="headerlink" href="#type-checking" title="Permalink to this headline">¶</a></h1>
  37 <div class="code ipython2 highlight-default 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>
  38
  39 <span class="n">logging</span><span class="o">.</span><span class="n">basicConfig</span><span class="p">(</span>
  40   <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>
  41   <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>
  42   <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>
  43   <span class="p">)</span>
  44 </pre></div>
  45 </div>
  46 <div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">joy.utils.types</span> <span class="k">import</span> <span class="p">(</span>
  47     <span class="n">doc_from_stack_effect</span><span class="p">,</span>
  48     <span class="n">infer</span><span class="p">,</span>
  49     <span class="n">reify</span><span class="p">,</span>
  50     <span class="n">unify</span><span class="p">,</span>
  51     <span class="n">FUNCTIONS</span><span class="p">,</span>
  52     <span class="n">JoyTypeError</span><span class="p">,</span>
  53 <span class="p">)</span>
  54 </pre></div>
  55 </div>
  56 <div class="code ipython2 highlight-default 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>
  57 <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>
  58 <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>
  59 </pre></div>
  60 </div>
  61 <div class="section" id="an-example">
  62 <h2>An Example<a class="headerlink" href="#an-example" title="Permalink to this headline">¶</a></h2>
  63 <div class="code ipython2 highlight-default 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>
  64 </pre></div>
  65 </div>
  66 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span>25 (--) ∘ pop swap rolldown rrest ccons
  67 28 (a1 --) ∘ swap rolldown rrest ccons
  68 31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons
  69 34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons
  70 37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons
  71 40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘
  72 </pre></div>
  73 </div>
  74 <div class="code ipython2 highlight-default 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>
  75 </pre></div>
  76 </div>
  77 <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>
  78 </pre></div>
  79 </div>
  80 <div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">joy.parser</span> <span class="k">import</span> <span class="n">text_to_expression</span>
  81 <span class="kn">from</span> <span class="nn">joy.utils.stack</span> <span class="k">import</span> <span class="n">stack_to_string</span>
  82 </pre></div>
  83 </div>
  84 <div class="code ipython2 highlight-default 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>
  85 <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>
  86 </pre></div>
  87 </div>
  88 <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>
  89 </pre></div>
  90 </div>
  91 <div class="code ipython2 highlight-default 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>
  92 <span class="n">u</span>
  93 </pre></div>
  94 </div>
  95 <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>
  96 </pre></div>
  97 </div>
  98 <div class="code ipython2 highlight-default 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>
  99 <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>
 100 </pre></div>
 101 </div>
 102 <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>
 103 </pre></div>
 104 </div>
 105 </div>
 106 <div class="section" id="unification-works-in-reverse">
 107 <h2>Unification Works “in Reverse”<a class="headerlink" href="#unification-works-in-reverse" title="Permalink to this headline">¶</a></h2>
 108 <div class="code ipython2 highlight-default 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>
 109 </pre></div>
 110 </div>
 111 <div class="code ipython2 highlight-default 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>
 112 <span class="n">u</span>
 113 </pre></div>
 114 </div>
 115 <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>
 116 </pre></div>
 117 </div>
 118 <div class="code ipython2 highlight-default 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>
 119 <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>
 120 </pre></div>
 121 </div>
 122 <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>
 123 </pre></div>
 124 </div>
 125 </div>
 126 <div class="section" id="failing-a-check">
 127 <h2>Failing a Check<a class="headerlink" href="#failing-a-check" title="Permalink to this headline">¶</a></h2>
 128 <div class="code ipython2 highlight-default 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>
 129 </pre></div>
 130 </div>
 131 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span>25 (--) ∘ dup mul
 132 28 (a1 -- a1 a1) ∘ mul
 133 31 (f1 -- f2) ∘
 134 31 (i1 -- i2) ∘
 135 </pre></div>
 136 </div>
 137 <div class="code ipython2 highlight-default 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>
 138 <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>
 139 </pre></div>
 140 </div>
 141 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="s1">&#39;two&#39;</span>
 142 </pre></div>
 143 </div>
 144 <div class="code ipython2 highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">try</span><span class="p">:</span>
 145     <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>
 146 <span class="k">except</span> <span class="n">JoyTypeError</span><span class="p">,</span> <span class="n">err</span><span class="p">:</span>
 147     <span class="nb">print</span> <span class="n">err</span>
 148 </pre></div>
 149 </div>
 150 <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>
 151 </pre></div>
 152 </div>
 153 </div>
 154 </div>
 155
 156
 157           </div>
 158         </div>
 159       </div>
 160       <div class="sphinxsidebar" role="navigation" aria-label="main navigation">
 161         <div class="sphinxsidebarwrapper">
 162   <h3><a href="../index.html">Table Of Contents</a></h3>
 163   <ul>
 164 <li><a class="reference internal" href="#">Type Checking</a><ul>
 165 <li><a class="reference internal" href="#an-example">An Example</a></li>
 166 <li><a class="reference internal" href="#unification-works-in-reverse">Unification Works “in Reverse”</a></li>
 167 <li><a class="reference internal" href="#failing-a-check">Failing a Check</a></li>
 168 </ul>
 169 </li>
 170 </ul>
 171 <div class="relations">
 172 <h3>Related Topics</h3>
 173 <ul>
 174   <li><a href="../index.html">Documentation overview</a><ul>
 175   <li><a href="index.html">Essays about Programming in Joy</a><ul>
 176       <li>Previous: <a href="Types.html" title="previous chapter">The Blissful Elegance of Typing Joy</a></li>
 177       <li>Next: <a href="NoUpdates.html" title="next chapter">No Updates</a></li>
 178   </ul></li>
 179   </ul></li>
 180 </ul>
 181 </div>
 182   <div role="note" aria-label="source link">
 183     <h3>This Page</h3>
 184     <ul class="this-page-menu">
 185       <li><a href="../_sources/notebooks/TypeChecking.rst.txt"
 186             rel="nofollow">Show Source</a></li>
 187     </ul>
 188    </div>
 189 <div id="searchbox" style="display: none" role="search">
 190   <h3>Quick search</h3>
 191     <div class="searchformwrapper">
 192     <form class="search" action="../search.html" method="get">
 193       <input type="text" name="q" />
 194       <input type="submit" value="Go" />
 195       <input type="hidden" name="check_keywords" value="yes" />
 196       <input type="hidden" name="area" value="default" />
 197     </form>
 198     </div>
 199 </div>
 200 <script type="text/javascript">$('#searchbox').show(0);</script>
 201         </div>
 202       </div>
 203       <div class="clearer"></div>
 204     </div>
 205     <div class="footer" role="contentinfo">
 206 <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">
 207 <img alt="Creative Commons License" style="border-width:0" src="https://i.creativecommons.org/l/by-nc-sa/4.0/88x31.png" />
 208 </a>
 209 <br />
 210 <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>.
 211       Created using <a href="http://sphinx-doc.org/">Sphinx</a> 1.7.3.
 212     </div>
 213
 214   </body>
 215 </html>