10

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?

Community
  • 1
  • 1
Alessandro Vermeulen
  • 1,321
  • 1
  • 9
  • 28

2 Answers2

15

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.

Ganesh Sittampalam
  • 28,821
  • 4
  • 79
  • 98
  • 1
    In ghc 7.8 every type will have a typeable instance automatically derived by the compiler, so that obstacle will no longer apply. In fact I believe that feature is in the current 7.7 HEAD so the restriction no longer applies to those Willing to brave building ghc from source – Carter Tazio Schonwald Mar 30 '13 at 18:22
  • 4
    But even in GHC 7.8 no information whatsoever will be available for an existential type. – kosmikus Mar 30 '13 at 18:59
  • 3
    For the new feature in GHC 7.8, it's important that although every concrete type would be Typeable, you wouldn't be able to assume Typeable for a /polymorphic/ variable - so for example the only total function of type (a -> a) would still have to be the identity function. Otherwise we'd lose parametricity. It does make my specific counter-argument invalid, though. – Ganesh Sittampalam Mar 30 '13 at 21:37
3

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.)

dave4420
  • 46,404
  • 6
  • 118
  • 152