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

[Chris Smith]

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.

-- 
Chris Smith