haskell - 当约束成立时，将没有约束的 GADT 转换为另一个有约束的 GADT

Question

我们能否将构造函数没有给定约束的 GADT 转换为具有上述约束的 GADT？我想这样做是因为我想要深度嵌入箭头，并使用(目前)似乎需要 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
  -- ...

我们可以尝试以下 from 函数，但由于我们没有递归点的可输入信息

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 来说是致命的。

要进行此转换，需要在 Comp 情况下找到存在类型 b 的 Typeable 字典 - 但什么 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 实例。