Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.haskell > #211

Re: Can Haskell compare functions?

Show all headers | View raw

ultranewb <pineapple.link@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.

Back to comp.lang.haskell | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Can Haskell compare functions? ultranewb <pineapple.link@yahoo.com> - 2012-04-06 23:48 -0700
  Re: Can Haskell compare functions? Paul Rubin <no.email@nospam.invalid> - 2012-04-07 00:09 -0700
    Re: Can Haskell compare functions? Paul Rubin <no.email@nospam.invalid> - 2012-04-07 00:18 -0700
    Re: Can Haskell compare functions? Roman W <bloody_rabbit@gazeta.pl> - 2012-04-18 02:40 -0700
      Re: Can Haskell compare functions? Paul Rubin <no.email@nospam.invalid> - 2012-04-18 22:23 -0700

csiph-web