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

[Paul Chiusano]

Hello,
I was recently trying to figure out if there was a way, at runtime, to do
better strictness analysis for polymorphic HOFs, for which the strictness of
some arguments might depend on the strictness of the strictness of function
types that are passed as arguments [1]. As an example, consider foldl. The
'seed' parameter of foldl can be made strict as long as the binary function
used for the fold is strict in its arguments. Unfortunately, because
strictness analysis is done statically, Haskell can't assume anything about
the strictness of the binary function - assuming we only compile one
instance of foldl, it must be the most conservative version possible, and
that means making the seed parameter lazy. :-(

I started thinking about ways you could to a check at runtime for this sort
of thing, something to the effect of asking foldl, before heap-allocating a
thunk for the seed parameter, whether that parameter could be made strict.
foldl could then inspect other arguments that have been supplied, and based
on these arguments, evaluate or go ahead with creating a thunk the seed
parameter. It's a runtime cost, sure, but would it be more than the cost of
having to do an additional heap allocation? In any case a small runtime cost
might be worth it if the analysis becomes more uniform.

So, my question is: does doing this sort of runtime analysis seem like a
horrible idea? Is it even possible? Has anyone tried this in the past? (So
far I haven't found anything, but would love references if people have
them.)

Note that I'm not suggesting Haskell should do anything like this. I'm
playing around with the ideas because I'm interesting in creating a lazy
language and I was hoping to have strictness analysis be very predictable
and uniform, something the programmer can count on and use to simply reason
about space usage ... which might be hopelessly unrealistic goal! I guess
the more general question is - is "perfect" strictness analysis (however
that is defined) possible, if we're willing to incur some runtime cost? What
would that look like?

Best,
Paul

[1]:
More background on my thinking here - a bit half-baked, so bear with me!

http://pchiusano.blogspot.com/2009/06/perfect-strictness-analysis-part-1.html

http://pchiusano.blogspot.com/2009/06/perfect-strictness-analysis-part-2.html

[Eugene Kirpichov]

2009/6/15 Paul Chiusano <paul.c...@gmail.com>:

The idea looks cool, but perfect strictness analysis is not possible,
t.i. the problem of determining whether f _|_ = _|_ is undecidable,
since it is a non-trivial property of f (there exist f's for which it
is true, and ones for which it is false) and non-trivial properties
are undecidable, thanks to Rice theorem.

> Best,
> Paul
> [1]:
> More background on my thinking here - a bit half-baked, so bear with me!
> ��http://pchiusano.blogspot.com/2009/06/perfect-strictness-analysis-part-1.html
> ��http://pchiusano.blogspot.com/2009/06/perfect-strictness-analysis-part-2.html
>

> _______________________________________________
> Haskell-Cafe mailing list
> Haskel...@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jason Dagit]

On Sun, Jun 14, 2009 at 8:18 PM, Eugene Kirpichov <ekirp...@gmail.com>wrote:

> The idea looks cool, but perfect strictness analysis is not possible,
> t.i. the problem of determining whether f _|_ = _|_ is undecidable,
> since it is a non-trivial property of f (there exist f's for which it
> is true, and ones for which it is false) and non-trivial properties
> are undecidable, thanks to Rice theorem.

Unless you remove _|_ from the language. If you have a "total" functional
programming language[1] it becomes a trivial property, right? I guess this
would also extend to some dependently typed languages too.

[1] http://lambda-the-ultimate.org/node/2003

Jason

[Luke Palmer]

On Sun, Jun 14, 2009 at 5:42 PM, Paul Chiusano <paul.c...@gmail.com>wrote:

>
> Note that I'm not suggesting Haskell should do anything like this. I'm
> playing around with the ideas because I'm interesting in creating a lazy
> language and I was hoping to have strictness analysis be very predictable
> and uniform, something the programmer can count on and use to simply reason
> about space usage ... which might be hopelessly unrealistic goal!
>

Others have commented on the undecidability of your problem. I can't come
up with a reasonable definition of "perfect" which is decidable (but that
may be due to lack of imagination on my part).

However, there is nothing undecidable about your larger goal of creating a
lazy language with easy space reasoning. I wholeheartedly support this
effort, and hope you will continue to blog about your ideas in this area.

Luke

[Claus Reinke]

