Re: [Haskell-cafe] GADT and instance deriving

[Richard Eisenberg]

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

Re: [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.


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

Re: [Haskell-cafe] GADT and instance deriving

[TP]

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-data-dot-dynamic-in-haskell/

and especially:

http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.html


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


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

Re: [Haskell-cafe] GADT and instance deriving

[Richard Eisenberg]

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
 not found this information explicitly in the Haskell stuff I have read).
 
 
 Yes.
 
 http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.html
 
 Is this (Typeable) the right way to go? Is there any other solution?
 
 
 Using typeable is a perfectly reasonable way to go.
 
 Thanks for your help.
 Unfortunately, I am in the following case (in my real code, not the dummy 
 example of my initial post):
 
 http://haskell.1045720.n5.nabble.com/Can-t-make-a-derived-instance-of-Typeable-A-B-A-has-arguments-of-kind-other-than-td3121994.html
 
 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:
 
 http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Typeable.html
 
 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
 
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


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

Re: [Haskell-cafe] GADT and instance deriving

[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:_heterogeneous_lists

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

Re: [Haskell-cafe] GADT and instance deriving

[Tillmann Rendel]

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:


http://www.haskell.org/ghc/docs/latest/html/users_guide/promotion.html#promoted-lists-and-tuples


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 
variables of your tensor.


  Tillmann

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

Re: [Haskell-cafe] GADT and instance deriving

[Richard Eisenberg]

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

Re: [Haskell-cafe] GADT and instance deriving

[Niklas Hambüchen]

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

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

Re: [Haskell-cafe] GADT and instance deriving

[Alexander Solla]

On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen m...@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 Eqs 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.html

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).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[Alexander Solla]

On Fri, May 24, 2013 at 9:37 AM, TP paratribulati...@free.fr 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:

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

 --
 {-# LANGUAGE GADTs #-}

 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 `=='
   at test_eq_GADT_before.hs:8:6-11
 [and more lines...]
 --

 (Do you confirm that tilde in s~s1 means s has the same type as s1? I
 have
 not found this information explicitly in the Haskell stuff I have read).


Yes.

http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.html

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


Using typeable is a perfectly reasonable way to go.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[TP]

Alexander Solla wrote:

 (Do you confirm that tilde in s~s1 means s has the same type as s1? I
 have
 not found this information explicitly in the Haskell stuff I have read).

 
 Yes.
 
 http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.html
 
 Is this (Typeable) the right way to go? Is there any other solution?

 
 Using typeable is a perfectly reasonable way to go.

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

http://haskell.1045720.n5.nabble.com/Can-t-make-a-derived-instance-of-Typeable-A-B-A-has-arguments-of-kind-other-than-td3121994.html

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:

http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Typeable.html

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


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

Re: [Haskell-cafe] GADT and instance deriving

[Niklas Hambüchen]

On 25/05/13 06:06, Alexander Solla wrote:
 On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen m...@nh2.me
 mailto:m...@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 Eqs 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.html
  
 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.

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