skaller wrote:

On Tue, 2007-01-30 at 14:24 +0100, Andrej Bauer wrote:

Simon Frost wrote:

I'm trying to use a software package written in ocaml (IBAL), however,
it fails a test due to 'Fatal error: exception Invalid_argument("equal:
functional value"). It seems that equality isn't defined for functional
values in OCAML (although I'm not an expert), so I'm wondering what the
workaround is.

This may not sound very helpful, but: you are doing something wrong if 
you need to rely on equality of functions. Equality of functions is not 
computable.

A suitable workaround would be to tell us what it is that you are doing, 
and we will tell you what to use instead of functions (if possible). To 
give you an idea of what you I am talking about:

Suppose you came to us and complained that you cannot compare 
polynomials with integer coefficients, and it turned out that you 
represent polynomials as functions. We would then tell you not to do 
that, and represent polynomials as arrays (or lists) of coefficients, or 
objects, or some other data structure that is equipped with decidable 
equality.


Actually the idea 'equality of functions is not computable'
is misleading .. IMHO. Equality of programmer written
'functions' should always be computable: more precisely one hopes
every function could have a mechanically verifiable proof
of correctness and wished programming languages provided an 
easy way to prove one.

The problem is that "programmer written functions" are a subset of all possible functions. Consider the three following expressions:

let f x = x + 3 in f

let f x y = x + y in (f 3)

let o = object method f x = x + 3 end in o#f

All of these expressions have type int -> int and thus are functions (in the general sense). At which point the naive question becomes why they aren't comparable?

Worse yet, all three are "equal" in the sense that for all ints, when called with the same argument they will return the same value.

This problem is trickier than it looks at first glance.

Brian