当这些约束成立时,将没有约束的GADT转换为具有约束的另一个GADT

Question

我们可以将没有给定约束的GADT转换为具有上述约束的GADT吗？我想这样做是因为我希望深入嵌入Arrows并使用(现在)似乎需要的表示来做一些有趣的事情Typeable.(一个原因)

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

我们可以尝试以下from函数但由于我们没有Typeable递归点的信息而快速中断

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

因此,我们尝试捕获类型类中的转换.然而,这将打破,我们将错过Typeable b信息,因为b是一个存在主义.

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)

还有其他建议吗？最后,我想创建的深嵌入Category并Arrow连同Typeable该类型参数的信息.这样我就可以使用arrow-syntax在我的DSL中构造一个值,并拥有相当标准的Haskell代码.也许我不得不求助于模板Haskell？

Answer 1

使用递归情况下的问题是致命的转化DSL a b成DSL2 a b.

要做到这一点,转换需要在案例中找到Typeable存在类型的字典- 但实际上已经忘记了.bCompb

例如,考虑以下程序:

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

换句话说,如果有一种方法可以进行一般的转换,你可以某种方式Typeable为一个实际上没有一个的类型发明一个实例.