[Haskell-cafe] reifying typeclasses

[Emil Axelsson]

2013-09-15 11:16, oleg at okmij.org skrev:
> Evan Laforge wrote:
>> 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.:
>
> If the universe (the set of types of interest to instantiate the type
> class to) is closed, GADTs spring to mind immediately. See, for
> example, the enclosed code. It is totally unproblematic (one should
> remember to always write type signatures when programming with
> GADTs. Weird error messages otherwise ensue.)
>
> One of the most notable differences between GADT and type-class--based
> programming is that GADTs are closed and type classes are open (that
> is, new instances can be added at will). In fact, a less popular
> technique of implementing type classes (which has been used in some Haskell
> systems -- but not GHC)) is intensional type analysis, or typecase.
> It is quite similar to the GADT solution.

I've been toying with using Data Types à la Carte to get type 
representations, a `Typeable` class and dynamic types parameterized by a 
possibly open universe:

   https://github.com/emilaxelsson/dsl-factory/blob/master/TypeReify.hs

Using this module (which depends on the syntactic package), Evan's 
problem can be solved easily without setting up any new classes or data 
types, as shown below.

/ Emil



import Language.Syntactic
import TypeReify

type Universe = IntType :+: CharType

argument :: forall a . Typeable Universe a => a -> Int
argument a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = fromEnum a
         -- Note: All cases are covered, since `Universe` is closed
   where
     TypeRep t = typeRep :: TypeRep Universe a

result :: forall a . Typeable Universe a => Int -> a
result a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = toEnum a
         -- Note: All cases are covered, since `Universe` is closed
   where
     TypeRep t = typeRep :: TypeRep Universe a

-- Note that we do not have to use a closed universe. Here's an alternative,
-- open version of `argument`:
argument' :: forall u a . (IntType :<: u, CharType :<: u) =>
              Typeable u a => a -> Int
argument' a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = fromEnum a
     | otherwise              = 0  -- or whatever :)
   where
     TypeRep t = typeRep :: TypeRep u a