I guess that deciding whether two functions are equal in most cases is algorithmically impossible. However maybe there exists quite a large domain of decidable cases? If so, how can I employ that in Haskell?
It is a common situation when one has two implementations of the same function, one being straightforward but slow, and the other being fast but complex. It would be nice to be able to check if these two versions are equal to catch bugs in the more complex implementation.
Every function with a "searchable" domain and a decidable codomain has decidable equality. šThe classic example of a big searchable domain is the cantor space:
import Data.Searchable
type Nat = Int š š š-- works with Integer too
type Cantor = Nat -> Bool
bit :: Set Bool
bit = doubleton True
cantor :: Set Cantor
cantor = fmap (!!) . sequence . repeat $ bit
decEq :: (Eq a) => (Cantor -> a) -> (Cantor -> a) -> Bool
decEq f g = forEvery (\c -> f c == g c)
So for example:
ghci> decEq ($ 4) ($ 4)
True
ghci> decEq ($ 4) ($ 100)
False
ghci>šdecEq (\c -> c 4 && c 42) (\c -> not (not (c 4) || not (c 42)))
True
Searchable is based on work by Martin Escardo, very cool stuff. šData.Searchable comes from the infinite-search package.
Luke