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 "

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

[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 existenti

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

[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

[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]

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

[Niklas Hambüchen]

On 25/05/13 06:06, Alexander Solla wrote:
> 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.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

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

[Alexander Solla]

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

[Alexander Solla]

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

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

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

[Haskell-cafe] GADT and instance deriving

[TP]

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

I have googled on the topic, and found:
http://stackoverflow.com/questions/6028424/defining-eq-instance-for-haskell-gadts
>From the proposed solution, I wrote:

--
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}

import Data.Typeable

data Box where
Box :: (Typeable s, Eq s) => s -> Box
deriving Typeable

instance Eq Box where

(Box s1) == (Box s2) = Just s1 == cast s2
--

that seems to work correctly:
--
let a = Box (2::Int)
let b = Box (2::Float)

print $ a == b
print $ a == a
--

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

Thanks,

TP


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