Can Haskell compare functions?

ultranewb

unread,

Apr 7, 2012, 2:48:59 AM4/7/12

to

I have no idea how dumb this question might be. I just know the
language is "functional," and the type system is "advanced," so I
figured an "advanced enough" type system would know all the inputs/
outputs of a function to such a degree that it could determine if
functions were equivalent.

*Main> (\x -> x*0) == (\x -> 0)

<interactive>:1:13:
No instance for (Eq (a0 -> a0))
arising from a use of `=='
Possible fix: add an instance declaration for (Eq (a0 -> a0))
In the expression: (\ x -> x * 0) == (\ x -> 0)
In an equation for `it': it = (\ x -> x * 0) == (\ x -> 0)

I have no idea what any of that means (I'm a Haskell idiot). Maybe my
functions just suck (I did note that one could produce a float).
Maybe what I'm trying to do here is impossible. Maybe if I added this
"instance declaration" (if I knew what it was) it would do what I
want.

Just curious is all.

Thanks.

Paul Rubin

unread,

Apr 7, 2012, 3:09:36 AM4/7/12

to

ultranewb <pineapp...@yahoo.com> writes:
> I have no idea how dumb this question might be. I just know the
> language is "functional," and the type system is "advanced," so I
> figured an "advanced enough" type system would know all the inputs/
> outputs of a function to such a degree that it could determine if
> functions were equivalent.
>
> *Main> (\x -> x*0) == (\x -> 0)

Determining if functions are equivalent is an undecidable problem,
so Haskell doesn't provide an automatic Eq instance for functions.

Consider the Fermat's Last Theorem function:

flt :: Integer -> Integer -> Integer -> Integer -> Bool
flt a b c n = n < 3 || a^n + b^n /= c^n

flt a b c n is true iff (a,b,c,n) is not a counterexample to Fermat's
Last Theorem.

Is flt the same function as (\_ _ _ _ -> True) ?
It's unreasonable to expect Haskell to figure that out.

Coq has an even fancier type system than Haskell, that can let you prove
equality for something like flt; but it can't do it automatically,
because of that undecidability. You have to write out the proof
yourself. If you do that though, Coq can check your proof for errors.

Paul Rubin

unread,

Apr 7, 2012, 3:18:57 AM4/7/12

to

Paul Rubin <no.e...@nospam.invalid> writes:
> flt a b c n = n < 3 || a^n + b^n /= c^n
>
> flt a b c n is true iff (a,b,c,n) is not a counterexample to Fermat's
> Last Theorem.
>
> Is flt the same function as (\_ _ _ _ -> True) ?
> It's unreasonable to expect Haskell to figure that out.

Actually, QuickCheck probably could have figured it out:

f 1 (-1) 0 3 => False

but you get the idea ;-).

Roman W

unread,

Apr 18, 2012, 5:40:00 AM4/18/12

to

On Saturday, April 7, 2012 8:09:36 AM UTC+1, Paul Rubin wrote:
> ultranewb

> writes:
> > I have no idea how dumb this question might be. I just know the
> > language is "functional," and the type system is "advanced," so I
> > figured an "advanced enough" type system would know all the inputs/
> > outputs of a function to such a degree that it could determine if
> > functions were equivalent.
> >
> > *Main> (\x -> x*0) == (\x -> 0)
>
> Determining if functions are equivalent is an undecidable problem,
> so Haskell doesn't provide an automatic Eq instance for functions.

Could it at least provide a comparison of function *implementations*? Something like a function pointer comparison in C.

RW

Paul Rubin

unread,

Apr 19, 2012, 1:23:50 AM4/19/12

to

Roman W <bloody...@gazeta.pl> writes:
> Could it at least provide a comparison of function *implementations*?
> Something like a function pointer comparison in C.

Haskell doesn't have object identity, as I think that would break
referential transparency. There is a hacky library called "stable
names" that might be useable for some such purposes:

http://www.haskell.org/ghc/docs/6.12.1/html/libraries/base/System-Mem-StableName.html

Stable names live in the IO monad so you can't use them in pure code.