是否有可能在Haskell 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一个变量时,它被实例化为k2iff k1不会发生k2.
3. 当只是k2一个变量时,它被实例化为k1iff k2不会发生k1.
4. 否则,我们检查是否k1与k2具有相同的名称和参数数量,统一各自的论点.

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

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

let f x = f

然而,无论我怎么努力,我都无法构建无限种类.请注意,我没有使用任何语言扩展.

我问这个的原因是因为如果根本不可能构建一个无限种类,那么我甚至不会在我的类系统中实现对种类的发生检查.

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’

该消息并未说明它是无限种类,但这基本上就是发生检查失败时的情况.

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