Jan Christiansen jac at informatik.uni-kiel.de
Wed Jan 7 06:07:07 EST 2009

```This is great. I am working on the very same topic for quite a while
now. My aim is to develop a tool that tells you whether a function is
least strict. My work is based on an idea by Olaf Chitil:

http://www.cs.kent.ac.uk/people/staff/oc/

I think he was the first who introduced the idea of least strictness.
In a paper in the pre-proceedings of IFL 2006 he introduced the term
least strict and presented the idea behind a tool called StrictCheck.
This tool was supposed to check whether a function is least strict.
The problem with this tool was that it proposes non-sequential
function definitions that are not implementable in Haskell.

The main example in the StrictCheck paper is the definition of unzip
by using foldr. This one is very similar to your partition example as
it is too strict if you do not use lazy pattern matching for the
tuple structure.

unzip2 :: [(a, b)] -> ([a], [b])
unzip2 = foldr (\(x,y) (xs,ys) -> (x:xs,y:ys)) ([],[])

My favorite example right now is the multiplication of Peano numbers.
Suppose the definition of a data type for Peano numbers and addition
and multiplication.

data Natural = Z | S Natural

(+) :: Natural -> Natural -> Natural
Z + y = y
S x + y = S (x + y)

(*) :: Natural -> Natural -> Natural
Z * _ = Z
S x * y = y + (x * y)

Now we can define an infinite Peano number as follows

infinity :: Natural
infinity = S infinity

The evaluation of Z * infinity yields Z while infinity * Z does not
terminate. The tool I am working on is supposed to yield the
following information.

Natural> strictCheck2 (*) 5 100

You have to fulfil

f (S _|_) Z = Z (_|_)

This states that the evaluation of S _|_ * Z yields _|_ but it could
yield Z.

Therefore we can improve the function as follows

(*) :: Natural -> Natural -> Natural
Z   * _ = Z
S _ * Z = Z
S x * y = y + (x * y)

Now the evaluation of infinity * Z yields Z as we wanted it to. If we
test this new implementation using StrictCheck we get

*Natural> strictCheck2 (*) 5 100

The function seems to be least strict

The non least strict definition of (*) is taken from the module
numbers package at hackage. I mention this here because I think it
clearly shows that it is even hard for experienced Haskell
programmers to define least strict functions.

An even more promising area of application are functional logic
programs as least strict functions result in smaller search spaces.
For example I was able to improve the enumeration of pythagorean
triples in Curry by a factor of 4 only by making a function least
strict.

Cheers, Jan

```