Proposal: Strict types

[Roman Leshchinskiy]

Edward Z. Yang wrote:
>
> * The bog-easy way of pulling this off (from the implementation side)
> would just be "seq", but ignore that it exists when you're performing
> rewrite rules. [1]

Yes, though I doubt it's all that easy. It isn't necessarily clear under
exactly which conditions this should happen. We could say that we want the
rule "f (g x) = f' x" to fire in this case:

  case g x of y -> f y

What about this case, though?

  case g x of y ->
  case h x of z -> f y

Or this?

  case g x of y ->
  case y of (y1,y2) ->
  case y1 of _ ->
  case y2 of _ -> f y

In general, two function applications can be quite far apart in the
presence of seqs and they won't be brought together by the simplifier
because those seqs introduce an artificial ordering on the computations.

> So it seems to me that once we decide that a structure ought to be
> unboxed (strict), then there's no point in applying anymore rewrite rules:
> we presumably want the unboxed structure because it's now going to be
> shipped to the far ends of the earth, traversed in non-rewritable ways,
> etc.  So in this sense, the failure of strict rewrite rules to make sense
> is sensible.

I disagree. Here is an example from DPH. A central operation is mapD which
applies in parallel a function to a distributed value (Dist). The
intention is that each thread will apply this function to its private
value:

mapD :: (a -> b) -> Dist a -> Dist b

We have the obvious rewrite rule:

"mapD/mapD" mapD f (mapD g x) = mapD (f . g) x

Now, mapD fully evaluates its argument before passing it to the function
so using strict types here seems like a good idea.

Suppose we use strict pairs:

data a :*: b = !a :*: !b

and get an intermediate term like this:

 mapD (\(x:*:y) -> f1 x :*: g1 y) $
 mapD (\(x:*:y) -> f2 x :*: g2 y) xy

The "mapD/mapD" rule gives us this:

  mapD (\(x :*: y) -> case f2 x of x' ->
                      case g2 y of y' ->
                      case f1 x' of x'' ->
                      case g1 y' of y'' -> x'' :*: y'') xy

If we have rules for f1/f2 and g1/g2, they won't fire even though we
really want them to. Contrast this with lazy pairs:

  mapD (\(x,y) -> (f1 x, g1 y)) $
  mapD (\(x,y) -> (f2 x, g2 y)) xy
  =
  mapD (\(x,y) -> (f1 (f2 x), g1 (g2 y))) xy

Here, the rules will fire without any problems. But now GHC doesn't know
that x and y are fully evaluated (or, rather, that it's ok to evaluate and
unbox x and y before doing anything else like executing loops).

Note that f1 and g1 will usually be strict so the two versions are really
semantically equivalent. But GHC won't necessarily be able to figure this
out on its own.

Roman