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