<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>Anything that's tail recursive could be converted to a while loop
      and then clocked, no? You could for instance compile<br>
      <br>
      <tt>fact :: Int -> Int</tt></p>
    <p><tt>fact 0 = 1</tt></p>
    <p><tt>fact n = n * fact (n - 1)<br>
        <br>
      </tt>to hardware even if it would not be a good idea.<br>
    </p>
    <div class="moz-cite-prefix">On 10/21/18 4:16 AM, William Yager
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAG8oi1PwFqwpzBpt=ht7KyR5HWV4VZKO7i14ZFLHxj=3TD-N+w@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div dir="ltr"><br>
          <br>
          <div class="gmail_quote">
            <div dir="ltr">On Sun, Oct 21, 2018 at 3:04 PM Joachim
              Durchholz <<a href="mailto:jo@durchholz.org"
                moz-do-not-send="true">jo@durchholz.org</a>> wrote:<br>
            </div>
            <blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><br>
              Is that subset described somewhere?<br>
              <br>
            </blockquote>
            <div><br>
            </div>
            <div>So there are two possible answers to this:</div>
            <div><br>
            </div>
            <div>1. The subset that Clash supports is a bit complicated
              and increases from time to time, depending mostly on the
              internal details of the clash compiler</div>
            <div><br>
            </div>
            <div>2. The subset that Clash *could* support with (roughly)
              its current approach, which I think I can answer a bit
              better: </div>
            <div><br>
            </div>
            <div>I gave a brief hand-wavy description earlier -
              "non-monomorphically-recursive"</div>
            <div><br>
            </div>
            <div>That is, any recursion has to be unrolled at the
              hardware level, and monomorphically (i.e. normally)
              recursive functions cannot (generally) stop being unrolled
              after a finite number of iterations. Sure, you can
              sometimes use fancy tricks (an SMT solver or something) to
              prove termination, but these come with a number of other
              challenges. For hardware you want a small, concrete number
              of recursions, which leads to lots of complications (e.g.
              need for dependent types to relate input values and
              recursion depth).</div>
            <div><br>
            </div>
            <div>Much simpler is to simply disallow monomorphic
              recursion, and then you shift the work of proving finite
              recursion depth to the type level. </div>
            <div><br>
            </div>
            <div>There's then a simple (constructive) rule for proving
              termination and calculating the number of recursive calls.</div>
            <div><br>
            </div>
            <div>Given</div>
            <div><br>
            </div>
            <div>F :: * -> *</div>
            <div>f :: a = ... (f :: F a) ...</div>
            <div><br>
            </div>
            <div>used at some site</div>
            <div><br>
            </div>
            <div>... f ...</div>
            <div><br>
            </div>
            <div>0. let seen_types = ∅</div>
            <div>1. let t = the type of "f"</div>
            <div>2. If t ∈ seen_types, fail - unbounded recursion</div>
            <div>3. Add t to seen_types</div>
            <div>4. Inline the definition of "f"</div>
            <div>5. Goto 1, with any newly introduced call to "f"</div>
            <div><br>
            </div>
            <div>This construction inlines every recursive call, which
              gives you a hardware-friendly representation without
              recursion at the end. This also supports multiple
              recursion, like over a binary tree (important for
              efficient hardware). </div>
            <div><br>
            </div>
            <div>To give a concrete example of how this works, consider</div>
            <div><br>
            </div>
            <div>sum :: ∀ n . Vec n Int -> Int</div>
            <div>sum :: Vec 0       Int -> Int = \Empty -> 0 --
              Non-recursive</div>
            <div>sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd +
              (sum :: Vec n Int -> Int) tl</div>
            <div><br>
            </div>
            <div>This function is polymorphically recursive and
              perfectly reasonable to instantiate in hardware. The rule
              above succeeds in synthesizing the "sum" function, but
              will reject monomorphically recursive functions like "sum
              :: [Int] -> Int" or functions that end up being
              monomorphically recursive through a few polymorphically
              recursive "layers".</div>
            <div><br>
            </div>
            <div>One downside of this approach is that if F is divergent
              (i.e. the type of "f" never cycles back on itself but it
              always changes), this will either hang the compiler or you
              have to have an upper bound on the allowed number of
              inlines. This is probably fine - if you're trying to
              represent a function with a huge recursion depth in
              hardware, your design sucks and will be slow anyway.</div>
            <div><br>
            </div>
            <div>Again, reiterating that Clash doesn't *actually*
              support the entire subset mentioned above. That is just
              what one *could* support with the same conceptual
              approach. Instead, Clash has a few hard-coded things that
              it knows how to recurse over, like fixed-length vectors.</div>
            <div><br>
            </div>
            <div>There are probably some errors in the above - I'm not
              an expert on the internals of the clash compiler and this
              is just a brain-dump of my vague thoughts on synthesis.</div>
            <div><br>
            </div>
            <div>--Will </div>
            <div><br>
            </div>
            <div><br>
            </div>
            <div><br>
            </div>
          </div>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
    </blockquote>
  </body>
</html>