Haskell 类型级 lambda 演算错误（或缺少）

Question

我一直在阅读 type arithmetic 上的 Haskell wiki 中的页面，并且在类型系统中嵌入的 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'

要找到我们的蛋糕，我们应该检查这两块石头下面：

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'

但是，嘿，转眼间！这是我们正在寻找的原始实例。所以总而言之，只要我们可以拥有我们的原始实例，我们就可以拥有我们的原始实例。所以我们声明我们可以拥有我们的原始实例，然后我们可以拥有我们的原始实例！是不是桃色。

Haskell 类型级 lambda 演算错误（或缺少）

Haskell type-level lambda calculus error (or lack thereof)

haskell

ghc

ghci