Re: Use of irrefutable

[John Matthews]

On Thu, 20 Apr 2000, Koen Claessen wrote:

 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".
 

[snip]

 
 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?

You're right, we should be able to remove the lazy pattern matching in
practice. For any practical circuit, all circuits have at least one
"delay" element along every cyclic definition. There are however
some "pathological" circuits that require lazy pattern matching, such as
the following:

wierdCirc :: Signal Int
wierdCirc = lift1 (const 0) wierdCirc


This circuit has a zero-delay cycle. With lift1 implemented using lazy
pattern-matching, it returns the following signal:

 0, 0, ...

With strict pattern-matching, wierdCirc is undefined (equals bottom).

In general, one would like the following law to hold for all
xs and ys of type (Signal a) (where "==" here is semantic equality, not
Haskell's overloaded equality operator):

  lift2 (\x y - x) xs ys == xs

With lift2 implemented using strict pattern matching the above equation
doesn't hold when xs is a defined signal, but ys == bottom:

  Let zeros = delay 0 zeros.

  Then...

  lift2 (\x y - x) zeros bottom == bottom
 /= zeroes

With lazy pattern matching, the above equation holds:

  lift2 (\x y - x) zeros bottom == zeros

Even with lazy pattern matching the original equation doesn't hold when
xs == bottom. Instead,

  lift2 (\x y - x) bottom ys == lift1 id bottom
  ==  bottom, bottom, ...

But at least this equation holds:

  lift2 (\x y - x) (lift1 id xs) ys == lift1 id xs


It would be nice if Haskell had the ability to define partially unlifted
datatypes, something like

  data #Signal a = #Sig a (#Signal a)

the idea being that the least defined value for this type is:

  #Sig bottom (#Sig bottom (#Sig bottom ...))

Thus one could always pattern-match along the "spine" of a #Signal without
hitting deadlock, even for the following value:

  loop :: #Signal a
  loop = loop

the compiler would ensure this by inserting a "lowering" function for any
definition that might otherwise be undefined. For #Signal, the lowering
function would be:

  lowerSig :: #Signal a - #Signal a
  lowerSig ~(#Sig x xs) = #Sig x (lowerSig xs)

For example, the above loop function would be silently rewritten by the
compiler to be:

  loop = lowerSig loop

With such a datatype, then the equation

  lift2 (\x y - x) xs ys == xs

would always hold.

By the way, I haven't really given a lot of thought to unlifted
datatypes, and it could very well be that they are unworkable!

To summarize, while lazy pattern matching for the lift operations is nicer
from a program transformation and verification perspective, strict pattern
matching seems to work fine for "normal" circuits, that is, circuits
with no zero-delay cycles. Since, as Koen says, the strict lifting
functions can have better space behavior, we should probably change our
implementation.

-john

Re: Use of irrefutable

[Koen Claessen]

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

RE: Use of irrefutable

[Mike Jones]

Let me explore this a bit:

  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!

What exactly do you mean by inspect the result before the evaluation? Do you
mean you can start consuming the produced list before all elements are
generated?

Mike