[<<][compsci][>>][..]

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

[Reply][About]

[<<][compsci][>>][..]