不能破坏传递的类型

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的一些代码不同的方式（每种方式我有多个不同的运行功能）。 运行函数将尝试尽可能多地运行代码，然后报告它无法运行的代码以及它可以运行的代码的结果。

Answer 1

由于您在GADT上进行了模式匹配，因此您需要run的类型签名。 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