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?

Answer 1

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.

Answer 2

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.

Perhaps you should resort to {-# LANGUAGE RebindableSyntax #-} (while noting that it implies NoImplicitPrelude). Create your own arr, (>>>), first, app, (|||) and loop functions and GHC will use them when desugaring arrow notation, instead of the standard versions from Control.Arrow.

The manual states that “the types of these functions must match the Prelude types very closely”. If you're building a parallel class hierarchy (a copy of the hierarchy in Control.Arrow but with Typeable constraints added to the type signatures) you should be fine.

(n.b. I am not familiar with arrow notation so have never used it in conjunction with RebindableSyntax; my answer is an intelligent guess.)