I must be missing something, because to me the contract seems to be much simpler to express (than the Functor + Isomorphism route you seem to me to be heading towards): diff :: (Eq x, Dense x, Subtractible x, Subtractible y, Divisible y x yOverX) => (x -> y) -> x -> yOverX class Dense a where addEpsilon :: a -> a class Subtractible a where takeAway :: a -> a -> a class Divisible a b c | a b -> c where divide :: a -> b -> c Then diff is just: diff f a = if dx == dx' then error "Zero denom" else dydx where a' = addEpsilon a dx = a' `takeAway` a dx' = a `takeAway` a' dy = f a' `takeAway` f a dydx = dy `divide` dx With the instances: instance Dense Double where addEpsilon x = x * 1.0000001 + 1.0e-10 instance Dense Int where addEpsilon x = x + 1 instance Subtractible Double where takeAway x y = x - y instance Subtractible Int where takeAway x y = x - y instance Divisible Double Double Double where divide x y = x / y instance Divisible Int Int Int where divide x y = x `div` y and throwing in {-# OPTIONS_GHC -fglasgow-exts #-}, I get: *Diff> diff sin (0.0::Double) 1.0 *Diff> diff (\x -> x*7+5) (4::Int) 7 Dan Weston Chris Smith wrote:
Hi Dan, thanks for answering.
Dan Piponi wrote:
When you specify that a function has type a -> b, you're entering into a bargain. You're saying that whatever object of type a you pass in, you'll get a type b object back. "a -> b" is a statement of that contract.
Sure, that much makes perfect sense, and we agree on it.
Now your automatic differentiation code can't differentiate any old function. It can only differentiate functions built out of the finite set of primitives you've implemented (and other "polymorphic enough" functions).
Sure. To be more specific, here's the contract I would really like.
1. You need to pass in a polymorphic function a -> a, where a is, at *most*, restricted to being an instance of Floating. This part I can already express via rank-N types. For example, the diffFloating function in my original post enforces this part of the contract.
2. I can give you back the derivative, of any type b -> b, so long as b is an instance of Num, and b can be generalized to the type a from condition 1. It's that last part that I can't seem to express, without introducing this meaningless type called AD.
There need be no type called AD involved in this contract at all. Indeed, the only role that AD plays in this whole exercise is to be an artifact of the implementation I've chosen. I could change my implementation; I could use Jerzy's implementation with a lazy infinite list of nth-order derivatives... or perhaps I could implement all the operations of Floating and its superclasses as data constructors, get back an expression tree, and launch Mathematica via unsafePerformIO to calculate its derivative symbolically, and then return a function that interprets the result. And who knows what other implementations I can come up with? In other words, the type AD is not actually related to the task at hand.
[...]
Luckily, there's a nice way to express this. We can just say diff :: (AD a -> AD a) -> a -> a. So AD needs to be exported. It's an essential part of the language for expressing your bargain, and I think it *is* the Right Answer, and an elegant and compact way to express a difficult contract.
Really? If you really mean you think it's the right answer, then I'll have to back up and try to understand how. It seems pretty clear to me that it breaks abstraction in a way that is really rather dangerous.
If you mean you think it's good enough, then yes, I pretty much have conluded it's at least the best that's going to happen; I'm just not entirely comfortable with it.