Re: [Haskell-cafe] Typeable typeclass and type-level naturals
Try adding
deriving instance Typeable 'Zero
deriving instance Typeable a => Typeable ('Succ a)
to your module.
(I haven't tested it — you might need to tweak it a bit.)
Roman
* TP [2013-06-02 18:08:02+0200]
> Hi all,
>
> I try to play with the "Typeable" typeclass, and I have some difficulties to
> make it work in this simple case where I use type-level naturals:
>
> -
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DeriveDataTypeable #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE StandaloneDeriving #-}
>
> import Data.Typeable
>
> data Nat = Zero | Succ Nat
> deriving ( Show, Eq, Ord, Typeable )
>
> data Box where
> Box :: (Typeable s, Show s, Eq s) => s -> Box
> deriving Typeable
>
> data Proxy a = P deriving Typeable
>
> deriving instance Show Box
> instance Eq Box where
>
> (Box s1) == (Box s2) = Just s1 == cast s2
>
> main = do
>
> let one = undefined :: Main.Proxy ('Succ 'Zero)
> let foo = Box one
> print foo
> -
>
> I obtain:
>
> -
> No instance for (Typeable Nat 'Zero) arising from a use of ‛Box’
> In the expression: Box one
> In an equation for ‛foo’: foo = Box one
> In the expression:
> do { let one = ...;
>let foo = Box one;
>print foo }
> -
>
> Note that it is necessary to use the HEAD version of GHC to obtain this
> message (I use version 7.7.20130525); with GHC 7.6.2, the message is
> different because recent improvements in Typeable are not present (1).
>
> What is the problem? I've tried different things without success.
> Tell me if the "beginners" diffusion list is more suitable than Haskell-
> Cafe.
>
> Thanks,
>
> TP
>
>
> (1):
> http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.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
Re: [Haskell-cafe] Typeable typeclass and type-level naturals
Roman Cheplyaka wrote:
> Try adding
>
> deriving instance Typeable 'Zero
> deriving instance Typeable a => Typeable ('Succ a)
>
> to your module.
>
> (I haven't tested it — you might need to tweak it a bit.)
Thanks Roman.
Unfortunately, I already tried that (without the constraint "Typeable a =>",
what a fool), but it did not work. The error is the same with the
constraint:
Derived typeable instance must be of form (Typeable 'Succ)
In the stand-alone deriving instance for
‛Typeable a => Typeable (Succ a)’
What is the problem?
Is it possible that it is a bug in GHC? Indeed, we had unwanted similar
error messages recently:
http://hackage.haskell.org/trac/ghc/ticket/7704
Thanks,
TP
PS: the complete program for a test that shows the error:
--
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
import Data.Typeable
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord, Typeable )
deriving instance Typeable 'Zero
deriving instance Typeable a => Typeable ('Succ a)
data Box where
Box :: (Typeable s, Show s, Eq s) => s -> Box
deriving Typeable
data Proxy a = P deriving Typeable
deriving instance Show Box
instance Eq Box where
(Box s1) == (Box s2) = Just s1 == cast s2
main = do
let one = undefined :: Main.Proxy ('Succ 'Zero)
let foo = Box one
print foo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Typeable typeclass and type-level naturals
* TP [2013-06-05 00:37:36+0200]
> Roman Cheplyaka wrote:
>
> > Try adding
> >
> > deriving instance Typeable 'Zero
> > deriving instance Typeable a => Typeable ('Succ a)
> >
> > to your module.
> >
> > (I haven't tested it — you might need to tweak it a bit.)
>
> Thanks Roman.
> Unfortunately, I already tried that (without the constraint "Typeable a =>",
> what a fool), but it did not work. The error is the same with the
> constraint:
>
> Derived typeable instance must be of form (Typeable 'Succ)
> In the stand-alone deriving instance for
> ‛Typeable a => Typeable (Succ a)’
>
> What is the problem?
Oh, it should probably be simply
deriving instance Typeable 'Zero
deriving instance Typeable 'Succ
Roman
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Typeable typeclass and type-level naturals
On Wed, Jun 5, 2013 at 8:46 AM, Roman Cheplyaka wrote:
> * TP [2013-06-05 00:37:36+0200]
> > Roman Cheplyaka wrote:
> >
> > > Try adding
> > >
> > > deriving instance Typeable 'Zero
> > > deriving instance Typeable a => Typeable ('Succ a)
> > >
> > > to your module.
> > >
> > > (I haven't tested it -- you might need to tweak it a bit.)
> >
> > Thanks Roman.
> > Unfortunately, I already tried that (without the constraint "Typeable a
> =>",
> > what a fool), but it did not work. The error is the same with the
> > constraint:
> >
> > Derived typeable instance must be of form (Typeable 'Succ)
> > In the stand-alone deriving instance for
> > 'Typeable a => Typeable (Succ a)'
> >
> > What is the problem?
>
> Oh, it should probably be simply
>
> deriving instance Typeable 'Zero
> deriving instance Typeable 'Succ
>
Yes, that's how it should be. Please let me know if that
doesn't work.
(Sorry for taking so long to reply to this...)
Cheers,
Pedro
>
> Roman
>
> ___
> 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] Typeable typeclass and type-level naturals
José Pedro Magalhães wrote:
>> Oh, it should probably be simply
>>
>> deriving instance Typeable 'Zero
>> deriving instance Typeable 'Succ
>>
>
> Yes, that's how it should be. Please let me know if that
> doesn't work.
Thanks, it works perfectly like that.
I don't understand exactly why the previous syntax did not work, but maybe
it will be clearer when I finish the paper "Scrap your boilerplate: a
practical design pattern for generic programming" (anyway, this paper seems
very interesting).
Output of the code:
-
$ runghc-head test_typeable.hs
Box test_typeable.hs: Prelude.undefined
-
Maybe the "Box " in front of the line is strange, but it is OK: "one" is
undefined, not "Box one".
This is the full tested code, for sake of reference:
---
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
import Data.Typeable
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )
deriving instance Typeable 'Zero
deriving instance Typeable 'Succ
data Box where
Box :: (Typeable s, Show s, Eq s) => s -> Box
deriving Typeable
data Proxy a = P deriving (Typeable, Show, Eq)
deriving instance Show Box
instance Eq Box where
(Box s1) == (Box s2) = Just s1 == cast s2
main = do
let one = undefined :: Main.Proxy ('Succ 'Zero)
let foo = Box one
print foo
--
Thanks a lot,
TP
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Typeable typeclass and type-level naturals
Hi,
On Wed, Jun 5, 2013 at 11:21 PM, TP wrote:
> José Pedro Magalhães wrote:
>
> >> Oh, it should probably be simply
> >>
> >> deriving instance Typeable 'Zero
> >> deriving instance Typeable 'Succ
> >>
> >
> > Yes, that's how it should be. Please let me know if that
> > doesn't work.
>
> Thanks, it works perfectly like that.
> I don't understand exactly why the previous syntax did not work, but maybe
> it will be clearer when I finish the paper "Scrap your boilerplate: a
> practical design pattern for generic programming" (anyway, this paper seems
> very interesting).
>
It's an interesting paper, but I'm afraid it won't help you understand
what's going
on. Typeable is changing in GHC 7.8 to become poly-kinded. You are using
Typeable instances for things which are not of kind *, so you need this new
poly-kinded variant. The SYB paper says nothing about polykinds (it was
written
way before polykinds came up).
You can find some more information on the new Typeable here:
http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable
By the way, you can also get those Typeable instances derived automatically
if you use the LANGUAGE pragma AutoDeriveTypeable. This is also documented
in the HEAD user's guide.
Cheers,
Pedro
> Output of the code:
>
> -
> $ runghc-head test_typeable.hs
> Box test_typeable.hs: Prelude.undefined
> -
>
> Maybe the "Box " in front of the line is strange, but it is OK: "one" is
> undefined, not "Box one".
>
> This is the full tested code, for sake of reference:
>
> ---
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DeriveDataTypeable #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE StandaloneDeriving #-}
>
> import Data.Typeable
>
> data Nat = Zero | Succ Nat
> deriving ( Show, Eq, Ord )
>
> deriving instance Typeable 'Zero
> deriving instance Typeable 'Succ
>
> data Box where
> Box :: (Typeable s, Show s, Eq s) => s -> Box
> deriving Typeable
>
> data Proxy a = P deriving (Typeable, Show, Eq)
>
> deriving instance Show Box
> instance Eq Box where
>
> (Box s1) == (Box s2) = Just s1 == cast s2
>
> main = do
>
> let one = undefined :: Main.Proxy ('Succ 'Zero)
> let foo = Box one
> print foo
> --
>
> Thanks a lot,
>
> 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
