綁定的相互遞歸語法

這是一個依賴型lambda演算的語法。綁定的相互遞歸語法

data TermI a = Var a 
      | App (TermI a) (TermC a) -- when type-checking an application, infer the type of the function and then check that its argument matches the domain 
      | Star -- the type of types 
      | Pi (Type a) (Scope() Type a) -- The range of a pi-type is allowed to refer to the argument's value 
      | Ann (TermC a) (Type a) -- embed a checkable term by declaring its type 
      deriving (Functor, Foldable, Traversable) 

data TermC a = Inf (TermI a) -- embed an inferrable term 
      | Lam (Scope() TermC a) 
      deriving (Functor, Foldable, Traversable) 

type Type = TermC -- types are values in a dependent type system

（I更多或更少從Simply Easy解除此。）類型系統是bidirectional，分裂字詞那些類型可以從打字上下文來推斷，以及那些只能針對一個目標被檢查類型。這在依賴類型系統中很有用，因爲一般來說，lambda表達式將不具有主體類型。

無論如何，我得堅持試圖定義一個Monad實例的語法：

instance Monad TermI where 
    return = Var 
    Var x >>= f = f x 
    App fun arg >>= f = App (fun >>= f) (arg >>= Inf . f) -- embed the substituted TermI into TermC using Inf 
    Star >>= _ = Star 
    Pi domain range >>= f = Pi (domain >>= Inf . f) (range >>>= Inf . f) 
    Ann term ty >>= f = Ann (term >>= Inf . f) (ty >>= Inf . f) 

instance Monad TermC where 
    return = Inf . return 
    Lam body >>= f = Lam (body >>>= f) 
    Inf term >>= f = Inf (term >>= _)

爲了填補TermC的情況下的最後一列上的孔，我需要的類型a -> TermI b但f的東西有一種a -> TermC b。我不能使用Ann構造函數將生成的TermC嵌入到TermI中，因爲我不知道TermC的類型。

該數據類型是否與bound的模型不兼容？或者是否有一個技巧可以讓Monad實例去？

來源

2016-08-20 Benjamin Hodgson

如果運行（濫用符號）'（VAR 0（VAR 1））[\ X - > X]'，你會得到'（\ x - > x）（var 1）'，它在你的類型系統中沒有語法表示。請注意，本文中的兩個'subst'都接收可推論的術語，並且沒有'subst：TermC - > TermC - > TermC'。爲了定義一個雙向類型檢查器，不一定要有雙向類型系統，所以你可以將這些相互遞歸的數據類型合併成一個「Term」。 – user3237465

'bound'不支持共享數據，但（如上所述），您可以使用單個數據定義來完成類型檢查。「綁定」的索引版本可以執行相互數據（[例如]（http://lpaste.net/79582）），但它不作爲發佈的庫存在。 –

將所有東西都放到一個數據類型中並不是沒有缺點：它可以讓你在沒有註釋的情況下編寫一個'Lam'，它不應該在語法上有效。我想我可以在'Lam'構造函數（'Lam（Scope（）Term a）Type'）中需要一個類型，但是對於嵌套lambda表達式您會得到多餘的註釋，並且您必須支持用於註釋其他項的額外構造。 –

這完全不可能：TermC不是一個monad。替代放置條款代替變量。爲了有意義，這些術語需要能夠適合，即足夠相似以致所得到的術語仍然具有良好的性質。這意味着它的類型必須是可以推斷的。 TermC不會。

您可以實現：

substI :: TermI a -> (a -> TermI b) -> TermI b 
substC :: TermC a -> (a -> TermI b) -> TermC b

，並有

instance Monad TermI where 
    return = Var 
    bind = substI

來源

2016-08-22 10:12:01 gallais

這種有點作品 - 你得到了「Monad」實例 - 但它最終變得醜陋。你不能使用大部分'bound'的組合器（包括'>>> =' - 你必須通過'Scope'下的'fmap'ping來實現'subst'），因爲它們需要一個'Monad'實例用於'範圍的第二個參數。所以你最終重新實現了大部分「綁定」。 –

綁定的相互遞歸語法

回答

相關問題