> I was recently trying to figure out if there was a way, at runtime, to do
> better strictness analysis for polymorphic HOFs, for which the strictness of
> some arguments might depend on the strictness of the strictness of function
> types that are passed as arguments [1]. As an example, consider foldl. The
> 'seed' parameter of foldl can be made strict as long as the binary function
> used for the fold is strict in its arguments. Unfortunately, because
> strictness analysis is done statically, Haskell can't assume anything about
> the strictness of the binary function - assuming we only compile one
> instance of foldl, it must be the most conservative version possible, and
> that means making the seed parameter lazy. :-(

As has been pointed out, strictness analysis is not decidable. That doesn't
mean it is undecidable - running the code and seeing what it does gives a
naive semi-decision procedure. So strictness analysis can be made more
precise by using more and more runtime information; unfortunately it also
becomes less and less useful as a static analysis in the process (in practice,
not just termination is important, but also efficiency of the analyses, so an
analysis would tend to become unusable before it became possibly non-
terminating - there are trade-offs between precision and efficiency).

For typical higher-order functions, there's a simple workaround, already
employed in the libraries, namely to split the definition into a simple front
that may be inlined, and a recursive back where the parameter function
is no longer a parameter. Then, after inlining the front at the call site, the
back can be compiled and analysed with knowledge of the parameter
function. See the comment above foldl:

http://www.haskell.org/ghc/docs/latest/html/libraries/base/src/GHC-List.html#foldl

Claus

[Paul Chiusano]

Thanks for replies everyone. :) I had not heard of Rice's theorem but it's
not too surprising.
A couple thoughts I had:
1. In general determining whether a function is strict is undecideable. But
a conservative approximation can certainly be guaranteed to terminate. And
what is stopping us from having our conservative analysis continue at
runtime, as terms are evaluated by the running program? I think I could
formulate some notion of having the running program incorporate all
available information from terms that have already been evaluated into its
analysis. This could be considered the best possible analysis that doesn't
affect the termination properties of the program. (Since it does not affect
evaluation order of the program or what terms are evaluated.) Of course,
like Claus says there are tradeoffs here since a more accurate analysis
might not be efficient enough timewise to be useful. But like I said, we
already have a "budget" for doing some analysis at runtime since unnecessary
memory allocation of thunks also incurs a runtime cost.

2. Having to rewrite higher-order functions so they can be inlined and
specialized isn't really a general solution, IMO. It's too fragile, can't be
counted on to apply in 100% of all relevant cases, and places additional
conceptual burden on the programmer. You have to explicitly unpack the
concept and reason about it in each case. I'd rather be able to write the
most natural, idiomatic code, and have the compiler/runtime be a bit
smarter! Of course, if you are just looking to eek out performance from your
available tools, ad hoc solutions like this are fine. But I am asking if we
could do better!

So, right now it sounds like I should maybe explore this problem a bit more
to see what I find out, but tread carefully...

Best,
Paul

