<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">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`:<br>
<br>
    mapMaybeSF<br>
      = \ (@ a) (@ b) (f :: SF a b) -><br>
          case f of { SF @ s f2 s2 -><br>
          SF<br>
            (\ (a1 :: Maybe a) (ds2 :: ((), ((), (((), (((), (((), s), ())), ((), ((), ())))), ((), ()))))) -></div></blockquote><div><br></div><div>That is indeed true. But note that as long as you manage to inline `mapMaybeSF`, the final `runSF` will only allocate once on the "edge" of each iteration, all intermediate allocations will have been fused away. But the allocation of these non-sense records seems unfortunate.</div><div><br></div><div>Optimisation-wise, I see two problems here:</div><div><ol><li>`mapMaybeSF` is already too huge to inline without INLINE. That is because its lambda isn't floated out to the top-level, which is because of the existential @s (that shouldn't be a problem), but also its mention of f2. The fact that f2 occurs free rather than as an argument makes the simplifier specialise `mapMaybeSF` for it, so if it were floated out (thereby necessarily lambda-lifted) to top-level, then we'd lose the ability to specialise without SpecConstr (which currently only applies to recursive functions anyway).<br></li><li>The lambda isn't let-bound (which is probably a consequence of the previous point), so it isn't strictness analysed and we have no W/W split. If we had, I imagine we would have a worker of type `s -> ...` here. W/W is unnecessary if we manage to inline the function anyway, but I'm pretty certain we won't inline for larger programs (like `mapMaybeSF` already), in which case every failure to inline leaves behind such a residue of records.<br></li></ol></div><div>So this already seems quite brittle. Maybe a very targeted optimisation that gets rid of the boring ((), _) wrappers could be worthwhile, given that a potential caller is never able to construct such a thing themselves. But that very much hinges on being able to prove that in fact every such ((), _) constructed in the function itself terminates.<br></div><div><br></div><div><div><div>There are a few ways I can think of in which we as the programmer could have been smarter, though:</div><div><br></div><div><ul><li>Simply by specialising `SF` for the `()` case:<br><br><span style="font-family:monospace">data SF a b where<br>  SFState :: !(a -> s -> Step s b) -> !s -> SF a b<br>  SFNoState :: !(a -> Step () b) -> SF a b</span><br><br>And then implementing every action 2^n times, where n is the number of `SF` arguments. That undoubtly leads to even more code bloat.</li><li>An alternative that I'm a little uncertain would play out would be<br><br>data SMaybe a = SNothing | SJust !a<br>data SF a b where<br>  SF :: !(SMaybe (s :~: ()) ->  !(a -> s -> Step s b) -> !s -> SF a b<br><br>and try match on the proof everywhere needed to justify e.g. in `(.)` only storing e.g. s1 instead of (s1, s2). Basically do some type algebra in the implementation.</li><li>An even simpler thing would be to somehow use `Void#` (which should have been named `Unit#`), but I think that doesn't work due to runtime rep polymorphism restrictions.</li></ul><div>I think there is lots that can be done to tune this idea.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Mi., 1. Apr. 2020 um 01:16 Uhr schrieb Alexis King <<a href="mailto:lexi.lambda@gmail.com">lexi.lambda@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> On Mar 31, 2020, at 17:05, Sebastian Graf <<a href="mailto:sgraf1337@gmail.com" target="_blank">sgraf1337@gmail.com</a>> wrote:<br>
> <br>
> 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<br>
<br>
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.<br>
<br>
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:<br>
<br>
    mapMaybeSF :: SF a b -> SF (Maybe a) (Maybe b)<br>
    mapMaybeSF f = proc v -> case v of<br>
      Just x -> do<br>
        y <- f -< x<br>
        returnA -< Just y<br>
      Nothing -> returnA -< Nothing<br>
<br>
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`:<br>
<br>
    mapMaybeSF<br>
      = \ (@ a) (@ b) (f :: SF a b) -><br>
          case f of { SF @ s f2 s2 -><br>
          SF<br>
            (\ (a1 :: Maybe a) (ds2 :: ((), ((), (((), (((), (((), s), ())), ((), ((), ())))), ((), ()))))) -><br>
<br>
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.<br>
<br>
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<br>
<br>
    SF (\a ((), x) -> ... Yield ((), y) b ...) ((), s)<br>
<br>
to<br>
<br>
    SF (\a x -> ... Yield y b) s<br>
<br>
by parametricity. Is that an unreasonable ask? I don’t know!<br>
<br>
Another subtlety I considered involves recursive arrows, where I currently depend on laziness in (|||). Here’s one example:<br>
<br>
    mapSF :: SF a b -> SF [a] [b]<br>
    mapSF f = proc xs -> case xs of<br>
      x:xs -> do<br>
        y <- f -< x<br>
        ys <- mapSF f -< xs<br>
        returnA -< (y:ys)<br>
      [] -> returnA -< []<br>
<br>
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:<br>
<br>
    lazy :: SF a b -> SF a b<br>
    lazy sf0 = SF g (Unit sf0) where<br>
      g a (Unit sf1) = case runSF sf1 a of<br>
        (b, sf2) -> Yield (Unit sf2) b<br>
<br>
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.<br>
<br>
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.<br>
<br>
Alexis</blockquote></div></div></div></div>