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

[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.chiusano at 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
> 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
>>
>>
>>
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>