[Haskell-cafe] What does it mean to derive "equations of restricted from" in Haskell?

Johannes Waldmann waldmann at imn.htwk-leipzig.de
Tue Jul 16 14:01:52 CEST 2013

Daryoush Mehrtash <dmehrtash <at> gmail.com> writes:

> What does "restricted form" mean?

non-restricted: e.g., f (f x y) z = f x (f y z))

restricted: the shape of function declarations in Haskell
(where lhs is a pattern) 

>  "definitions are terminating ...

non-termination: an equation like  "f x y = f y x"
when you orient it as a rule  "f x y -> f y x",
there are infinite derivations

> and exhaustive"

non-exhaustive: you have an equation "f (x : ys) = ..."
but you don't have an equation for "f [] = ..."

(all the above is is standard stuff in algebraic specification, 
equational reasoning, etc.)

- J.W.

More information about the Haskell-Cafe mailing list