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