Fusing loops by specializing on functions with SpecConstr?

Alexis King lexi.lambda at gmail.com
Tue Mar 31 23:16:50 UTC 2020

```> On Mar 31, 2020, at 17:05, Sebastian Graf <sgraf1337 at gmail.com> wrote:
>
> Yeah, SPEC is quite unreliable, because IIRC at some point it's either consumed or irrelevant. But none of the combinators you mentioned should rely on SpecConstr! They are all non-recursive, so the Simplifier will take care of "specialisation". And it works just fine, I just tried it

Ah! You are right, I did not read carefully enough and misinterpreted. That approach is clever, indeed. I had tried something similar with a CPS encoding, but the piece I was missing was using the existential to tie the final knot.

I have tried it out on some of my experiments. It’s definitely a significant improvement, but it isn’t perfect. Here’s a small example:

mapMaybeSF :: SF a b -> SF (Maybe a) (Maybe b)
mapMaybeSF f = proc v -> case v of
Just x -> do
y <- f -< x
returnA -< Just y
Nothing -> returnA -< Nothing

Looking at the optimized core, it’s true that the conversion of Maybe to Either and back again gets eliminated, which is wonderful! But what’s less wonderful is the value passed around through `s`:

mapMaybeSF
= \ (@ a) (@ b) (f :: SF a b) ->
case f of { SF @ s f2 s2 ->
SF
(\ (a1 :: Maybe a) (ds2 :: ((), ((), (((), (((), (((), s), ())), ((), ((), ())))), ((), ()))))) ->

Yikes! GHC has no obvious way to clean this type up, so it will just grow indefinitely, and we end up doing a dozen pattern-matches in the body followed by another dozen allocations, just wrapping and unwrapping tuples.

Getting rid of that seems probably a lot more tractable than fusing the recursive loops, but I’m still not immediately certain how to do it. GHC would have to somehow deduce that `s` is existentially-bound, so it can rewrite something like

SF (\a ((), x) -> ... Yield ((), y) b ...) ((), s)

to

SF (\a x -> ... Yield y b) s

by parametricity. Is that an unreasonable ask? I don’t know!

Another subtlety I considered involves recursive arrows, where I currently depend on laziness in (|||). Here’s one example:

mapSF :: SF a b -> SF [a] [b]
mapSF f = proc xs -> case xs of
x:xs -> do
y <- f -< x
ys <- mapSF f -< xs
returnA -< (y:ys)
[] -> returnA -< []

Currently, GHC will just compile this to `mapSF f = mapSF f` under your implementation, since (|||) and (>>>) are both strict. However, I think this is not totally intractable—we can easily introduce an explicit `lazy` combinator to rein in strictness:

lazy :: SF a b -> SF a b
lazy sf0 = SF g (Unit sf0) where
g a (Unit sf1) = case runSF sf1 a of
(b, sf2) -> Yield (Unit sf2) b

And now we can write `lazy (mapSF f)` at the point of the recursive call to avoid the infinite loop. This defeats some optimizations, of course, but `mapSF` is fundamentally recursive, so there’s only so much we can really expect.

So perhaps my needs here are less ambitious, after all! Getting rid of all those redundant tuples is my next question, but that’s rather unrelated from what we’ve been talking about so far.

Alexis
```