Linearity Requirement for Patterns

[Koen Claessen]

Michael Hanus wrote:

 | For instance, the meaning of the definition
 |
 |   h = let x = f y in g x x
 |
 | is defined as an abbreviation for the rules
 |
 |   h = aux (f y)
 |   aux x = g x x
 |
 | W.r.t. this semantics, there is no problem even with
 | non-deterministic functions.

In ML, the meaning of the expression:

  let x = e1 in e2

is defined as an abbreviation for the expression

  mdo x <- e1; e2

W.r.t. this semantics, there is no problem even with
side-effecting functions.

/Koen.

--
Koen Claessen         http://www.cs.chalmers.se/~koen
phone:+46-31-772 5424      mailto:koen@cs.chalmers.se
-----------------------------------------------------
Chalmers University of Technology, Gothenburg, Sweden