[Haskell-cafe] Propositions in Haskell

[Tillmann Rendel]

Hi,

Patrick Browne wrote:
> In am trying to understand why some equations are ok and others not.
>
> I suspect that in Haskell equations are definitions rather than assertions.

Yes. Haskell function definitions look like equations, but in many ways, 
they aren't. Here is an example for an equation that is not valid as a 
Haskell function definition:

   g x = 42
   f (g x) = x    -- not valid

The problem is that we cannot use g at the left-hand side.


Here is an example that doesn't mean what you might be hoping for:

   f x = f x
   f x = 42

Seen as an equation system, this should constrain f to be a function 
that always returns 42. But in Haskell, it defines f to be a 
non-terminating function. The reason is that only the first line counts, 
because it covers all possible argument values. The second line is ignored.

The behavior changes if we swap the two lines:

   g x = 42
   g x = g x

Again, only the first line counts, so g is the function that always 
returns 42.

Here is a more complicated example:

   h 27 = 42
   h x = h x
   h 13 = 100

What function is h?

   Tillmann