是否有可能在 Haskell 98 中获得无限种类的错误？答案

【问题标题】：Is it possible to get the infinite kind error in Haskell 98?是否有可能在 Haskell 98 中获得无限种类的错误？
【发布时间】：2015-07-09 01:54:03
【问题描述】：

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

+---------+---------+-------------------------------------------------------+
|   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 |
+---------+---------+-------------------------------------------------------+

当k1 和k2 都是变量时，它们会相互实例化。
当只有k1 是一个变量时，如果k1 没有出现在k2 中，它就会被实例化为k2。
当只有k2 是一个变量时，如果k2 没有出现在k1 中，它就会被实例化为k1。
否则我们检查k1和k2是否具有相同的名称和数量，并统一各自的参数。

对于第二种和第三种情况，我们需要实现发生检查，以免陷入无限循环。但是，我怀疑程序员是否能够构建无限种类。

在 Haskell 中，很容易构造一个无限类型：

let f x = f

但是，无论我多么努力，我都无法构建出无限种类。请注意，我没有使用任何语言扩展。

我问这个的原因是因为如果根本不可能构造一个无限的种类，那么我什至不会费心在我的种类系统中实现种类的发生检查。

【问题讨论】：

然后一些可怜的 sap 无论如何都会管理它并得到一个有用的“不可能发生的事情”
为什么你的问题被标记为 Prolog 和 OCaml？根据我的理解，这只是关于 Haskell 和你的新语言。
@Kevin：两者都很脆弱，但并非完全无关。 OCaml 具有与 Haskell 非常相似的类型系统，Prolog 是统一思想和发生检查的起源（据我所知）。从某种意义上说，这种类型检查很像运行 Prolog 程序。
Greenspun's Tenth Rule 的修改形式表明任何足够复杂的类型检查器都包含一个临时的、非正式指定的、充满错误的、缓慢的 Prolog 一半实现。

标签： haskell functional-programming ocaml type-inference unification

【解决方案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’

消息并没有说它是无限类型，但本质上就是发生检查失败时的情况。

【讨论】：

【解决方案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

【讨论】：