[Haskell-cafe] Cabal config file Guide
Hello Cafe! As you already know, cabal-install is configured in the file "config". It has a lot of fields, but I didn't find a single place where each field is explained with detail. Most of the options are trivial enough to understand what they do without previous explanation, but some of them aren't. Therefore, in order to know what these options do, you have to search info about that one specifically, when it would be much more convenient to have all the information together. So, is there any place like this out there in the web? Thank you, Daniel Díaz. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 existenti
Re: [Haskell-cafe] 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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@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 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
