Dear Paul,This thread as well as your blog post is very interesting. Hopefully I can add something more or less valuable to it.
On your blog, you mention that your scheme for run-time strictness analysis doesn't work out because it'll have you force a function first before you can find out about its strictness. I guess this can be easily overcome by separating the function from the strictness information it carries.
One way to do this, would be by storing strictness information in the type of a function. Actually, this is exactly what type-based approaches to strictness analyses do. So, for example, an extended type of the function const,
const :: a -> b -> a
const x y = x
could read
a -> {S} -> b ->{L} a
Here, we have annotated the function-space constructor (->) with
information about whether the corresponding function is strict or lazy
in its argument. Indeed, const is lazy in its first argument and lazy
in its second. (Note that this is very simple take on storing
strictness information in types: there is plenty more to say about it,
but I will refrain from that.)
An annotated type like the one above can be easily inferred by a strictness analyser. But what exactly is type inference? Well, one way to look at it is a means to reconstruct typing information that was left out from the program. For example, if we infer the type a -> b -> a for the const function in Haskell, we are effectively completing the definition of const with explicit type information. This information can then be stored in the program. Using Java-like syntax:
const <a> <b> (x :: a) (y :: b) = xSo, now const takes two extra arguments, both of which are types rather than values. When, calling a polymorphic function, type inference then computes the type arguments for a specific instantiation of the polymorphic function:
const 2 'x' becomes const <Int> <Char> 2 'x'While typing information can proof valuable to have around at compile type, we don't actually want types to be passed around at run time. Luckily, in Haskell no run-time decisions can be made based on these type arguments, so all these extra abstractions and applications can be erased when generating code for a program.
Pretty much the same holds for the strictness annotations that are inferred by a strictness analyser. Inferring strictness can be thought of as decorating the program. For instance, for const we get something like:
const <a> <b> (x :: a{S}) (y :: b{L}) = x
where a {S} indicates strictness and {L} laziness.
Viewing strictness annotations as types, a natural step is to allow
functions to be polymorphic in their strictness annotations as well.
This is especially useful for higher-order functions. The function
apply, for example,
apply :: (a -> b) -> a -> b apply f x = f xis supposed to work on both strict and lazy functions. Moreover, depending on whether we pass it a strict or a lazy function as its first argument, it becomes, respectively, strict or lazy in its second argument. This insight can be captured quite nicely by means of a type that is polymorphic in its strictness annotations:
(a ->{i} b) ->{S} ->{i} b
Here, i is a strictness variable that is to be instantiated with
either S or L. Decorating the definition of apply may now yield
something like
apply <a> <b> {i} (f :: (a ->{i} b){S}) (x :: a{i})
Of course, just as with ordinary types, strictness annotations don't
have to be passed around at run-time: they can be erased from the
program and all that are made based on strictness information can then
be made at compile time.
But what if we don't erase these annotations? Then we can use strictness information to participate in run-time decisions as well--- just as you proposed. Let's explore that idea.
Performing strictness analysis on foldl,
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f e [] = e
foldl f e (x : xs) = foldl f (f e x) xs
we find the annotated type
(b ->{i} ->{j} b) ->{L} b ->{i} [a] ->{S} -> b
Indeed, whether foldl is strict in its second argument depends on
wether its first argument is strict in its own first argument. Let's
decorate the definition of foldl accordingly:
foldl <a> <b> {i} {j} (f :: (b ->{i} ->{j} b){L}) (e :: b{i}) (l :: [a]{S}) =
case l of
[] -> e
x : xs -> foldl <a> <b> {i} {j} f (f e x) xs
Allright, that's messy, but bear with me. (At this point, we could
erase the type arguments and only keep the strictness arguments for we
only want the latter to play a role at run time, but let's keep them
both, just to be uniform.)
Now, let's apply the foldl to (+), 0, and [1 .. 1000000] assuming that (+) is strict in both its arguments and specialised to Int,
(+) :: Int ->{S} Int ->{S} Int
and let's pass in the arguments in three steps. First we pass in the
type arguments:
foldl <Int> <Int> :: (Int ->{i} Int ->{j} Int) ->{L} Int ->{i} [Int] ->{S} Int
Then the strictness arguments:foldl <Int> <Int> <S> <S> :: (Int ->{S} ->Int ->{S} Int) ->{L} Int - >{S} [Int] ->{S} Int
Now we have obtained a specialised version of foldl that is lazy in its first argument and strict in its second and third argument! When passing in the remaining three arguments we can thus indeed evaluate the second argument before we pass it to foldl:
foldl <Int> <Int> <S> <S> (+) (0) [1 .. 1000000]Moreover, this can be done for each recursive call as well, effectively having the computation require constant space.
So, the on strictness information depending decision that is to made here, is to apply functions strictly or lazily. Funnily, if we are willing to do the static part of the strictness analysis by hand, we can already experiment a bit with this scheme in Haskell. (I've attached the source code.)
First, let us abstract from function types annotated with S or L and introduce a type class:
infixl 9 #
class Fun f where
lam :: (a -> b) -> f a b
(#) :: f a b -> (a -> b)
That is, functions are constructed by means of the method lam and
applied (destructed) by means of (#).
Haskell's built-in lazy function space (->) provides a natural implementation of the class:
instance Fun (->) where
lam = id
(#) = ($)
In addition, we provide a strict function-space constructor (:->):
newtype a :-> b = S {unS :: a -> b}
instance Fun (:->) where
lam = S
(#) = \f x -> unS f $! x
Now we can have a "hand-annotated" version of foldl:
foldl :: (Fun i, Fun j) => i b (j a b) -> i b ([a] :-> b)
foldl = lam $ \f -> lam $ \e -> lam $ \l -> case l of
[] -> e
x : xs -> foldl # f # (f # e # x) # xs
Note how the type arguments i and j play the roles of the strictness
annotations from the explanation above. Furthermore we have replaced
Haskell's lambda abstraction by means of abstraction through lam and
Haskell's function application by application through (#). Apart from
that, this is just your ordinary foldl. Well... :-)
What's important to note is that the transformation from the "normal" definition of foldl to this annotated beast could be performed at compile time by a strictness analyser.
Now, let's try it out. Say we have two versions of addition on integers: a lazy one (lplus) and a strict one (splus). Note the types:
lplus :: Int -> Int -> Int lplus = (+) splus :: Int :-> Int :-> Int splus = lam $ \m -> lam $ \n -> ((+) $! m) $! n There we go: *Main> foldl # lplus # 0 # [1 .. 1000000] *** Exception: stack overflow *Main> foldl # splus # 0 # [1 .. 1000000] 1784293664 Isn't that neat?Of course, whether this scheme would work out in practice depends on whether the cost of lazy evaluation really outweighs the cost of passing around strictness information. I'm not so sure, but I would be interested to see the results of experiments with this idea. An important factor seems to be how much strictness information that is passed around in a naive implementation of this scheme can be eliminated by "normal" compiler optimisations.
Well, just my two cents. :-) Cheers, Stefan
RuntimeSA.hs
Description: Binary data
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
