[Haskell-cafe] Runtime strictness analysis for polymorphic HOFs?
Stefan Holdermans
stefan at cs.uu.nl
Wed Jun 17 06:31:28 EDT 2009
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 --------------
More information about the Haskell-Cafe
mailing list