[Haskell-cafe] reifying typeclasses (resend)

[Timon Gehr]

On 09/15/2013 09:38 AM, Evan Laforge wrote:
> ...
>
> It seems to me like I should be able to replace a typeclass with
> arbitrary methods with just two, to reify the type and back.  This
> seems to work when the typeclass dispatches on an argument, but not on
> a return value.  E.g.:
>
> ...
>
> Say m_argument and m_result are the ad-hoc methods  I'd like to get out
> of the typeclass.  I can do that well enough for 'argument', but
> 'result' runs into trouble.  One is the ugly undefined trick with
> toTaggedType, but the bigger one is that ghc says 'Could not deduce (a
> ~ Int) from the context (Taggable a)'.  I wasn't really expecting it
> to work, because it would entail a case with multiple types.  As far
> as I know, the only way for that to happen is with GADTs.  But I don't
> see how they could help me here.
>

As follows:

{-# LANGUAGE GADTs, StandaloneDeriving #-}

class Taggable a where
     toTagged :: a -> Tagged a
     toTaggedType :: TaggedType a
     fromTagged :: Tagged b -> Maybe a

data Tagged a where -- (example works if this is not a GADT)
   TInt  :: Int -> Tagged Int
   TChar :: Char -> Tagged Char

deriving instance Show (Tagged a)

data TaggedType a where
   TypeInt :: TaggedType Int
   TypeChar :: TaggedType Char

deriving instance Show (TaggedType a)

instance Taggable Int where
     toTagged = TInt
     toTaggedType = TypeInt
     fromTagged (TInt x) = Just x
     fromTagged _ = Nothing

instance Taggable Char where
     toTagged = TChar
     toTaggedType = TypeChar
     fromTagged (TChar x) = Just x
     fromTagged _ = Nothing

argument :: (Taggable a) => a -> Int
argument a = case toTagged a of
     TInt x -> x
     TChar c -> fromEnum c

result :: (Taggable a) => Int -> a
result val = go val $ toTaggedType
   where
     go :: (Taggable a) => Int -> TaggedType a -> a
     go val TypeInt = val
     go val TypeChar = toEnum val


> So, perhaps my intuition was wrong.  toTagged and fromTagged methods
> give you the power to go between value and type level,  but apparently
> that's not enough power to express what typeclasses give you.

You do get enough power to write that second function, but the result is 
necessarily uglier than if you use GADTs as there are less invariants 
expressed in the type system.

result :: (Taggable a) => Int -> a
result val = case fromTagged (TInt val) of
   Just a -> a
   Nothing -> case fromTagged (TChar $ toEnum val) of
     Just a -> a
     Nothing -> case error "matches are non-exhaustive" of
       TInt _ -> undefined
       TChar _ -> undefined

(The last pattern match allows the compiler to warn you if 'result' gets 
out of sync with 'Tagged'.)