当约束条件成立时，将带有约束条件的GADT转换为不受约束的GADT [英] Transform a GADT without constraints to another GADT with constraints when such constraints hold

问题描述

我们是否可以将GADT在其构造函数没有给定约束的情况下转换为具有上述约束的GADT？我想这样做是因为我想深入嵌入箭头，并用（现在）似乎需要 Typeable 的表示方式做一些有趣的事情。 （一个原因）

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

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

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)

因此，我们尝试捕获类型类中的转换。然而，这将打破以及我们将缺少 Typeable b 信息，因为 b 是一个存在。

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)

还有其他建议吗？最终，我想创建一个深层嵌入类别和箭头以及类型化 code>关于类型参数的信息。这样我就可以使用箭头语法在我的DSL中构建一个值，并拥有相当标准的Haskell代码。也许我必须求助于模板Haskell？

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?

推荐答案

递归案例的问题对于转换 DSL ab 转换为 DSL2 ab 。

The problem with the recursive case is fatal to transforming DSL a b into DSL2 a b.

要做这种转换，需要找到 Typeable 字典用于 Comp 情况下的存在类型 b 但实际上 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.

例如，考虑以下程序：

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 实例。

这篇关于当约束条件成立时，将带有约束条件的GADT转换为不受约束的GADT的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！