csnjr@its63b.ed.ac.uk (Nick Rothwell) (11/30/87)
In article <347@sequent.cs.qmc.ac.uk> keithc@qmc.ac.uk (Keith Clarke) writes: > >Michael Schmidt writes (neulich shrieb): >> there is no concept of rewrites in ML > >Correct. But there is a large sublanguage of ML that does >have a rewrite semantics. >One can apply equational reasoning to programs written in the >sublanguage. (I'm ignoring the problem of partial functions, >like most people who work with strict functional languages). Forgive my mathematical ignorance here - but, by "partial" do you mean nonterminating, or undefined for some arguments? You can't have exceptions and maintain the applicative property of your sublanguage, since you've lost referential transparency - for example, fun f() = raise F fun g() = raise G val x = f() + g() handle F => 1 || G => 2 The evaluation order becomes important. If you omit exceptions, then you've got to define some behaviour for "head(nil)" - or is this what you mean by partial? You *can* have exceptions in a pure functional language, if you treat exceptions as special values - I did this for the language described in my thesis, precisely for this reason. There's an implementation overhead, and you have to program some things slightly differently, but it works... -- Nick Rothwell, Laboratory for Foundations of Computer Science, Edinburgh. nick%lfcs.ed.ac.uk@nss.cs.ucl.ac.uk <Atlantic Ocean>!mcvax!ukc!lfcs!nick ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ "Nothing's forgotten. Nothing is ever forgotten." - Herne