haskell - 当此类约束成立时，将一个没有约束的 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这样我就可以使用箭头语法在我的 DSL 中构造一个值，并拥有相当标准的 Haskell 代码。也许我必须求助于 Template Haskell？

Answer 1

递归情况的问题对于转换DSL a b为DSL2 a b.

要进行这种转换，需要找到案例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