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/" />
9 <title>Type Checking — 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" />
21 <link rel="stylesheet" href="../_static/custom.css" type="text/css" />
24 <meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9" />
29 <div class="document">
30 <div class="documentwrapper">
31 <div class="bodywrapper">
34 <div class="body" role="main">
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>import logging, sys
41 format='%(message)s',
47 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>from joy.utils.types import (
48 doc_from_stack_effect,
57 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>D = FUNCTIONS.copy()
58 del D['product']
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>fi, fo = infer(pop, swap, rolldown, rrest, ccons)[0]
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]) ∘
75 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>print doc_from_stack_effect(fi, fo)
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>
81 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>from joy.parser import text_to_expression
82 from joy.utils.stack import stack_to_string
85 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>e = text_to_expression('0 1 2 [3 4]') # reverse order
86 print stack_to_string(e)
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>
92 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>u = unify(e, fi)[0]
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>
99 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>g = reify(u, (fi, fo))
100 print doc_from_stack_effect(*g)
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>
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>e = text_to_expression('[2 3]')
112 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>u = unify(e, fo)[0] # output side, not input side
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>
119 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>g = reify(u, (fi, fo))
120 print doc_from_stack_effect(*g)
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>
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>fi, fo = infer(dup, mul)[0]
132 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span>25 (--) ∘ dup mul
133 28 (a1 -- a1 a1) ∘ mul
138 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>e = text_to_expression('"two"')
139 print stack_to_string(e)
142 <div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="s1">'two'</span>
145 <div class="highlight-ipython2 notranslate"><div class="highlight"><pre><span></span>try:
147 except JoyTypeError, err:
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">'two'</span> <span class="ow">and</span> <span class="n">f1</span><span class="o">.</span>
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>
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="Zipper.html">Traversing Datastructures with Zippers</a></li>
193 <li class="toctree-l2"><a class="reference internal" href="Types.html">The Blissful Elegance of Typing Joy</a></li>
194 <li class="toctree-l2 current"><a class="current reference internal" href="#">Type Checking</a></li>
195 <li class="toctree-l2"><a class="reference internal" href="NoUpdates.html">No Updates</a></li>
196 <li class="toctree-l2"><a class="reference internal" href="Categorical.html">Categorical Programming</a></li>
197 <li class="toctree-l2"><a class="reference internal" href="The_Four_Operations.html">The Four Fundamental Operations of Definite Action</a></li>
198 <li class="toctree-l2"><a class="reference internal" href="Derivatives_of_Regular_Expressions.html">∂RE</a></li>
203 <div class="relations">
204 <h3>Related Topics</h3>
206 <li><a href="../index.html">Documentation overview</a><ul>
207 <li><a href="index.html">Essays about Programming in Joy</a><ul>
208 <li>Previous: <a href="Types.html" title="previous chapter">The Blissful Elegance of Typing Joy</a></li>
209 <li>Next: <a href="NoUpdates.html" title="next chapter">No Updates</a></li>
214 <div id="searchbox" style="display: none" role="search">
215 <h3 id="searchlabel">Quick search</h3>
216 <div class="searchformwrapper">
217 <form class="search" action="../search.html" method="get">
218 <input type="text" name="q" aria-labelledby="searchlabel" autocomplete="off" autocorrect="off" autocapitalize="off" spellcheck="false"/>
219 <input type="submit" value="Go" />
223 <script>$('#searchbox').show(0);</script>
234 <div class="clearer"></div>
236 <div class="footer" role="contentinfo">
237 <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">
238 <img alt="Creative Commons License" style="border-width:0" src="https://i.creativecommons.org/l/by-nc-sa/4.0/88x31.png" />
241 <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>.
242 Created using <a href="http://sphinx-doc.org/">Sphinx</a> 4.3.0.