[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

[Paul Chiusano]

Stefan,
Thank you for the detailed response! In trying to follow your email I got a
bit confused by your notation -

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.

Did you mean to say that const is *strict *in its first param and lazy in
its second (since const _|_ y = _|_)? Also, can you explain your notation,
how does a -> {S} -> b ->{L} a indicate the strictness? Why not just {S} a
-> {L} b -> a?

Best,
Paul

> information to participate in run-time decisions as well---just as you

[Ryan Ingram]

Also, partial application + seq throws a wrench in things:

seq (const undefined) ()
== ()
/= seq undefined ()

but

seq (const undefined ()) ()
== undefined
== seq undefined ()

So const is only strict in its first argument when fully applied; I
think any strictness annotation would have to have information about
*when* the strictness applies.

That is, these two functions need to have different types:

const1 = \x -> seq x (\y -> x)
const2 = \x ->\y -> x

The first is strict always whereas the second is only strict when fully applied.

-- ryan

On Wed, Jun 17, 2009 at 3:07 PM, Paul Chiusano<paul.c...@gmail.com> wrote:
> Stefan,
> Thank you for the detailed response! In trying to follow your email I got a
> bit confused by your notation -
>>
>> �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.
>

> Did you mean to say that const is strict in its first param and lazy in its

[Stefan Holdermans]

Ryan,

> Also, partial application + seq throws a wrench in things: [...]

You're absolutely right. I did not take into account the effects of
seq in my previous post. However, this is exactly the subject of a
paper I presented at TFP, two weeks ago. A revised version of the
paper will be available soon; slided can already be picked up from

http://people.cs.uu.nl/stefan/pubs/holdermans09spreading.html .

[Stefan Holdermans]

Paul,

> In trying to follow your email I got a bit confused by your notation -
>
> 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.
>

> Did you mean to say that const is strict in its first param and lazy

> in its second (since const _|_ y = _|_)? Also, can you explain your
> notation, how does a -> {S} -> b ->{L} a indicate the strictness?
> Why not just {S} a -> {L} b -> a?

I'm sorry for the confusion. Indeed, const, as the type was intended
to reflect, const is strict in its first argument and lazy in its
second.

I prefer to put the annotation on the function arrow as strictness is
a property of functions, but if you want to have these annotations
prefixing the argument types, then I guess that's fine as well; in the
end, it really doesn't matter, does it?

Cheers,

Stefan

[Stefan Holdermans]

Paul,

>> Did you mean to say that const is strict in its first param and
>> lazy in its second (since const _|_ y = _|_)? Also, can you explain
>> your notation, how does a -> {S} -> b ->{L} a indicate the
>> strictness? Why not just {S} a -> {L} b -> a?
>
> I'm sorry for the confusion. Indeed, const, as the type was intended
> to reflect, const is strict in its first argument and lazy in its
> second.

Ah, sorry. Now I see where I really confused you. Someone pointed out
that I erroneously inserted an extra -> in the type. The type should
read

a ->{S} b ->{L} a

HTH,

[Edward Kmett]

I have been exploring a weak form of runtime strictness analysis in a
tracing JIT project of my own in the spirit of TraceMonkey. Basically a
tracing JIT doesn't compile blocks of code but instead once a tracing point
has been passed often enough, it starts a trace from that point logging the
series of instructions executed to a bounded log. If you make it back to the
starting point before the log fills up then you've identified a superblock
with a bunch of side exits for handling when your assumptions are violated.

What is interesting is in a lazy setting, if you are tracing a bytecode
representation that knows about allocation and thunks, you can do some
additional optimizations in here. If on every path to a side exit or the end
of the loop you find that the thunk is evaluated you can evaluate it
strictly and move its execution earlier in the trace. This gives you a weak
form of runtime strictness analysis. If the pointer to that thunk never
escapes, then you can unbox the contents of the thunk and operate on its
members in registers. Add constant folding, polyinline caching to improve
branch prediction for spineless tagless g-machine thunk evaluation, and code
migration to the side exits and it becomes an interesting runtime system.

But the key concern for the sake of the current discussion is that it models
strictness analysis and unboxing quite naturally as an artifact of the
jitting process. So that said, a form of conservative strictness analysis at
runtime is possible.

-Edward Kmett

[Max Bolingbroke]

2009/6/18 Edward Kmett <ekm...@gmail.com>:

> What is interesting is in a lazy setting, if you are tracing a bytecode
> representation that knows about allocation and thunks, you can do some
> additional optimizations in here. If on every path to a side exit or the end
> of the loop you find that the thunk is evaluated you can evaluate it
> strictly and move its execution earlier in the trace. This gives you a weak
> form of runtime strictness analysis. If the pointer to that thunk never
> escapes, then you can unbox the contents of the thunk and operate on its
> members in registers. Add constant folding, polyinline caching�to improve
> branch prediction for spineless tagless g-machine thunk evaluation, and code
> migration to the side exits�and it becomes an interesting runtime system.

This sounds absolutely awesome! Is the source code for your prototype
publicly available anywhere? I'd love to take a look at the basic
structure of something like this - trace JITing is something I keep
meaning to look at in more depth.

Cheers,
Max

[Edward Kmett]

Hi Max,
I don't have anything in a public repository at this time. I have been
exploring a series of designs in this space trying to see if any could be
applied to a system like GHC's bytecode interpreter, but up to now I've been
working mostly with cooperatively jitting x86-64 assembly to x86-64 assembly
for a possibly commercial project. I have only recently started trying to
adapt my research to a more functional setting. If you hop on #haskell some
time, I'd be happy to talk further.

-Edward Kmett