哈斯克尔98是否可能出现无限种错误？

Question

我正在为一种新的函数式编程语言实现一种类型系统，目前正在编写将两种类型统一的函数。需要考虑四种情况：

+---------+---------+-------------------------------------------------------+
|   k1    |   k2    |                        action                         |
+=========+=========+=======================================================+
|   var   |   var   |                  k1 := k2 ^ k2 := k1                  |
+---------+---------+-------------------------------------------------------+
|   var   | non var |             if (!occurs(k1, k2)) k1 := k2             |
+---------+---------+-------------------------------------------------------+
| non var |   var   |             if (!occurs(k2, k1)) k2 := k1             |
+---------+---------+-------------------------------------------------------+
| non var | non var | ensure same name and arity, and unify respective args |
+---------+---------+-------------------------------------------------------+

1. 当k1和k2都是变量时，它们会互相实例化。
2. 当只有k1是变量时，如果k1不出现在k2中，则将其实例化为k2。
3. 当只有k2是变量时，如果k2不出现在k1中，则将其实例化为k1。
4. 否则，我们将检查k1和k2是否具有相同的名称和arity，并统一它们各自的参数。

对于第二种和第三种情况，我们需要实现“出现检查”以避免陷入无限循环。但是，我怀疑程序员能够构造出无限的类型。

在Haskell中，构造无限类型很容易:

let f x = f

不过，我尽力了但是没有成功构建出无限种类。请注意，我没有使用任何语言扩展。

我问这个问题的原因是，如果根本无法构建无限种类，那么我就不会费心在我的种类系统中实现出现检查。

- Aadit M Shah

---

然后一些可怜的家伙仍然设法做到了，并得到了一句有用的话“奇迹发生了”。 - Cubic

为什么你的问题被标记为Prolog和OCaml？从我阅读它的理解来看，它只涉及到Haskell和你的新语言。 - Kevin

@Kevin：两者都不是很紧密相关，但也不完全无关。OCaml的类型系统与Haskell非常相似，而Prolog则是协一化和出现检查思想的来源（就我所知）。在某种程度上，这种类型检查非常类似于运行Prolog程序。 - Tikhon Jelvis

格林斯潘的第十条规则的修改版称：任何足够复杂的类型检查器都包含一个临时指定、非正式规定、错误百出、速度缓慢的 Prolog 的一半实现。 - Jack

Answer 1

data F f = F (f F)

在 GHC 7.10.1 上，我收到了如下消息：

kind.hs:1:17:
    Kind occurs check
    The first argument of ‘f’ should have kind ‘k0’,
      but ‘F’ has kind ‘(k0 -> k1) -> *’
    In the type ‘f F’
    In the definition of data constructor ‘F’
    In the data declaration for ‘F’

该消息并没有明确表明它是一种无限类型，但当发生检查失败时，本质上就是这种情况。

- Carl

Answer 2

另一个简单的例子

GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
Prelude> let x = undefined :: f f

<interactive>:2:24:
    Kind occurs check
    The first argument of ‘f’ should have kind ‘k0’,
      but ‘f’ has kind ‘k0 -> k1’
    In an expression type signature: f f
    In the expression: undefined :: f f
    In an equation for ‘x’: x = undefined :: f f

- Reid Barton