无法破坏传递类型

Question

说我有以下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函数将尝试尽可能多地运行给出的代码,然后报告它无法运行的代码以及它可以运行的代码的结果.

Answer 1

你需要一个类型签名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