[Haskell-cafe] Well typed OS

[Vanessa McHale]

Anything that's tail recursive could be converted to a while loop and
then clocked, no? You could for instance compile

fact :: Int -> Int

fact 0 = 1

fact n = n * fact (n - 1)

to hardware even if it would not be a good idea.

On 10/21/18 4:16 AM, William Yager wrote:
>
>
> On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz <jo at durchholz.org
> <mailto:jo at durchholz.org>> wrote:
>
>
>     Is that subset described somewhere?
>
>
> So there are two possible answers to this:
>
> 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
>
> 2. The subset that Clash *could* support with (roughly) its current
> approach, which I think I can answer a bit better: 
>
> I gave a brief hand-wavy description earlier -
> "non-monomorphically-recursive"
>
> 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).
>
> Much simpler is to simply disallow monomorphic recursion, and then you
> shift the work of proving finite recursion depth to the type level. 
>
> There's then a simple (constructive) rule for proving termination and
> calculating the number of recursive calls.
>
> Given
>
> F :: * -> *
> f :: a = ... (f :: F a) ...
>
> used at some site
>
> ... f ...
>
> 0. let seen_types = ∅
> 1. let t = the type of "f"
> 2. If t ∈ seen_types, fail - unbounded recursion
> 3. Add t to seen_types
> 4. Inline the definition of "f"
> 5. Goto 1, with any newly introduced call to "f"
>
> 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). 
>
> To give a concrete example of how this works, consider
>
> sum :: ∀ n . Vec n Int -> Int
> sum :: Vec 0       Int -> Int = \Empty -> 0 -- Non-recursive
> sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd + (sum :: Vec n Int ->
> Int) tl
>
> 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".
>
> 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.
>
> 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.
>
> 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.
>
> --Will 
>
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181021/c6a6682f/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181021/c6a6682f/attachment.sig>