[Haskell-cafe] type-level integers for GHC
What is your recommendation for type-level integers? I'd like to use it to improve the unittyped, https://bitbucket.org/xnyhps/haskell-unittyped/ the library for physical dimension. Therefore, I need negative numbers, additions, but multiplications are not necessary. I've been looking forward for the type-nats extension of GHC, but I haven't been able to compile the type-nats branch. Just learned that it still takes a few month to merge the branch into the main. http://hackage.haskell.org/trac/ghc/wiki/Status/May13 Thijs, the original author of unittyped, has commited a branch that uses type-nats, but I can't try that out for the same reason. Best, -- Takayuki MURANUSHI The Hakubi Center for Advanced Research, Kyoto University http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-level integers for GHC
I wonder why you can't compile type-nats? It should just work. You could email ghc-devs and Iavor (type-nats author, cc'd) explaining exactly what goes wrong. You may need the type-nats branch of some libraries, I'm not sure Simon Microsoft Research Limited (company number 03369488) is registered in England and Wales Registered office 21 Station Road, Cambridge, CB1 2FB | -Original Message- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe- | boun...@haskell.org] On Behalf Of Takayuki Muranushi | Sent: 17 May 2013 07:18 | To: haskell | Subject: [Haskell-cafe] type-level integers for GHC | | What is your recommendation for type-level integers? | | I'd like to use it to improve the unittyped, | https://bitbucket.org/xnyhps/haskell-unittyped/ the library for physical | dimension. Therefore, I need negative numbers, additions, but | multiplications are not necessary. | | I've been looking forward for the type-nats extension of GHC, but I | haven't been able to compile the type-nats branch. Just learned that it | still takes a few month to merge the branch into the main. | http://hackage.haskell.org/trac/ghc/wiki/Status/May13 | | Thijs, the original author of unittyped, has commited a branch that uses | type-nats, but I can't try that out for the same reason. | | | Best, | -- | Takayuki MURANUSHI | The Hakubi Center for Advanced Research, Kyoto University | http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html | | ___ | 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
[Haskell-cafe] question about GADT and deriving automatically a Show instance
Hi everybody,
I have a question about deriving automatically a Show instance when using
GADT.
It works in this situation:
{-# LANGUAGE GADTs #-}
data Male
data Female
data Person gender where
Dead :: Person gender
Alive :: { name :: String
, weight :: Float
, father :: Person gender } - Person gender
deriving Show
main = do
let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male
print a
print b
Indeed:
$ runghc test_show.hs
Alive {name = Joe, weight = 60.0, father = Dead}
Alive {name = Jim, weight = 70.0, father = Alive {name = Joe, weight =
60.0, father = Dead}}
But when I replace father :: Person gender by father :: Person gender2
in the code (this is one of the advantages of GADT: with a classical
algebraic data type declaration, gender2 would have to be a type variable
for the data type), I obtain:
Can't make a derived instance of `Show (Person gender)':
Constructor `Alive' must have a Haskell-98 type
Possible fix: use a standalone deriving declaration instead
In the data declaration for `Person'
So I modify my code by removing deriving Show, and adding the line:
instance Show (Person gender)
But now, I obtain:
$ runghc test_show.hs
GHC stack-space overflow: current limit is 536870912 bytes.
Use the `-Ksize' option to increase it.
Why (I imagine this is because there is an infinite loop in the construction
of the show function)? Is there any workaround?
Thanks,
TP
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance
Hi TP, On 17/05/13 15:32, TP wrote: | [...] | | So I modify my code by removing deriving Show, and adding the line: | | instance Show (Person gender) | | | But now, I obtain: | | $ runghc test_show.hs | GHC stack-space overflow: current limit is 536870912 bytes. | Use the `-Ksize' option to increase it. | | Why (I imagine this is because there is an infinite loop in the construction | of the show function)? Is there any workaround? To use standalone deriving, you need to write deriving instance Show (Person gender) and everything will work fine. By writing instance Show (Person gender) you are instead giving an instance with no methods, and the default methods in the Show class contain a loop (so that one can define either show or showsPrec). Hope this helps, Adam P.S. You might like to check out the new DataKinds extension, which would allow Male and Female to be data constructors rather than type constructors. -- The University of Strathclyde is a charitable body, registered in Scotland, with registration number SC015263. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
Hi, Patrick Browne wrote: In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. Yes. Haskell function definitions look like equations, but in many ways, they aren't. Here is an example for an equation that is not valid as a Haskell function definition: g x = 42 f (g x) = x-- not valid The problem is that we cannot use g at the left-hand side. Here is an example that doesn't mean what you might be hoping for: f x = f x f x = 42 Seen as an equation system, this should constrain f to be a function that always returns 42. But in Haskell, it defines f to be a non-terminating function. The reason is that only the first line counts, because it covers all possible argument values. The second line is ignored. The behavior changes if we swap the two lines: g x = 42 g x = g x Again, only the first line counts, so g is the function that always returns 42. Here is a more complicated example: h 27 = 42 h x = h x h 13 = 100 What function is h? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance
Adam Gundry wrote:
[...]
To use standalone deriving, you need to write
deriving instance Show (Person gender)
and everything will work fine. By writing
instance Show (Person gender)
you are instead giving an instance with no methods, and the default
methods in the Show class contain a loop (so that one can define either
show or showsPrec).
Thanks a lot. I did not remember that Standalone Deriving has a meaning as
a GHC extension. My idea was correct, but the employed syntax was incorrect.
Just for reference (future Google search by others), the corresponding link
in the GHC documentation:
http://www.haskell.org/ghc/docs/7.6.2/html/users_guide/deriving.html
P.S. You might like to check out the new DataKinds extension, which
would allow Male and Female to be data constructors rather than type
constructors.
Thanks a lot for pointing out this subject (it compells me to work on it - I
am not an advanced user of GHC).
I have just tried to understand all this stuff about type and data
constructor promotion:
http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/promotion.html
If I understand well, your idea is to avoid letting someone write:
let a = Alive Joe 60 Dead :: Person Int
which is nonsense (a Person cannot have a gender of type Integer), but
legal code.
I have tried to use the technique described at the beginning of the article
Given Haskell a Promotion, but I'm stuck. See the code below. My problem
is that now Gender is a kind, no more a type, such that I cannot use it in
the type definition of the GADT; but I am compelled to write something after
::, and I cannot write for instance Dead :: Person Male because I want a
dead person to be either a man or woman, of course. In fact, what I need is
Gender both as a type and as a kind, if I am correct? What do I miss?
So the following version does not work:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
data Gender = Male | Female
data Person :: Gender - * where
Dead :: Person Gender -- WHAT DO I PUT HERE
Alive :: { name :: String
, weight :: Float
, father :: Person Gender } - Person Gender
deriving instance Show (Person Gender)
main = do
let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male
print a
print b
How to modify it?
Thanks a lot,
TP
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance
On Sat, May 18, 2013 at 9:11 AM, TP paratribulati...@free.fr wrote:
So the following version does not work:
[..]
data Person :: Gender - * where
Dead :: Person Gender -- WHAT DO I PUT HERE
Alive :: { name :: String
, weight :: Float
, father :: Person Gender } - Person Gender
Here's the problem. In the line:
Dead :: Person Gender
you are referring to the Gender *type*, not the Gender kind.
To refer to the kind instead, change this to:
Dead :: forall (a :: Gender). Person a
This means for all types A which have the kind Gender, I can give you
a Person with that type. The Alive declaration and deriving clause
can be fixed in a similar way.
Also, to enable the forall syntax, you need to add
{-# LANGUAGE ExplicitForAll #-}
at the top of the file.
Chris
--
Chris Wong, fixpoint conjurer
e: lambda.fa...@gmail.com
w: http://lfairy.github.io/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
