24 May 2013 18:37

```Hello,

I continue my learning of "not so obvious" Haskell/GHC topics when
encountering problems in the code I write.
Below is a small example of an heterogeneous list, using GADT, inspired
from:

----------

data Box where
Box :: Eq s => s -> Box

instance Eq Box where

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

This code does not compile, because GHC is not sure that s1 and s2 have the
same type:

----------
Could not deduce (s ~ s1)
from the context (Eq s)
bound by a pattern with constructor
Box :: forall s. Eq s => s -> Box,
in an equation for `=='
[and more lines...]
```

24 May 2013 19:41

### Re: GADT and instance deriving

```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.

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"

which is not possible.
```
25 May 2013 00:06

### Re: GADT and instance deriving

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".

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).
```_______________________________________________
```
25 May 2013 06:08

### Re: GADT and instance deriving

```
On 25/05/13 06:06, Alexander Solla wrote:
> On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen <mail <at> nh2.me
> <mailto:mail <at> nh2.me>> 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".
>
>
> To say that s1 and s2 are Eq's, but not necessarily the same one, we
> would write a constraint of the form:

Sorry, I didn't formulate that clearly: I meant to describe what the
problem in the complaint about s1 ~ s2 is, not what s1 ~ s2 means.

>     Your first example allows that, so you could have one with an Int and
>     one with a String inside (both are Eqs).
>
>      ...
>
> Nope.  It would perform (Just 1) == (cast "hello"), which is completely
> possible, since (cast "hello") has the same type as (Just 1).

That's why I said "your first example"; there is no cast in it.
```
25 May 2013 00:09

### Re: GADT and instance deriving

On Fri, May 24, 2013 at 9:37 AM, TP wrote:
Hello,

I continue my learning of "not so obvious" Haskell/GHC topics when
encountering problems in the code I write.
Below is a small example of an heterogeneous list, using GADT, inspired
from:

----------

data Box where
Box :: Eq s => s -> Box

instance Eq Box where

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

This code does not compile, because GHC is not sure that s1 and s2 have the
same type:

----------
Could not deduce (s ~ s1)
from the context (Eq s)
bound by a pattern with constructor
Box :: forall s. Eq s => s -> Box,
in an equation for `=='
[and more lines...]
----------

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

Yes.

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

Using typeable is a perfectly reasonable way to go.
```_______________________________________________
```
25 May 2013 00:45

### Re: GADT and instance deriving

```Alexander Solla wrote:

>> (Do you confirm that tilde in s~s1 means "s has the same type as s1"? I
>> have
>>
>
> Yes.
>
>
> Is this (Typeable) the right way to go? Is there any other solution?
>>
>
> Using typeable is a perfectly reasonable way to go.

Unfortunately, I am in the following case (in my real code, not the dummy
example of my initial post):

Indeed, I obtain at compilation:

Can't make a derived instance of `Typeable (Tensor (\$a))':
`Tensor' must only have arguments of kind `*'

"Tensor" is a type constructor which takes a type-level integer as argument
to make a concrete type "Tensor order" (so its kind is Nat -> *).
Thus in my real code, I cannot derive the typeable instance automatically. I
am compelled to write an instance of typeable for my GADT. Are there some
tutorial around here? Because the documentation page is a bit terse for my
level of knowledge:

In the first link above, someone writes:

"""
You'll have to manually
write a Typeable instance if you want one.  The process is somewhat
trickier than you might expect, due to the fact that Typeable does
some unsafe stuff.  But there are plenty of examples for how to do it
safely.
"""

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.

Thanks,

TP
```
25 May 2013 10:48

### Re: GADT and instance deriving

```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:

and especially:

