Re: Use of irrefutable
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
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
Use of irrefutable
Mike Jones writes: I am looking at the Hawk Signal module, where the following definition occurs: lift1 f (List xs) = List $ lazyMap f xs where lazyMap f ~(x:xs) = f x : lazyMap f xs Now setting aside how the function is used in Hawk, I ran a little experiment to see what happens when the irrefutable definition is removed by calling it with: a = List [1, 2] b = lift1 (+ 1) a Now without it I get an error for a "non-exhaustive pattern". With it, I get an "irrefutable pattern failed". Because you used a finite list as input. lazyMap only matches the cons case, but a finite list always has a nil case. The error messages may be different, but the problem is the same. Try "take 2 $ lift1 (+ 1) (cycle a)". Can some one explain to me the advantages and disadvantages of using irrefutable matching, including how irrefutable matching is used in general? Why and when it is used, etc. I'm pretty sketchy on this too. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
RE: Use of irrefutable
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
Use of irrefutable
Hi, I have a rather naive question, being new to Haskell. I am looking at the Hawk Signal module, where the following definition occurs: lift1 f (List xs) = List $ lazyMap f xs where lazyMap f ~(x:xs) = f x : lazyMap f xs Now setting aside how the function is used in Hawk, I ran a little experiment to see what happens when the irrefutable definition is removed by calling it with: a = List [1, 2] b = lift1 (+ 1) a Now without it I get an error for a "non-exhaustive pattern". With it, I get an "irrefutable pattern failed". Can some one explain to me the advantages and disadvantages of using irrefutable matching, including how irrefutable matching is used in general? Why and when it is used, etc. Thanks, Mike