Haskell 中存在类型的类型错误

Question

我在程序中与存在类型作斗争。我认为我正在尝试做一些非常合理的事情，但是我无法通过类型检查器:(

我有一个有点模仿 Monad 的数据类型

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

现在我为它创建一个上下文，类似于 关于 Zipper 的 Haskell Wiki 文章，但是为了简单起见，我使用函数而不是数据结构 -

type C o1 o2 = M o1 -> M o2

现在，当我尝试编写一个将数据值拆分为的函数时它的背景和subvalue，类型检查器抱怨 -

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

为什么第二个定义进行类型检查而不是第一个定义？

另外，如果我尝试将 ctx 转换为完整的函数？通过检查 R，我再次收到类型检查错误 -

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 fm) = (B f, m)
   

   我们知道 f :: (o2 -> M o) 和 m :: M o2，对于 some 类型 o2，但我们必须能够提供任何类型o1，所以我们不能假设o1 ~ o2 .

2. 在第二种情况下，

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

   在这里，我们知道 o :: o，但同样，必须为 any 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而不是一个有趣的 GHC 错误的案例 :)}