Equality of functions in Haskell

Question

I am trying to define a function which would take a Double -> Double function and return its mathematical derivative. I have tried doing the following:

der :: (Double -> Double) -> (Double -> Double)
der f
    | f == exp = exp
    | otherwise = undefined

but Haskell does not support == on Double -> Double values. Is what I am trying to do impossible in Haskell?

You could do it numerically using, `f'(x) = (f(x + dx) - f(x))/dx` or automatic differentiation. What you trying to do is impossible in the general case for Turing-Complete languages. — dan_waterworth, Apr 10 '12 at 10:07

huon · Accepted Answer · 2019-05-23T23:08:13.237

Yes, what you are trying to do is impossible in Haskell, and in general: deciding whether two functions are equal for all possible inputs (without just checking every input value, if that is even possible) is equivalent to solving the Halting problem.

However, in your specific case, you can get around it, using a custom type that simulates a Double (i.e. has the same instances, and so can be used in place of it) but instead of evaluating to a number, it constructs an abstract representation of the operations the functions does. Expr represents the right-hand side of a mathematical function definition f(x) = ....

data Expr = X | Const Double |
            Add Expr Expr | Mult Expr Expr |
            Negate Expr | Inverse Expr |
            Exp Expr | Log Expr | Sin Expr | ...
       deriving (Show, Eq)

instance Num Expr where
    (+) = Add
    (*) = Mult
    ...
instance Fractional Expr where
    recip = Inverse
    ...
instance Floating Expr where
    pi = Const pi
    exp = Exp
    log = Log
    sin = Sin
    ...

Then, using rank-2 types, you can define conversion functions that convert between functions that take any Floating and Exprs:

{-# LANGUAGE Rank2Types #-}

fromFunction :: (forall a. Floating a => (a -> a)) -> Expr
fromFunction f = f X

toFunction :: Expr -> (Double -> Double)
toFunction X = \x -> x
toFunction (Const a) = const a
toFunction (Add a b) = \x -> (toFunction a x) + (toFunction b x)
...

You can also define a function diff :: Expr -> Expr that differentiates the expression:

diff X = Const 1
diff (Const _) = Const 0
diff (Add a b) = Add (diff a) (diff b)
diff (Exp a) = Mult (diff a) (Exp a)
...

Having all these parts should mean that you can differentiate (some) functions, e.g.

f x = sin x + cos x * exp x
f' = toFunction . diff . fromFunction $ f

Caveats:

this won't work in general,
defining a complete Eq instance for Expr is tricky (it is equivalent to the Halting problem, since it is basically asking if two functions are equal),
I haven't actually tested any of this code,
the differentiation and reconstruction are done at runtime, so the resulting function is highly likely to be very slow.

For this to be general you need more than just one `X` comstructor. And indeed, the `Eq` instance _is_ tricky. I once tried it, but my equality check failed to finish in overseeable time with expressions more complicated than e.g. `∂/∂x (a+x)/sin x`. — leftaroundabout, Mar 28 '12 at 12:36
Depending on what functions you actually add to your Expr data type, it may or may not be equivalent to the halting problem. In some cases, you can normalise your expressions and see if they are equivalent. Or you can make a rewrite system (which is in some ways equivalent to computing normal forms), which can decide if two expressions are equal under evaluation with toFunction. — danr, Mar 28 '12 at 16:23
There are a couple of errors here, so this example won't compile. The type signature for `fromFunction :: Floating a => (a -> a) -> Expr` seems to be incorrect, and `Add Expr Expr` should be `Plus Expr Expr.` — Anderson Green, May 23 '19 at 16:25
@huon I [tested this example](https://stackoverflow.com/a/56282943/975097), and it also works when the type signature for `fromFunction` is omitted. — Anderson Green, May 23 '19 at 23:16

augustss · Answer 2 · 2012-03-28T11:51:02.533

12

It is in general impossible to test functions for equality, since function equality should be extensional, i.e., two functions are equal if they give the same results for all arguments.

But there are other ways to define derivatives in Haskell that uses different types. For example, Automatic Differentiation, simpler version of AD.

edited Mar 28 '12 at 11:51

answered Mar 28 '12 at 11:38

augustss

22,884
5
56
93

+1 - but details on the other ways to define derivatives would be nice. – Don Roby Mar 28 '12 at 11:43
I'm not interested in numerical differentiation. – quant_dev Mar 28 '12 at 12:06
5

It's not numerical differentation, it's very different from that. It's neither numerical, nor symbolic, but the third mysterious alternative. :) – augustss Mar 28 '12 at 12:21
The words "forward-mode" suggest it is numerical. – quant_dev Mar 28 '12 at 12:32
1

@quant_dev It might suggest numerical to you, but it's not. – augustss Mar 28 '12 at 12:36
@augustss Can you provide a link to some description of what it is? I'm curious. – quant_dev Mar 28 '12 at 12:43
@quant_dev Take a look at, e.g., http://users.info.unicaen.fr/~karczma/arpap/diffalg.pdf (there is a link to it in docs of the second package). – augustss Mar 28 '12 at 12:49
Well... the abstract says "We present a purely functional implementation of the computational differentiation tools—the well known numeric (i.e., not symbolic) techniques". So I think I was right that we're talking about numerical differentiation. – quant_dev Mar 28 '12 at 12:51
1

It can be used to compute numerical values of the derivatives, but it's not done by traditional numerical differentation. – augustss Mar 28 '12 at 12:53
1

More links: http://blog.sigfpe.com/2005/07/automatic-differentiation.html http://augustss.blogspot.se/2007/04/overloading-haskell-numbers-part-2.html – augustss Mar 28 '12 at 12:58
@quant_dev: It is numerical, but it does not require uncanonical approximations. In the end, for sufficiently complex calculations, the analytic expressions become rather meaningless (too complicated) so numerical results are the only interesting thing; of course you want them to be as precise as possible. And with automatic differentiation, the results are always as precise as with symbolic differentiation, while much easier to do. – leftaroundabout Mar 28 '12 at 19:03
@leftaroundabout It's numerical if the underlying number type is numerical (which is the normal way). If the underlying number type is symbolic then AD also becomes symbolic. – augustss Mar 28 '12 at 19:50

Equality of functions in Haskell

2 Answers2

Linked