On Sun, Feb 20, 2011 at 6:11 PM, Edward Z. Yang wrote:

I'm curious about how strict types interact horribly with fusion and other optimisations; I know strictness limits your optimisation ability, but my impression is that it shouldn't blow up too horribly unless you're trying to implement extremely clever optimisations.

I'm curious too. In my experience it often helps e.g. getting things unboxed. Do we really need to go all the way to type families to get strict data types? Wouldn't something simpler like a Haskell 98 Data.Strict module do? Johan

On Mon, Feb 21, 2011 at 11:04 AM, Max Bolingbroke wrote:

On 21 February 2011 02:28, Johan Tibell wrote:

...

On Sun, Feb 20, 2011 at 6:11 PM, Edward Z. Yang wrote:

...

I'm curious about how strict types interact horribly with fusion and other optimisations; I know strictness limits your optimisation ability, but my impression is that it shouldn't blow up too horribly unless you're trying to implement extremely clever optimisations.

I'm curious too. In my experience it often helps e.g. getting things unboxed.

I haven't seen what Roman is describing, but I would guess that it's something like if GHC sees:

 let x = f y in g x

Then it can apply a rule g (f y) = foo. But if it sees:

 case f y of x -> g x

It may get scared and not do the rewrite. Adding strictness to your program introduces extra case bindings at the Core level and therefore makes this problem more frequent. You can see this problem with the following program:

"""

g_f :: Bool -> Bool g_f y = y

{-# RULES "g/f" forall y. g (f y) = g_f y #-}

{-# NOINLINE f #-} f :: Bool -> Bool f = id

{-# NOINLINE g #-} g :: Bool -> Bool g = not

one x = g y  where !y = f x

two x = g y  where y = f x

main = do    print (one True, two True) """

GHC successfully rewrites "one" but not "two" using the RULE, so the output is (False, True).

Hmm... did you mean to say "two" but not "one"?

Max

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

-- Work is punishment for failing to procrastinate effectively.

Max Bolingbroke wrote:

On 21 February 2011 02:28, Johan Tibell wrote:

...

On Sun, Feb 20, 2011 at 6:11 PM, Edward Z. Yang wrote:

...

I'm curious about how strict types interact horribly with fusion and other optimisations; I know strictness limits your optimisation ability, but my impression is that it shouldn't blow up too horribly unless you're trying to implement extremely clever optimisations.

I'm curious too. In my experience it often helps e.g. getting things unboxed.

I haven't seen what Roman is describing, but I would guess that it's something like if GHC sees:

let x = f y in g x

Then it can apply a rule g (f y) = foo. But if it sees:

case f y of x -> g x

It may get scared and not do the rewrite.

Yes, GHC won't rewrite in this case which is a big problem. The other big problem is that strict types have much uglier laws than lazy ones. For instance, fst (x,y) = x but strictFst (StrictPair x y) = y `seq` x. Strict types lead a lot of seqs which are often quite artificial, disrupt other optimisations because of the dependencies they introduce and prevent code from becoming dead. In general, there seems to be a big difference between "evaluate this now" (which is what strict types do), "it's ok to evaluate this now" (which is what's needed for unboxing) and "this is guaranteed to be evaluated at this point" (which strict types do, too, and which is quite useful). There is also http://hackage.haskell.org/trac/ghc/ticket/4081. Roman

On February 21, 2011 08:15:38 Tyson Whitehead wrote:

The non-deterministic semantics

??? _|_ x -> possibly _|_ or x

are also pretty interesting. Very reminiscent of what can happen with rewrites in the presence of the other two. Could there be something here (i.e., this would allow you to have rewrites that still preserve the semantics as the non-determinism would officially be part of the semantics)?

To clarify a bit more. Traditionally, I believe the problem is you use seq in some function f. Appearing in some composition g, f results in the semantics g _|_ /= a There is a rewrite that either you or the compiler would like to perform on the composition g to give g', but due to seq/pseq in f you windup with g' _|_ = _|_ (or the other way around). If we are using ??? instead of seq/pseq, however, this the rewrite can be expressed such that the semantics are preserved g _|_ = a or _|_ non-deterministically g' _|_ = a or _|_ non-deterministically Cheers! -Tyson

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

Johan Tibell wrote:

Do we really need to go all the way to type families to get strict data types? Wouldn't something simpler like a Haskell 98 Data.Strict module do?

Sure. Type families just give us nicer syntax. Also this: class Strictify a where strictify :: a -> Strict a unstrictify :: Strict a -> a Roman