differential operation (Typing Question!)

Fri, 11 Jan 2002 12:27:05 -0600 (CST)

If you happen to be talking about symbolically differentiating expressions,
I happen to be in the early stage of developing a extendible module to
do such a thing right now!  However I seem to have come across some typing
problems.

But to understand my problem I may need to try to summarize the details
thereof

I started out with a recursive datatype

>data BasDif r = Ext (r (BasDif r)) |
>     Symbol Sym | Constant Rational |
>     Sum (BasDif r) (BasDif r) |
>     Prod (BasDif r) (BasDif r) |
>     Divide (BasDif r) (BasDif r) |
>     Negate (BasDif r) | D (BasDif r)

Notice the Ext( r (BasDif r)).  I use this to extend the datatype.

I define a basic differentiating function "d" on all of these constructs
except Ext.  When d pattern matches (Ext x) it calls some instance of the
diff class on x.  diff on some function g(u)  where u is an expression
returns a pair (u,g') back to "d" so that "d"  can complete the chain rule
d(g(u))=g'(u)*d(u).

(technically it returns a function g' which takes two arguments: a
data constructor and a BasDif expression of some sort

the current expected typing of diff (forgive me for not knowing proper
vernacular) is given below.

>class Diff x where
>  diff:: Sym -> x a -> (a, (x a1 -> r (BasDif r)) -> a1 -> BasDif r)

Its rather complex but I'll admit I stole it from the ghci interpreter
giving me the type of function which did conceptually what I wanted it to
do. the types are below.

Differentiate> :type diffTrig
forall t a a1 r.
t -> Trig a -> (a, (Trig a1 -> r (BasDif r)) -> a1 -> BasDif r)
Differentiate> :type diffNe
forall t a a1 r.
t -> NumExp a -> (a, (NumExp a1 -> r (BasDif r)) -> a1 -> BasDif r)

Before I expound upon why the type needs to be so complicated, let me
tell you what I'm trying to do with these diff functions that follow.

(In the following definitions, prod, sum_, negate_, are more or less
helper functions which make some trivial simplifications as they make
products, sums, and additive inverses)

>data NumExp a =  N Rational a
>diffNe s (N i x) =
>    let j = i-1
>    in if (j /= 0 )
>       then (x,\f-> \v -> prod (Ext(f (N (i-1) v))) (Constant i))
>       else (x,\_-> \_->Constant 1)
>
>instance Diff NumExp where
> diff=diffNe

>data Trig a = Sin a | Cos a | Tan a | Cot a| Sec a |Csc a deriving Show
>diffTrig s (Sin x) = (x, \f -> Ext . f . Cos)
>diffTrig s (Cos x) = (x, \f -> negate_ . Ext . f . Sin)
... more defs
>instance Diff Trig where
>  diff = diffTrig

With these definitions, I have enough to take derivatives of (BasDif Trig)
expressions or (BasDif NumExp) expressions, but not both.

Therefore I defined the above expressions (as complicated as they are)
so that I could make a instance of diff by combining the two without
copy/pasting code  (and without explicitly calling diffTrig and diffNe)
thus being able to differentiate expressions of BasDif TrigNumExp (and
thus being able to differentiate expressions with + - * /
sine,cosine,tangent,their reciprocals and any combination thereof with
a rational exponent)

>data TrigNumExp a= T (Trig a) | NE (NumExp a)
>instance Show a => Show (TrigNumExp a) where
>  showsPrec _ (T x) = shows x
>  showsPrec _ (NE x) = shows x
>
>diffTrigNumExp s (T x)  = let (k,f)= diff s x in (k,\g->f (g .T))
>diffTrigNumExp s (NE x) = let (k,f)= diff s x in (k,\g->f (g .NE))
>
>instance Diff TrigNumExp where
>  diff = diffTrigNumExp

In this I have succeeded. THEN I tried to do the same for inverse
trig functions.  These are of a rather different nature.  the derivative
of inverse sine requires something to represent square roots of
expressions, hence I use the constructor for NE expressions.

>diffArcT s (ArcSin x) =(x,\f-> \y->Ext(f ( N (-1/2)
>                  (sum_ (Constant 1) (negate_ (prod y y))))))
>diffArcT s _ = error "incomplete"

the type of diffArcT is

Differentiate> :type diffArcT
forall t a r1 r.
t
-> ArcTrig a
   -> (a,
          (NumExp (BasDif r1) -> r (BasDif r)) -> BasDif r1 -> BasDif r)

I suppose the error message I get when adding this function to the
module is understandable given the class constraints..

...
Differentiate.v2.lhs:177:
    Couldn't match `ArcTrig a1' against `NumExp (BasDif r)'
    Expected type:
      Sym
      -> ArcTrig a
         -> (a, (ArcTrig a1 -> r1 (BasDif r1)) -> a1 -> BasDif r1)
    Inferred type:
      Sym
      -> ArcTrig a
         -> (a, (NumExp (BasDif r) -> r2 (BasDif r2)) -> BasDif r
            -> BasDif r2)
    In the definition of `diff': diffArcT
...

but seems to me to be a reasonable relaxing of types for the class doesn't
work either (in fact it produces errors for every instance of diff

...
Old class
>class Diff x where
>  diff:: Sym -> x a -> (a, (x a1 -> r (BasDif r)) -> a1 -> BasDif r)

New class
class Diff x where
  diff:: Sym -> x a -> (a, (x1 a1 -> r (BasDif r)) -> a1 -> BasDif r)

New errors with new class
    Cannot unify the type-signature variable `x1'
       with the type `TrigNumExp'
       Expected type:
         Sym
         -> TrigNumExp a ->
         (a, (x1 a1 -> r (BasDif r)) -> a1 -> BasDif r)
       Inferred type:
         Sym
         -> TrigNumExp a
         -> (a, (TrigNumExp a11 -> r1 (BasDif r1)) -> a11 -> BasDif r1)
In the definition of `diff': diffTrigNumExp
Differentiate.v2.lhs:177:
    Cannot unify the type-signature variable `x1'
       with the type `NumExp'
       Expected type:
         Sym
         -> ArcTrig a
         -> (a, (x1 a1 -> r (BasDif r)) -> a1 -> BasDif r)
       Inferred type:
         Sym
         -> ArcTrig a
         -> (a,
         (NumExp (BasDif r1) -> r2 (BasDif r2)) -> BasDif r1 -> BasDif r2)
...
etc.

What I don't understand is WHY NumExp cannot be unified with x1. what I
would personally would like to understand is if Haskell's Hindley-Miller
type system can even deal with what I want to do (basically I want a type
for diff such that the definition of diffArcT would be tolerable to the
compiler.)

I realize I am a bit over my head here so it might be concievable that
just some pointer to a reference on how haskell deals with type resolution
might help as well, or perhaps some general method for concieving of a
general type for a member of a class, or perhaps some ideas to re-engineer
this module.

Anyway, I suppose this module might be of some interest to some people
so I have put it in a temporary place so that some people may play with
it.  It doesnt have any functions for reading general expresssions yet,
you could enter some funky multivariable expression and see what comes
out.  (I must warn you, if you happen to use the "d" function, it doesnt
do much but the simplest simplifications. some of the less trivial
simplifications have been commented out because they do not help the
runtime.

It is at (temporarely)
http://home.flash.net/~flygal/Jay/Haskell/Differentiate/v0.1/Differentiate.lhs

Have fun and thanks for any help

Jay Cox