[Haskell-cafe] Runtime strictness analysis for polymorphic HOFs?

[Stefan Holdermans]

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) = x

So, 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 x

is 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: RuntimeSA.hs
Type: application/octet-stream
Size: 610 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090617/710b89ec/RuntimeSA-0001.obj
-------------- next part --------------