TP | 24 May 18:37 2013
Picon

GADT and instance deriving

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...]
(Continue reading)

Niklas Hambüchen | 24 May 19:41 2013

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.
Alexander Solla | 25 May 00:06 2013
Picon

Re: GADT and instance deriving




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

(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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Niklas Hambüchen | 25 May 06:08 2013

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".
> 
> 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.
Alexander Solla | 25 May 00:09 2013
Picon

Re: GADT and instance deriving




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


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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 25 May 00:45 2013
Picon

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
>> 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
TP | 25 May 10:48 2013
Picon

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:

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
Richard Eisenberg | 25 May 10:52 2013

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
>>> 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 25 May 11:23 2013
Picon

Re: GADT and instance deriving

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.
Tillmann Rendel | 25 May 15:08 2013
Picon

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:

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
TP | 26 May 14:20 2013
Picon

Re: GADT and instance deriving

Hi Tillmann and Richard,

Thanks for your answers.

I have tried to analyze the code snippets you proposed.
I've tried to transpose your examples to what I need, but it is not easy.

The problem I see with putting the list of independent variables (*) at the 
type level is that at some time in my code I want for instance to perform 
formal mathematical operations, for example I want a function "deriv" that 
takes f(x(t),y(t),z(t)) as input, and returns

df/dt = ∂f/∂x*dx/dt + ∂f/∂y*dy/dt + ∂f/∂z*dz/dt

If the list of dependencies is encoded at the type level, I don't see how to 
produce the previous output from the knowledge of "f(x(t),y(t),z(t))". You 
understand that what I want to do is some type of basic Computer Algebra 
System library.

Moreover, I want overloading for infix functions as '*', '/', '⋅' (scalar 
product), × (vector product) etc., that is why I have used typeclasses (see 
the code I showed in my previous post). For example, for the time being I 
will restrict myself to scalar product between vector and vector, vector and 
dyadic, dyadic and vector (a dyadic is a tensor of order 2, a matrix if you 
prefer). So I have three instances for scalar product '⋅'. I don't see how 
to combine this idea of overloading or derivation function with what you 
proposed. But I have perhaps missed something.

Thanks,

TP

(*): That is to say the list of tensors of which one tensor depends, e.g. 
[t,r] for E(t,r), or simply [x,y,z] for f(x(t),y(t),z(t)) where x, y, and z 
themselves are scalars depending on a scalar t). In the test file of my 
library, my code currently looks like:

-----------------
type Scalar = Tensor Zero
type Vector = Tensor One
[...]
let s = (t "s" []) :: Scalar
let v = (t "v" [i s]) :: Vector
let c1 = v + v
let c2 = s + v⋅v
-----------------

t is a smart constructor taking a string str and a list of independent 
variables, and makes a (Tensor order) of name str.

So in the example above, s is a scalar that depends on nothing (thus it is 
an independent variable), v is a vector that depends on s (i is a smart 
constructor that wraps s into a Box constructor, such that I can put all 
independent variables in an heterogeneous list).
c1 is the sum of v and v, i.e. is equal to 2*v.
c2 is the sum of s and v scalar v.
If I try to write:

let c3 = s + v

I will obtain a compilation error, because adding a scalar and a vector has 
no meaning.

Is there some way to avoid typeable in my case?

Moreover, if I wanted to avoid the String in the first argument of my smart 
constructor "t", such that

let s = (t []) :: Scalar

constructs an independent Scalar of name "s", googling on the topic seems to 
indicated that I am compelled to use "Template Haskell" (I don't know it at 
all, and this is not my priority).
Thus, in a general way, it seems to me that I am compelled to use some 
"meta" features as typeable or Template Haskell to obtain exactly the result 
I need while taking benefit from a maximum amount of static type checking.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 27 May 10:30 2013

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:
http://www.haskell.org/haskellwiki/GHC/Type_families    Once upon a time, I earned a degree in physics
and have actually taught multivariable calculus, but those days are long gone and my memory pages giving
the exact definitions you need are buried under many more pages of type theory. Nevertheless, I'm sure
that the types you need should be easily derivable given the inputs. Using type families in this way is
often necessary when using GADTs and strongly-typed interfaces.

