[Haskell-cafe] Maintaining laziness

[Jan Christiansen]

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  
Data.Number.Natural which was published by Lennart Augustsson in the  
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