4

假设我有以下 GADT：

data Stage a b where
    Comb :: Stage a b -> Stage b c -> Stage a c
    FMap :: (a -> b) -> Stage a b

我现在想要一个像这样工作的函数：

run (a `Comb` b) = (a,b)
run (FMap f)     = (FMap f,FMap id)

我将如何构建这样的功能？

我尝试了不同的绑定类型的方法，但没有成功。是否有我缺少的扩展可以实现更广泛的类型绑定？

这是错误消息：

Couldn't match type `t' with `(Stage t1 b, Stage b t2)'
  `t' is a rigid type variable bound by
      the inferred type of run :: Stage t1 t2 -> t at <interactive>:11:5
In the expression: (a, b)
In an equation for `run': run (a Comb b) = (a, b)

我想要完成的描述：我想设计一个 DSL 和一个函数运行，它可以尝试以几种不同的方式运行 DSL 的一些代码（每种方式我有多个不同的运行函数）。run 函数将尝试运行尽可能多的代码，然后报告它不能运行的代码以及它可以运行的代码的结果是什么。

4

1 回答 1

7

您将需要 的类型签名run，因为您在 GADT 上进行模式匹配。GADT 上的模式匹配需要类型细化，并且通常仅在存在类型签名时才有效。

但目前还不清楚类型签名是什么。如果输入值为

a `Comb` b :: Stage x y

然后你回来(a, b)，在哪里

a :: Stage x b
b :: Stage b y

对于一些不为人知的b。这是一种存在类型的逃避。你不能写

run :: Stage x y -> (State x b, Stage b y)

因为这意味着它必须适用于所有人 b，但它只适用于某些（未知）b。

不幸的是，尚不清楚为什么要编写类似run. 为什么要生产一双？以后你想用这对做什么？构造Comb函数被定义为结合两个具有未知中间类型的阶段，所以这个版本的run可以工作：

run :: Stage a b -> Stage a b
run (a `Comb` b) = a `Comb` b
run (FMap f)     = FMap f `Comb` FMap id

或者您可以定义一个更具体的数据类型，只允许具有未知中间类型的两个阶段的“对”：

data PairStages a b where
  PairStages :: Stage a b -> Stage b c -> PairStages a c

接着：

run :: Stage a b -> PairStages a b
run (a `Comb` b) = PairStages a b
run (FMap f)     = PairStages (FMap f) (FMap id)

但是我仍然觉得run返回一对很奇怪。正如我所说，目前还不清楚你想对run. run有一个递归函数似乎更有用，它实际上以某种方式结合了在Comb案例中运行组件的结果。例如，像这样：

run :: Stage a b -> (a -> b)
run (a `Comb` b) = run b . run a
run (FMap f)     = f
于 2013-03-06T19:44:59.593 回答