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

5 Jun 2013

      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