### Re: GADT and instance deriving

Richard Eisenberg <eir <at> cis.upenn.edu>

2013-05-27 08:30:59 GMT

I don't yet see a problem with the strongly-typed approach.
Following the code I posted previously, for your deriv function, you would need sommething like the following:
---
deriv :: (HList indeps -> Tensor result) -> (HList (DerivIndeps indeps result) -> Tensor (DerivResult
indeps result))
type family DerivIndeps (indeps :: [Nat]) (result :: Nat) :: [Nat]
type family DerivResult (indeps :: [Nat]) (result :: Nat) :: Nat
---
If you haven't come across them before, type families are essentially type-level functions. See here:
http://www.haskell.org/haskellwiki/GHC/Type_families Once upon a time, I earned a degree in physics
and have actually taught multivariable calculus, but those days are long gone and my memory pages giving
the exact definitions you need are buried under many more pages of type theory. Nevertheless, I'm sure
that the types you need should be easily derivable given the inputs. Using type families in this way is
often necessary when using GADTs and strongly-typed interfaces.
Overloading operators should be possible using type classes. For example:
instance Addable (Tensor n) (Tensor n) where
(+) = …
You can use functional dependencies ***or*** type families/associated types (type families and associated
types are almost two names for the same thing) for the output type. I prefer type families over functional
dependencies, because I think type families use a syntax like function application and I find them easier
to think about. But, either will work for you here.
As for your question whose answer was "Template Haskell", I have to agree with that answer. Haskell gives
you no direct access to the names of your variables, so you can't have any decisions made based on a variable
name. So, if you want your names to be significant, you have to use Template Haskell, which involves
essentially writing programs to produce Haskell code. In your case, though, I think that approach is
overkill, and it's probably best just to be a little redundant in your code (i.e. name a variable `s` and
have a string `"s"` nearby).
I hope this helps!
Richard
On May 26, 2013, at 1:20 PM, TP wrote:
> 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.
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe