home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
BURKS 2
/
BURKS_AUG97.ISO
/
BURKS
/
LANGUAGE
/
ML
/
GIML
/
STU77.HTM
< prev
next >
Wrap
Text File
|
1996-12-09
|
2KB
|
50 lines
<b>Comments from David Boyle</b><br>
Response from Andrew<p>
<b>What's this I hear about ML having all the nasty constructs of
other languages (like loops, else - if ladders). Is this because
many problems simply can't be implemented without the use of these
constructs or is it a facility for "quick dirty code" for programmers
who are not interested in proving their software?
</b><br>
So far as I know there is a while loop, I've never
used it.
We do not need loops, recursion will always do the job.
<br>
Consider the while loop
<pre>while B do S;</pre>
Where B is a boolean expression and S is a statement.
We model the action of S by changing some data state
space DS. The program fragment above might be rewritten
<pre>while fB(DS) do DS := fS(DS);</pre>
where fB and fS are proper functions which take in the
data state DS and return appropriate values. DS might
include all the global and local variables of the program.
This program fragment may now be modelled with ML
<pre>fun while fB fS DS = if fB DS then (while fB fS (fS DS)) else DS;
</pre>
If then else ladders are there and it's OK to
use them - pattern matching is preferred but it's
not always convenient (I suspect not always possible).
If _ then _ else _ introduces a new complexity
to proofs - but it's not a serious problem.
<br>Quick & dirty is possible in ML, but somehow the
quick dirty programs turn out slower and cleaner
than their C equivalents.<p>
<b>
If the former is true then surely the use of ML will continue to
be very scarce. If the latter is true then it seems that any language
(including C) which has these nasty contructs removed (or just
avoided by the lecturer!) can be proved as easily as ML.
</b><br>
Latter - yes, you could build ML by taking the bad
bits from C and adding a few new good bits. In the
end all languages are more or less the same.