Transform a GADT without constraints to another GADT with constraints when such constraints hold

Question

Can we transform a GADT without a given constraint on its constructors to a GADT that does have the said constraint? I want to do this because I want to get a deep-embedding of Arrows and do some interesting things with the representation that (for now) seem to require Typeable. (One reason)

data DSL a b where
  Id   :: DSL a a
  Comp :: DSL b c -> DSL a b -> DSL a c
  -- Other constructors for Arrow(Loop,Apply,etc)

data DSL2 a b where
  Id2   :: (Typeable a, Typeable b)             => DSL2 a a
  Comp2 :: (Typeable a, Typeable b, Typeable c) => DSL2 b c -> DSL2 a b -> DSL2 a c
  -- ...

We could try the following from function but that breaks quickly as we don't have the Typeable information for the recursive point

from :: (Typeable a, Typeable b) =>  DSL a b -> DSL2 a b
from (Id)       = Id2
from (Comp g f) = Comp2 (from g) (from f)

So instead we try to capture the transformation in a type class. However, that will break as well as we will be missing the Typeable b information as b is an existential.

class From a b where
  from :: a -> b

instance (Typeable a, Typeable b) => From (DSL a b) (DSL2 a b) where
  from (Id)       = Id2
  from (Comp g f) = Comp2 (from g) (from f)

Any other suggestions? Ultimately I want to create a deep-embedding of Category and Arrow together with Typeable information on the type parameters. This is so I can use the arrow-syntax to construct a value in my DSL and have fairly standard Haskell code. Maybe I have to resort to Template Haskell?

GS - Apologise to Monica GS - Apologise to Monica · Accepted Answer · 2013-03-30T10:31:19

The problem with the recursive case is fatal to transforming DSL a b into DSL2 a b.

To do this transformation would require finding the Typeable dictionary for the existential type b in the Comp case - but what b actually is has already been forgotten.

For example consider the following program:

data X = X Int
-- No Typeable instance for X

dsl1 :: DSL X Char
dsl1 = -- DSL needs to have some way to make non-identity terms,
       -- use whatever mechanism it offers for this.

dsl2 :: DSL Int X
dsl2 = -- DSL needs to have some way to make non-identity terms,
       -- use whatever mechanism it offers for this.

v :: DSL Int Char
v = Comp dsl1 dsl2

v2 :: DSL2 Int Char
v2 = -- made by converting v from DSL to DSL2, note that Int and Char are Typeable

typeOfIntermediate :: DSL a c -> TypeRep
typeOfIntermediate int =
    case int of
        Comp (bc :: DSL2 b c) (ab :: DSL2 a b) ->
            typeOf (undefined :: b)

typeOfX = typeOfIntermediate v2

In other words if there was a way to do the conversion in general, you could somehow invent a Typeable instance for a type that doesn't actually have one.

Transform a GADT without constraints to another GADT with constraints when such constraints hold

2 Answers