differential operation (Typing Question!)

|> Message: 1
|> From: "Zhe Fu"
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.l... Have fun and thanks for any help Jay Cox
participants (1)
-
Jay Cox