[Haskell-cafe] Well typed OS

[William Yager]

On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181021/c24fa7f2/attachment.html>