Mike Jones wrote:
| lift1 f (List xs) = List $ lazyMap f xs
| where
| lazyMap f ~(x:xs) = f x : lazyMap f xs
:
| a = List [1, 2]
| b = lift1 (+ 1) a
:
| "non-exhaustive pattern".
| "irrefutable pattern failed".
Hi Mike, let me tell you how irrefutable patterns work in
Haskell. Look at the definition of the standard Haskell
function "map":
map f [] = []
map f (x:xs) = f x : map f xs
Suppose we know that the list we apply map to is always
infinite. In this case, we know that the first case ([])
will never occur, so we can just as well take it away:
infiniteMap f (x:xs) = f x : infiniteMap f xs
(A compiler like GHC now probably complains about
"non-exhaustive pattern", because we have left out a case.
It cannot know we only intend to apply this function on
infinite lists!)
Inifinite lists occur in Hawk, as the streams of inputs and
outputs to circuits never stop.
If we take a look at the semantics of Haskell, then the
function infiniteList *insists* on evaluating its list
argument until it can see it has at least one element. This
is called "strictness"; we say that the function is strict
in its second argument.
Sometimes, this leads to bad behavior of the program. We
want to be able to tell the compiler: "yes, I know I did not
define all patterns" and "yes, I know the argument will
always be of the form (x:xs)" and "so, trust me, you do not
have to check this before entering the function".
So, all the programmer has to do is inserting a "~", for
irrefutable pattern:
lazyMap ~(x:xs) = f x : lazyMap f xs
Now you tell the compiler that the list you are constructing
is infinite. Moreover, you can inspect the *result* of the
function before it ever evaluates its argument! To see this,
note that the above definition is (almost) a short-hand for:
lazyMap' xs = f (head xs) : lazyMap' f (tail xs)
This function is obviously *not* strict in its first
argument.
----
I know there are some places (in a hardware description
language ;-) where these tricks are necessary (for example
constructing a loop over lists), but I don't see why the
standard "lift1" function should use lazy map. It can lead
to worse space behavior too ...
Maybe one of the Hawk implementors can enlighten us on
this subject?
Regards,
Koen.
--
Koen Claessen http://www.cs.chalmers.se/~koen
phone:+46-31-772 5424 e-mail:[EMAIL PROTECTED]
-----------------------------------------------------
Chalmers University of Technology, Gothenburg, Sweden