"""
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
```
25 May 2013 10:52

### Re: GADT and instance deriving

```Hi TP,

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.

I hope this helps!
Richard

On May 24, 2013, at 11:45 PM, TP wrote:

> Alexander Solla wrote:
>
>>> (Do you confirm that tilde in s~s1 means "s has the same type as s1"? I
>>> have
>>>
>>
>> Yes.
>>
>>
>> Is this (Typeable) the right way to go? Is there any other solution?
>>>
>>
>> Using typeable is a perfectly reasonable way to go.
>
> Unfortunately, I am in the following case (in my real code, not the dummy
> example of my initial post):
>
>
> Indeed, I obtain at compilation:
>
> Can't make a derived instance of `Typeable (Tensor (\$a))':
>      `Tensor' must only have arguments of kind `*'
>
> "Tensor" is a type constructor which takes a type-level integer as argument
> to make a concrete type "Tensor order" (so its kind is Nat -> *).
> Thus in my real code, I cannot derive the typeable instance automatically. I
> am compelled to write an instance of typeable for my GADT. Are there some
> tutorial around here? Because the documentation page is a bit terse for my
> level of knowledge:
>
>
> In the first link above, someone writes:
>
> """
> You'll have to manually
> write a Typeable instance if you want one.  The process is somewhat
> trickier than you might expect, due to the fact that Typeable does
> some unsafe stuff.  But there are plenty of examples for how to do it
> safely.
> """
>
> 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.
>
> Thanks,
>
> TP
>
>
> _______________________________________________
```
25 May 2013 11:23

### Re: GADT and instance deriving

```Hi Richard,

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:

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:
>
> 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.
```
25 May 2013 15:08

### Re: GADT and instance deriving

```Hi,

TP wrote:
> 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.

I don't know what a tensor is, but maybe you have to track *statically*
what independent variables a tensor is a function of, using something like:

E :: R -> T -> Tensor ...

or

E :: Tensor (One -> Zero -> ...)

or

E :: Tensor '[One, Zero] ...

I have two simple pointers to situations where something similar is
going on. First, see the example for type-level lists in the GHC user's
guide:

> data HList :: [*] -> * where
>   HNil  :: HList '[]
>   HCons :: a -> HList t -> HList (a ': t)

In this example, an HList is an heterogenous list, but it doesn't use
existential types. Instead, we know statically what the types of the
list elements are, because we have a type-level list of these element types.

And the second situation: The need for such type-level lists also shows
up when you try to encode well-typed lambda terms as a datatype. You
have to reason about the free variables in the term and their type. For
example, the constructor for lambda expressions should remove one free
variable from the term. You can encode this approximately as follows:

>   data Type = Fun Type Type | Num
>
>   data Term :: [Type] -> Type -> * where
>     -- arithmetics
>     Zero :: Term ctx 'Num
>     Succ :: Term ctx 'Num -> Term ctx 'Num
>     Add :: Term ctx 'Num -> Term ctx 'Num -> Term ctx 'Num
>
>     -- lambda calculus
>     App :: Term ctx ('Fun a b) -> Term ctx a -> Term ctx b
>     Lam :: Term (a ': ctx) b -> Term ctx ('Fun a b)
>     Var :: Var ctx a -> Term ctx a
>
>   -- variables
>   data Var :: [Type] -> Type -> * where
>     This :: Var (a ': ctx) a
>     That :: Var ctx a -> Var (b ': ctx) a

The point is: We know statically what free variables a term can contain,
similarly to how you might want to know statically the independent

Tillmann
```
26 May 2013 14:20

### Re: GADT and instance deriving

```Hi Tillmann and Richard,

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
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.

_______________________________________________
```
27 May 2013 10:30

### Re: GADT and instance deriving

```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:
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.

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.

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,
>
>
> 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.
>
>
> _______________________________________________
>

_______________________________________________
```
25 May 2013 15:11

### Re: GADT and instance deriving

```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

Richard

On May 25, 2013, at 10:23 AM, TP wrote:

> Hi Richard,
>
> We had a discussion about some "Tensor" type some time ago:
>
>
> 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:
>
>
> 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:
>>
>> 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.
>
>
>
> _______________________________________________