🚀 go-pugleaf

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