[Haskell-cafe] GADT and instance deriving

[TP]

Hi Tillmann and Richard,

Thanks for your answers.

I have tried to analyze the code snippets you proposed.
I've tried to transpose your examples to what I need, but it is not easy.

The problem I see with putting the list of independent variables (*) at the 
type level is that at some time in my code I want for instance to perform 
formal mathematical operations, for example I want a function "deriv" that 
takes f(x(t),y(t),z(t)) as input, and returns

df/dt = ∂f/∂x*dx/dt + ∂f/∂y*dy/dt + ∂f/∂z*dz/dt

If the list of dependencies is encoded at the type level, I don't see how to 
produce the previous output from the knowledge of "f(x(t),y(t),z(t))". You 
understand that what I want to do is some type of basic Computer Algebra 
System library.

Moreover, I want overloading for infix functions as '*', '/', '⋅' (scalar 
product), × (vector product) etc., that is why I have used typeclasses (see 
the code I showed in my previous post). For example, for the time being I 
will restrict myself to scalar product between vector and vector, vector and 
dyadic, dyadic and vector (a dyadic is a tensor of order 2, a matrix if you 
prefer). So I have three instances for scalar product '⋅'. I don't see how 
to combine this idea of overloading or derivation function with what you 
proposed. But I have perhaps missed something.

Thanks,

TP

(*): That is to say the list of tensors of which one tensor depends, e.g. 
[t,r] for E(t,r), or simply [x,y,z] for f(x(t),y(t),z(t)) where x, y, and z 
themselves are scalars depending on a scalar t). In the test file of my 
library, my code currently looks like:

-----------------
type Scalar = Tensor Zero
type Vector = Tensor One
[...]
let s = (t "s" []) :: Scalar
let v = (t "v" [i s]) :: Vector
let c1 = v + v
let c2 = s + v⋅v
-----------------

t is a smart constructor taking a string str and a list of independent 
variables, and makes a (Tensor order) of name str.

So in the example above, s is a scalar that depends on nothing (thus it is 
an independent variable), v is a vector that depends on s (i is a smart 
constructor that wraps s into a Box constructor, such that I can put all 
independent variables in an heterogeneous list).
c1 is the sum of v and v, i.e. is equal to 2*v.
c2 is the sum of s and v scalar v.
If I try to write:

let c3 = s + v

I will obtain a compilation error, because adding a scalar and a vector has 
no meaning.

Is there some way to avoid typeable in my case?

Moreover, if I wanted to avoid the String in the first argument of my smart 
constructor "t", such that

let s = (t []) :: Scalar

constructs an independent Scalar of name "s", googling on the topic seems to 
indicated that I am compelled to use "Template Haskell" (I don't know it at 
all, and this is not my priority).
Thus, in a general way, it seems to me that I am compelled to use some 
"meta" features as typeable or Template Haskell to obtain exactly the result 
I need while taking benefit from a maximum amount of static type checking.