变换GADT没有约束到另一个GADT与约束了这些约束举行(Transform a GADT with

我们可以将不会对其构造一个给定的约束，它有上述约束GADT一个GADT？我想这样做，因为我想获得的箭深嵌入和做一些有趣的事情表示是（现在）似乎需要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的类型参数信息。这是这样我就可以用箭头语法来构建我的DSL的值，并有相当标准的Haskell代码。也许我不得不求助于模板哈斯克尔？

Answer 1:

使用递归情况下的问题是致命的转化DSL ab成DSL2 ab 。

要做到这一点转变将需要找到Typeable词典的生存型b在Comp的情况下-但b实际上是已经被遗忘了。

例如，考虑下面的程序：

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实例的类型实际上并没有一个。

Answer 2:

最后，我想创建的深嵌入Category和Arrow一起Typeable的类型参数信息。这是这样我就可以用箭头语法来构建我的DSL的值，并有相当标准的Haskell代码。

也许你应该诉诸{-# LANGUAGE RebindableSyntax #-} （但同时指出，这意味着NoImplicitPrelude ）。创建自己的arr ， (>>>) first ， app ， (|||)和loop功能，脱糖箭头符号的时候，而不是标准的版本从Control.Arrow GHC会使用它们。

手册指出，“类型的这些功能必须非常密切的前奏类型匹配”。 如果你正在构建一个平行的类层次（层次的Control.Arrow但副本Typeable添加到该类型签名约束）你应该罚款。

（注：我不熟悉的箭头符号所以从来没有用过它与RebindableSyntax结合，我的答案是一个智能的猜测。）

文章来源: Transform a GADT without constraints to another GADT with constraints when such constraints hold