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

[Dan Piponi]

Chris,

> So I want the parameter to be more restricted.  No one is going to write
> a function that *only* works on AD types.

But exporting AD doesn't force people to write functions that work on
AD types, people can write whatever functions they like. They're only
constrained if they want to pass the function into 'diff', at which
point it needs to work on AD.

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. 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). So you have quite a complex contract to write. You
want to say "for any function you give me that is built out of these
functions (and other ...), and no others, I can give you back the
derivative". You need to say this somewhere otherwise it's like a
contract for a house purchase that doesn't bother to say where the
boundary line to the next house is (*). 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.
--
Dan

(*) I admit that I have bought a house like this, but it's not a good thing.