在Haskell中使用存在类型键入错误

Question

我在计划中与存在主义类型斗争.我想我正在尝试做一些非常合理的事情但是我无法超越typechecker :(

我有一种模仿Monad的数据类型

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

现在我为它创建一个Context,类似于关于Zipper的Haskell Wiki文章中描述的,但是为简单起见,我使用函数而不是数据结构 -

type C o1 o2 = M o1 -> M o2

现在,当我尝试编写一个将数据值拆分为其上下文和子值的函数时,类型检查器会抱怨 -

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 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 o1from和M ofor的任何组合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为一个有趣的GHC错误 :)}