On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen wrote:

On Sat 25 May 2013 00:37:59 SGT, TP wrote:

...

Is this the right way to go? Is there any other solution?

I believe whether it's right or just depends on what you want to express.

...

Do you confirm that tilde in s~s1 means "s has the same type as s1"?

It means: Both your s and s1 are "Eq"s but not necessarily the same one.

No, it doesn't. s1 ~ s2 means the types are the same. ~ is the "equality constraint". http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.... To say that s1 and s2 are Eq's, but not necessarily the same one, we would write a constraint of the form: (Eq s1, Eq s2) => That is a completely different notion of equality than ~. Your first example allows that, so you could have one with an Int and

one with a String inside (both are Eqs).

a = Box 1 b = Box "hello"

Now if that first code compiled, your code

(Box s1) == (Box s2) = s1 == s2

would effectively perform

... = 1 == "hello"

Nope. It would perform (Just 1) == (cast "hello"), which is completely possible, since (cast "hello") has the same type as (Just 1).

TP wrote:

Where are these examples that can help me to write my instance? I have tried to read the source of the implemented instances in data.typeable, not so easy for me.

Ok, by doing a better search on Google ("instance typeable " blog), I have found interesting information: http://blog-mno2.csie.org/blog/2011/12/24/what-are-data-dot-typeable-and-dat... and especially: http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.htm... """ In this new class, we are no longer restricted to datatypes with a maximum of 7 parameters, nor do we require the parameters to be of kind *. """ So, I have to try that. I will give some feedback here (from my beginner point of view). TP

Hi Richard, Thanks a lot for your answer. We had a discussion about some "Tensor" type some time ago: https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ Today I have a type constructor "Tensor" in which there is a data constructor Tensor (among others): ------------ data Tensor :: Nat -> * where [...] Tensor :: String -> [IndependentVar] -> Tensor order [...] ------------ The idea is that, for example, I may have a vector function of time and position, for example the electric field: E( r, t ) (E: electric field, r: position vector, t: time) So, I have a Tensor (E) that depends on two tensors (r and t). I want to put r and t in a list, the list of independent variable of which E is a function. But we see immediately that r and t have not the same type: the first is of type "Tensor One", the second of type "Tensor Zero". Thus we cannot put them in a list. This is why I have tried to use an heterogeneous list: http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:... Thus in the first place the problem comes from the fact that I have put the order of the Tensor in the type rather than in the data constructors. But it is useful: * I can make type synonyms type Scalar = Tensor Zero type Vector = Tensor One [...] * with multi-parameter typeclasses, I can define operations as: class Division a b c | a b -> c where (/) :: a -> b -> c and then I implement these operations on a subset of types: instance (PrettyPrint (Tensor a)) => Division (Tensor a) Scalar (Tensor a) where ZeroTensor / _ = ZeroTensor _ / ZeroTensor = error "Division by zero!" t / s = Divide t s So, the code is clear, and instead of runtime dimension checks, everything is detected at compilation. So the choice of putting the order in the type seems to be correct. My only need to use Typeable comes from the heterogeneous list. But how to do without? Thanks, TP Richard Eisenberg wrote:

Thankfully, the problem you have is fixed in HEAD -- the most recent version of GHC that we are actively working on. I am able, using the HEAD build of GHC, to use a `deriving Typeable` annotation to get a Typeable instance for a type that has non-*-kinded parameters. To get the HEAD compiler working, see here: http://hackage.haskell.org/trac/ghc/wiki/Building

However, I'm worried that other aspects of your design may be suboptimal. The `Box` type you mentioned a few posts ago is called an existential type. Existential types have constructors who have type parameters that are *not* mentioned in the conclusion. As an example, your `Box` constructor involved a type parameter `a`, but the `Box` type itself has no parameters. This existential nature of the type is why your comparison didn't work.

A Tensor, however, doesn't seem like it would need to be an existential type. The order of the tensor should probably (to my thinking) appear in the type, making it not existential anymore.

In general, I (personally -- others will differ here) don't love using Typeable. By using Typeable, you are essentially making a part of your program dynamically typed (i.e., checked at runtime). The beauty of Haskell (well, one of its beauties) is how it can check your code thoroughly at compile time using its rich type language. This prevents the possibility of certain bugs at runtime. Using Typeable circumvents some of that, so I would recommend thinking carefully about your design to see if its use can be avoided.

Just to diffuse any flames I get for the above paragraph: I fully support the role of Typeable within Haskell. Indeed, sometimes it is unavoidable. In fact, I have a small update to the Typeable interface on my to-do list (adding functionality, not changing existing). I am just arguing that its use should be judicious.

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.

