Wed Feb 17 11:20:43 CET 2010

Typeful symbolic differentiation of compiled functions

The interesting part about this[1] paper is the `reflect' function:

     > class Term t a | t -> a where
     >     reflect :: t -> a -> a
     > newtype Const a = Const a deriving Show
     > data Var a      = Var     deriving Show
     > data Add x y    = Add x y deriving Show
     > newtype Sin x   = Sin x   deriving Show
     > instance Term (Const a) a where reflect (Const a) = const a
     > instance Term (Var a) a where reflect _ = id
     > instance (D a, Term x a, Term y a) => Term (Add x y) a
     >     where
     >     reflect (Add x y) = \a -> (reflect x a) + (reflect y a)
     > instance (D a, Term x a) => Term (Sin x) a
     >     where
     >     reflect (Sin x) = sin . reflect x

     ... This is the straightforward emulation of GADT. The function
     `reflect' removes the `tags' after the symbolic
     differentiation. Actually, `Sin' is a newtype constructor, so there is
     no run-time tag to eliminate in this case.

Note that the different kinds of terms are types collected in a class,
not constructors collected in a type.  This is compile-time type
dispatching vs. run-time tag dispatching.

This is an interesting trick, and also seems to be at the basis of a
lot of later work.  So let's have a look at this GADT trick in
isolation [2][3].

[1] http://okmij.org/ftp/Haskell/differentiation/differentiation.lhs
[2] http://okmij.org/ftp/ML/#GADT
[3] http://lambda-the-ultimate.org/node/1293