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