Would this work for you? ---- {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators #-} data Nat = Zero | Succ Nat type One = Succ Zero type Two = Succ One data Operation :: [Nat] -- list of operand orders -> Nat -- result order -> * where ElectricField :: Operation '[One, Zero] One GravitationalField :: Operation '[Zero] One opToString :: Operation a b -> String opToString ElectricField = "E" opToString GravitationalField = "G" data HList :: [Nat] -> * where HNil :: HList '[] HCons :: Tensor head -> HList tail -> HList (head ': tail) data Tensor :: Nat -> * where Tensor :: Operation operands result -> HList operands -> Tensor result ---- The idea here is that a well-typed operands list is intimately tied to the choice of operation. So, we must somehow expose the required operands in our choice of operation. The Operation GADT does this for us. (It is still easy to recover string representations, as in opToString.) Then, in the type of the Tensor constructor, we say that the operands must be appropriate for the operation. Note that `operands` is still existential in the Tensor constructor, but I believe that is what you want. Does this work for you? I will repeat that others will likely say that this approach is *too* strongly-typed, that the types are getting in the way of the programmer. There is merit to that argument, to be sure. However, I still believe that using a detailed, strongly-typed interface will lead sooner to a bug-free program than the alternative. Getting your program to compile and run the first time may take longer with a strongly-typed interface, but I posit that it will have fewer bugs and will be ready for "release" (whatever that means in your context) sooner. Richard On May 25, 2013, at 10:23 AM, TP wrote:

Hi Richard,

Thanks a lot for your answer. We had a discussion about some "Tensor" type some time ago:

https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ

Today I have a type constructor "Tensor" in which there is a data constructor Tensor (among others):

------------ data Tensor :: Nat -> * where [...] Tensor :: String -> [IndependentVar] -> Tensor order [...] ------------

The idea is that, for example, I may have a vector function of time and position, for example the electric field:

E( r, t )

(E: electric field, r: position vector, t: time)

So, I have a Tensor (E) that depends on two tensors (r and t). I want to put r and t in a list, the list of independent variable of which E is a function. But we see immediately that r and t have not the same type: the first is of type "Tensor One", the second of type "Tensor Zero". Thus we cannot put them in a list. This is why I have tried to use an heterogeneous list:

http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:...

Thus in the first place the problem comes from the fact that I have put the order of the Tensor in the type rather than in the data constructors. But it is useful:

* I can make type synonyms type Scalar = Tensor Zero type Vector = Tensor One [...]

* with multi-parameter typeclasses, I can define operations as:

class Division a b c | a b -> c where (/) :: a -> b -> c

and then I implement these operations on a subset of types:

instance (PrettyPrint (Tensor a)) => Division (Tensor a) Scalar (Tensor a) where ZeroTensor / _ = ZeroTensor _ / ZeroTensor = error "Division by zero!" t / s = Divide t s

So, the code is clear, and instead of runtime dimension checks, everything is detected at compilation. So the choice of putting the order in the type seems to be correct. My only need to use Typeable comes from the heterogeneous list. But how to do without?

Thanks,

TP

Richard Eisenberg wrote:

...

Thankfully, the problem you have is fixed in HEAD -- the most recent version of GHC that we are actively working on. I am able, using the HEAD build of GHC, to use a `deriving Typeable` annotation to get a Typeable instance for a type that has non-*-kinded parameters. To get the HEAD compiler working, see here: http://hackage.haskell.org/trac/ghc/wiki/Building

However, I'm worried that other aspects of your design may be suboptimal. The `Box` type you mentioned a few posts ago is called an existential type. Existential types have constructors who have type parameters that are *not* mentioned in the conclusion. As an example, your `Box` constructor involved a type parameter `a`, but the `Box` type itself has no parameters. This existential nature of the type is why your comparison didn't work.

A Tensor, however, doesn't seem like it would need to be an existential type. The order of the tensor should probably (to my thinking) appear in the type, making it not existential anymore.

In general, I (personally -- others will differ here) don't love using Typeable. By using Typeable, you are essentially making a part of your program dynamically typed (i.e., checked at runtime). The beauty of Haskell (well, one of its beauties) is how it can check your code thoroughly at compile time using its rich type language. This prevents the possibility of certain bugs at runtime. Using Typeable circumvents some of that, so I would recommend thinking carefully about your design to see if its use can be avoided.

Just to diffuse any flames I get for the above paragraph: I fully support the role of Typeable within Haskell. Indeed, sometimes it is unavoidable. In fact, I have a small update to the Typeable interface on my to-do list (adding functionality, not changing existing). I am just arguing that its use should be judicious.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe