[Haskell-cafe] Re: Safe forward-mode AD in Haskell?

[Björn Buckwalter]

Oops, that went to soon.

My intention was to ask for comments from those who know better than
I. These corners of the type system are pretty unknown to me but I am
trying to learn from e.g. Oleg's array branding[1].

Anyway, please rip my exposition apart and expose my sure-to-be flawed
logic and terminology. ;)

Cheers,
Bjorn

[1] http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs


On 5/8/07, Björn Buckwalter <bjorn.buckwalter at gmail.com> wrote:
> Dear all,
>
>
>
>
>
> = Introduction =
>
> In [1] Siskind and Pearlmutter expose the danger of "perturbation
> confusion" in forward-mode automatic differentiation. In particular
> they state:
>
>     "We discuss a potential problem with forward-mode AD common to
>     many AD systems, including all attempts to integrate a forward-mode
>     AD operator into Haskell."
>
> This literate Haskell message shows how, using a type system extension
> of the Glasgow Haskell Compiler[2] (GHC), we can statically guarantee
> that perturbation confusion does not occur.
>
>
> = Code =
>
> The below code closely follows the Haskell code in the appendices
> of [1]. It relies on GHC's arbitrary-rank polymorphism(?) extension
> to Haskell 98.
>
> > {-# OPTIONS_GHC -fglasgow-exts #-}
>
> In our definition of the 'Bundle' data type we add the phantom type
> 's', which will be the key to disambiguating between different
> application of the 'd' operator.
>
> > data Bundle s a = Bundle a a
>
> > instance Num a => Show (Bundle s a) where
> >   showsPrec p (Bundle x x') = showsPrec p [x,x']
>
> > instance Num a => Eq (Bundle s a) where
> >   (Bundle x x') == (Bundle y y') = (x == y)
>
> > lift z = Bundle z 0
>
> > instance Num a => Num (Bundle s a) where
> >   (Bundle x x') + (Bundle y y') = Bundle (x + y) (x' + y')
> >   (Bundle x x') * (Bundle y y') = Bundle (x * y) (x * y' + x' * y)
> >   fromInteger z = lift (fromInteger z)
>
> > instance Fractional a => Fractional (Bundle s a) where
> >   fromRational z = lift (fromRational z)
>
> We provide a type signature for 'd' where we existentially quantify
> the phantom type 's' to prevent mixing of bundles from different
> 'd' operators.
>
> > d :: Num a => (forall s. Bundle s a -> Bundle s a) -> a -> a
> > d f x = let (Bundle y y') = f (Bundle x 1) in y'
>
> The extential quantification makes the definition
>
> ] constant_one' x = d (\y -> x + y) 1
>
> impossible since 'x' originates externally to the 'd' operator. GHC
> rejects the definition with a "Inferred type is less polymorphic
> than expected". In order to pass the compiler the definition must
> be changed to the corrected[1] version.
>
> > constant_one x = d (\y -> (lift x) + y) 1
> > should_be_one_a = d (\x -> x * (constant_one x)) 1
> > should_be_one_b = d (\x -> x * 1 ) 1
>
> > violation_of_referential_transparency = should_be_one_a /= should_be_one_b
>
>
> = References =
>
> [1] http://www.bcl.hamilton.ie/~qobi/nesting/papers/ifl2005.pdf
> [2] http://haskell.org/ghc/
>