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型尚未在任何地方定义。这是上述两种语言扩展的结果，它们是相互作用的，还是格拉斯哥外部语言？如果是这样，怎么样？

Answer 1

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

要真正熬下来到它的最基本，考虑这个备用文件：

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

class Loopy a 
instance Loopy a => Loopy a 

x :: Loopy a => a 
x = undefined 

如果你问的x在ghci的类型，它会告诉你它的类型为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' 

但是，嘿presto！这是我们正在寻找的原始实例。所以总而言之，只要我们可以拥有原始实例，我们就可以拥有原始实例。所以我们声明我们可以拥有我们的原始实例，然后我们可以拥有我们的原始实例！这不是那么好吗？