Haskell 类型级 lambda 演算错误(或缺乏)

Question

我一直在阅读 Haskell wiki 上的页面 type arithmetic并且在类型系统中嵌入的 lambda 演算部分遇到了一些麻烦。从该部分中，我了解到以下代码不应该与 GHC/GHCi 一起使用 - 显然 GHC 不应该能够确定 g 的类型签名。

{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

data X
data App t u
data Lam t

class Subst s t u | s t -> u
instance Subst X u u
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')
instance Subst (Lam t) u (Lam t)

class Apply s t u | s t -> u
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

class Eval t u | t -> u
instance Eval X X
instance Eval (Lam t) (Lam t)
instance (Eval s s', Apply s' t u) => Eval (App s t) u

f :: Eval (App (Lam X) X) u => u
f = undefined
g :: Eval (App (Lam (App X X )) (Lam (App X X ))) u => u
g = undefined

请注意，我必须添加FlexibleContexts 和UndecidableInstances，因为如果没有这些扩展，给定的代码似乎无法编译。但是，当我使用 GHCi(版本 8.0.2)运行此命令时，我得到以下结果:

*Main> :t f
f :: X
*Main> :t g
g :: u

这对我来说特别奇怪，因为类型 u 还没有在任何地方定义。这是上面两种语言扩展相互交互和 glasgow-exts 交互的结果吗？如果是这样，怎么办？

Answer 1

类型u只是一个单独的类型变量——就像undefined::a中的a一样。

要真正将其归结为最基本的要素，请考虑这个备用文件:

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

class Loopy a
instance Loopy a => Loopy a

x :: Loopy a => a
x = undefined

如果您在 ghci 中询问 x 的类型，它会告诉您它的类型为 a，但没有上下文。这可能看起来有点神奇；您只需认识到 GHC 中的实例解析完全可以递归，并且实现会竭尽全力支持这一点。

如果您愿意，我们可以详细了解您的示例中发生的情况，但它与上面的文件非常相似。以下是详细信息。

所以，我们想看看是否允许我们拥有这个实例:

Eval (App (Lam (App X X)) (Lam (App X X))) u

我们知道

instance (Eval s s', Apply s' t u) => Eval (App s t) u

所以只要我们同时拥有这两者，我们就可以拥有它:

Eval (Lam (App X X)) s'
Apply s' (Lam (App X X)) u

第一个很简单，因为:

instance Eval (Lam t) (Lam t)

因此，当我们满足以下条件时，我们就可以享用蛋糕:

Apply (Lam (App X X)) (Lam (App X X)) u

自从

instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

要找到我们的蛋糕，我们应该检查这两 block 岩石下面:

Subst (App X X) (Lam (App X X)) u
Eval u u'

来自

instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')

我们知道什么时候可以吃蛋糕

Subst X (Lam (App X X)) s'
Subst X (Lam (App X X)) t'
Eval (App s' t') u'

这很容易取得进展，因为:

instance Subst X u u

因此，我们可以在以下任何时候拥有原始实例:

Eval (App (Lam (App X X)) (Lam (App X X))) u'

但是，嘿，快点!这是我们正在寻找的原始实例。总之，只要我们能够拥有原始实例，我们就可以拥有原始实例。所以我们声明我们可以拥有我们的原始实例，然后我们就可以拥有我们的原始实例!这不是桃子吗？