Overloading operators should be possible using type classes. For example:

instance Addable (Tensor n) (Tensor n) where
  (+) = …

You can use functional dependencies *or* type families/associated types (type families and associated
types are almost two names for the same thing) for the output type. I prefer type families over functional
dependencies, because I think type families use a syntax like function application and I find them easier
to think about. But, either will work for you here.

As for your question whose answer was "Template Haskell", I have to agree with that answer. Haskell gives
you no direct access to the names of your variables, so you can't have any decisions made based on a variable
name. So, if you want your names to be significant, you have to use Template Haskell, which involves
essentially writing programs to produce Haskell code. In your case, though, I think that approach is
overkill, and it's probably best just to be a little redundant in your code (i.e. name a variable `s` and
have a string `"s"` nearby).

I hope this helps!
Richard

On May 26, 2013, at 1:20 PM, TP wrote:

> Hi Tillmann and Richard,
> 
> Thanks for your answers.
> 
> I have tried to analyze the code snippets you proposed.
> I've tried to transpose your examples to what I need, but it is not easy.
> 
> The problem I see with putting the list of independent variables (*) at the 
> type level is that at some time in my code I want for instance to perform 
> formal mathematical operations, for example I want a function "deriv" that 
> takes f(x(t),y(t),z(t)) as input, and returns
> 
> df/dt = ∂f/∂x*dx/dt + ∂f/∂y*dy/dt + ∂f/∂z*dz/dt
> 
> If the list of dependencies is encoded at the type level, I don't see how to 
> produce the previous output from the knowledge of "f(x(t),y(t),z(t))". You 
> understand that what I want to do is some type of basic Computer Algebra 
> System library.
> 
> Moreover, I want overloading for infix functions as '*', '/', '⋅' (scalar 
> product), × (vector product) etc., that is why I have used typeclasses (see 
> the code I showed in my previous post). For example, for the time being I 
> will restrict myself to scalar product between vector and vector, vector and 
> dyadic, dyadic and vector (a dyadic is a tensor of order 2, a matrix if you 
> prefer). So I have three instances for scalar product '⋅'. I don't see how 
> to combine this idea of overloading or derivation function with what you 
> proposed. But I have perhaps missed something.
> 
> Thanks,
> 
> TP
> 
> (*): That is to say the list of tensors of which one tensor depends, e.g. 
> [t,r] for E(t,r), or simply [x,y,z] for f(x(t),y(t),z(t)) where x, y, and z 
> themselves are scalars depending on a scalar t). In the test file of my 
> library, my code currently looks like:
> 
> -----------------
> type Scalar = Tensor Zero
> type Vector = Tensor One
> [...]
> let s = (t "s" []) :: Scalar
> let v = (t "v" [i s]) :: Vector
> let c1 = v + v
> let c2 = s + v⋅v
> -----------------
> 
> t is a smart constructor taking a string str and a list of independent 
> variables, and makes a (Tensor order) of name str.
> 
> So in the example above, s is a scalar that depends on nothing (thus it is 
> an independent variable), v is a vector that depends on s (i is a smart 
> constructor that wraps s into a Box constructor, such that I can put all 
> independent variables in an heterogeneous list).
> c1 is the sum of v and v, i.e. is equal to 2*v.
> c2 is the sum of s and v scalar v.
> If I try to write:
> 
> let c3 = s + v
> 
> I will obtain a compilation error, because adding a scalar and a vector has 
> no meaning.
> 
> Is there some way to avoid typeable in my case?
> 
> Moreover, if I wanted to avoid the String in the first argument of my smart 
> constructor "t", such that
> 
> let s = (t []) :: Scalar
> 
> constructs an independent Scalar of name "s", googling on the topic seems to 
> indicated that I am compelled to use "Template Haskell" (I don't know it at 
> all, and this is not my priority).
> Thus, in a general way, it seems to me that I am compelled to use some 
> "meta" features as typeable or Template Haskell to obtain exactly the result 
> I need while taking benefit from a maximum amount of static type checking.
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 25 May 15:11 2013

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
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 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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane