<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>