Haskell中的存在类型错误

Question

我在我的程序中苦于存在类型。我想我试图做一些非常合理的，但是我不能让过去的typechecker :(

我有一个数据类型，那种模仿的单子

data M o = R o | forall o1. B (o1 -> M o) (M o1) 

现在，我为它创建一个背景下，类似要在Haskell Wiki article on Zipper描述，但是我用的功能，而不是一个数据结构为简单起见 -

type C o1 o2 = M o1 -> M o2 

现在，当我尝试写一个分割数据值到它的上下文和子值函数，因此typechecker抱怨 -

ctx :: M o -> (M o1 -> M o, M o1) 
ctx (B f m) = (B f, m) -- Doesn't typecheck 

错误是 -

Couldn't match type `o2' with `o1' 
    `o2' is a rigid type variable bound by 
     a pattern with constructor 
     B :: forall o o1. (o1 -> M o) -> M o1 -> M o, 
     in an equation for `ctx' 
     at delme1.hs:6:6 
    `o1' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:6:1 
Expected type: M o2 
    Actual type: M o1 
In the expression: m 
In the expression: (B f, m) 

不过，我可以解决它像这样 -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK 

为什么这第二个定义类型检测，但不是第一位？

另外，如果我尝试通过检查R键ctx转换成完整的功能，我又得到一个类型检测错误 -

ctx (R o) = (id, R o) -- Doesn't typecheck 

错误 -

Couldn't match type `o' with `o1' 
    `o' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:7:1 
    `o1' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:7:1 
In the first argument of `R', namely `o' 
In the expression: R o 
In the expression: (id, R o) 

我怎样才能解决这个错误？

任何帮助表示赞赏！

Answer 1

让我们先看看失败的案例。这两个失败出于同样的原因，一旦你在暗示forall在类型添加签名是清晰的：

ctx :: forall o o1. M o -> (M o1 -> M o, M o1) 

即你的功能绝不仅仅是一个为一些o1的工作，但对于任何o1。

1. 在你的第一种情况下，

   ctx (B f m) = (B f, m) 
   

   我们知道f :: (o2 -> M o)和m :: M o2，为一些型o2，但我们必须能够提供任何类型o1，所以我们可以我们假设o1 ~ o2。

2. 在第二种情况下，

   ctx (R o) = (id, R o) 
   

   在这里，我们知道o :: o，但同样，该功能有任何o1来定义，所以我们不能假设o ~ o1。

您的解决方法似乎只起作用，因为它自称，类似于归纳证明。但是，如果没有基础的情况下，它只是循环论证的，你不能写基本情况该功能，因为没有办法构建从M o的M o1为o和o1任意组合，而无需使用底值。

什么你可能需要做的，就是要定义另一个生存型的背景下，而不是只使用一个元组。不知道这是否会为您的工作需要，但这种编译，至少：

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1) 

ctx :: M o -> Ctx o 
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m' 
ctx (R o) = Ctx id (R o) 

_{尝试使用的let代替case为a funny GHC error :)}