[Haskell-cafe] Typeable typeclass and type-level naturals

[José Pedro Magalhães]

Hi,

On Wed, Jun 5, 2013 at 11:21 PM, TP <paratribulations at free.fr> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130606/dc18faf5/attachment-0001.htm>