[Haskell-cafe] Typeable typeclass and type-level naturals
TP
paratribulations at free.fr
Thu Jun 6 00:21:48 CEST 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
More information about the Haskell-Cafe
mailing list