[Haskell-cafe] Equality of functions

[Ralf Laemmel]

Adam Zachary Wyner wrote:

>Question -- is this all there is to the issue, or is there something more?
> Apologies in advance for not understanding the math better here.
>
You can compare functions in a pointwise fashion,
which does not work (other than approximatively) for infinite domains.
This is the black box approach.

You can also compare functions in a proof-theoretic fashion.
Try to proof a derivation that f can be transformed into g.
This is the white-box approach.
This requires reasoning at the level of program text.

>Question -- though Haskell, as a lazy language, does not otherwise have
>problems with infinite lists, why does it here?
>
Because lazyness only helps in cases where we don't want to see the full 
infinite data structure.
Equality is a universal property; we would need to iterate over all 
elements of the domain.

>Question -- is there some way around this problem?  It is very handy to be
>able to have a variable over functions and then compare the value to a
>designated function.  This would let me say things like:
>
>when variableFunctionX == functionA then....
>otherwise etc...
>
Don't understand.

>One possible (dirty?) solution I thought up is to use the record types of
>Hugs to correlate the function with a name of type String:
>
>type FunctionNameFunction = Rec (functionName :: String, functionFunction
>:: WhateverFunction)
>
>Then, whenever one needs to use the function, one uses the value of
>functionFunction, but whenever one needs to evaluate for identity, one
>uses the value of functionName, using just string identity.  Of course,
>this makes lots of things less 'pretty' (to apply a function to an
>argument, one has to first 'pull out' the function from the record), but
>it addresses a general problem.  One would also have to keep careful track
>of which functionNames correlate with with functionFunctions.
>  
>
Yes, one can represent functions by type codes.
These type codes would be interpreted by an Apply class (as in the HList 
library).
Type codes could be compared for equality (again demonstrated in the 
HList paper).
Modulo some extra tweaking, we can compute type equality for such 
*fixed* functions.

In fact, one can build a little functional language in the type system 
this way.
Expressions in this language would distinguished terms.
One could even implement the abovementioned white-box approach in the 
type system.
(For any given system of proof/transformation rules.)

I am sure this is too complicated and too restricted than to be truly 
useful.

Cheers,
Ralf