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

[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

On Wed, Jun 17, 2009 at 6:31 AM, Stefan Holdermans <stefan at cs.uu.nl> 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
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090617/9aa0efb3/attachment-0001.html