[Haskell-cafe] Re: Re: Re: Hit a wall with the type system
Chris Smith
cdsmith at twu.net
Thu Nov 29 18:00:13 EST 2007
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
More information about the Haskell-Cafe
mailing list