On Sun, Jun 14, 2009 at 8:18 PM, Eugene Kirpichov 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

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

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 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 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

On Wed, Jun 17, 2009 at 6:31 AM, Stefan Holdermans wrote:

...

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

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

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

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 On Thu, Jun 18, 2009 at 12:30 PM, Max Bolingbroke < batterseapower@hotmail.com> wrote:

2009/6/18 Edward Kmett :

...

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