[Haskell-cafe] reifying typeclasses (resend)

[Bas van Dijk]

You can indeed use GADTs to solve this:

{-# LANGUAGE GADTs #-}

data Universe a where
    UInt  :: Int  -> Universe Int
    UChar :: Char -> Universe Char

class Universal a where
    universe :: a -> Universe a

instance Universal Int where
    universe = UInt

instance Universal Char where
    universe = UChar

argument :: (Universal a) => a -> Int
argument x = case universe x of
               UInt  n -> n
               UChar c -> fromEnum c

result :: (Universal a) => Int -> a
result val = x
  where
    x = case universe x of
          UInt  _ -> val
          UChar _ -> toEnum val

On 15 September 2013 09:38, Evan Laforge <qdunkan at gmail.com> wrote:
> [ This is the second time I sent this, the first time it said it was
> awaiting moderation because I'm not subscribed to haskell-cafe, which
> is weird because I thought I was.  Did a bunch of people get
> unsubscribed? ]
>
> I'm sure this is old-hat to typeclass wizards, but I've managed to get
> pretty far without understanding them too well, so here's a basic
> question.  I haven't seen it phrased this way before though:
>
> I have a typeclass which is instantiated across a closed set of 3
> types.  It has an ad-hoc set of methods, and I'm not too happy with
> them because being a typeclass forces them to all be defined in one
> place, breaking modularity.  A sum type, of course, wouldn't have that
> problem.  But in other places I want the type-safety that separate
> types provide, and packing everything into a sum type would destroy
> that.  So, expression problem-like, I guess.
>
> 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.:
>
> {-# LANGUAGE ScopedTypeVariables #-}
>
> class Taggable a where
>     toTagged :: a -> Tagged
>     toTaggedType :: a -> TaggedType
>     fromTagged :: Tagged -> Maybe a
>
>     m_argument :: a -> Int
>     m_result :: Int -> a
>
> data Tagged = TInt Int | TChar Char deriving (Show)
> data TaggedType = TypeInt | TypeChar deriving (Show)
>
> instance Taggable Int where
>     toTagged = TInt
>     toTaggedType _ = TypeInt
>     fromTagged (TInt x) = Just x
>     fromTagged _ = Nothing
>
>     m_argument = id
>     m_result = id
>
> instance Taggable Char where
>     toTagged = TChar
>     toTaggedType _ = TypeChar
>     fromTagged (TChar x) = Just x
>     fromTagged _ = Nothing
>
>     m_argument = fromEnum
>     m_result = toEnum
>
> argument :: (Taggable a) => a -> Int
> argument a = case toTagged a of
>     TInt x -> x
>     TChar c -> fromEnum c
>
> result :: forall a. (Taggable a) => Int -> a
> result val = case toTaggedType (undefined :: a) of
>     TypeInt -> val
>     TypeChar -> toEnum val
>
>
> 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.
>
> 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.  Also it
> seems like there's a fundamental difference between dispatching on
> argument vs dispatching on result.
>
> Is there a way to more formally understand the extents of what
> typeclasses provide, and what a toTagged fromTagged scheme gives me,
> so I can have a better intuition for how to go between value and type
> levels?
>
> Also, the toTaggedType thing is pretty ugly.  Not just passing it
> undefined, but how it has to repeat the types.  I don't really see a
> way to get around that though.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe