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！這是我們正在尋找的原始實例。所以總而言之，只要我們可以擁有原始實例，我們就可以擁有原始實例。所以我們聲明我們可以擁有我們的原始實例，然後我們可以擁有我們的原始實例！這不是那麼好嗎？