[Haskell-cafe] Hit a wall with the type system

[Dan Weston]

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.
>