🚀 go-pugleaf

turner@sdti.UUCP (0006-Prescott K. Turner, Jr.) wrote:
> ...isn't it false advertising to claim first-class functions unless you
> can compare functions for equality just like other types?  This means that
> the implementation will return "not-equal" if the functions are different,
> return "equal" if they can be proved equivalent, and otherwise continue
> searching for a proof or counterexample indefinitely.  Are there any
> languages which support this?

A language that requires an oracle for the Halting Problem is probably not
going to be much use to anyone but the Almighty.  ML, with good reason, omits
this.  There is another approach, taken by PS-algol, which is to give
procedure equality the semantics of pointer equality on closures.  This is
not, in practice, very useful.  What WOULD be useful would be to go further
and have *ordering* on procedures; this would mean they could be used as keys
for logarithmically searchable associative data structures.  This is a bit
harder to implement while keeping orthogonal persistence - all closures that
might be compared need to be given persistent pointers - but not ridiculously
so.  For non-persistent languages like Scheme it should be trivial to add it.

Another approach is the constructive type theory one; restrict the functions
you can define to provably terminating ones to make orthogonal equality work
with the behavioural semantics.  This is only good for a small range of
problems, though.

-- 
Jack Campin  *  Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, SCOTLAND.    041 339 8855 x6045 wk  041 556 1878 ho
INTERNET: jack%cs.glasgow.ac.uk@nsfnet-relay.ac.uk  USENET: jack@glasgow.uucp
JANET: jack@uk.ac.glasgow.cs     PLINGnet: ...mcvax!ukc!cs.glasgow.ac.uk!jack