使用遞歸類型對Haskell中的動態類型lambda積分進行編碼

我正在閱讀Pierce的類型和編程語言書籍，在關於遞歸類型的章節中他提到可以用類型化語言對動態lambda積分進行編碼。作爲練習，我試着寫在Haskell該編碼，但我不能讓它通過typechecker：眼下使用遞歸類型對Haskell中的動態類型lambda積分進行編碼

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} 

data D = D (forall x . x -> x) 

lam :: (D -> D) -> D 
--lam f = D f 
lam = undefined 

ap :: D -> D -> D 
ap (D f) x = f x 

--Some examples: 
myConst :: D 
myConst = lam (\x -> lam (\y -> x)) 

flippedAp :: D 
flippedAp = lam (\x -> lam (\f -> ap f x))

，這個代碼給我下面的錯誤信息（我就不說了真正理解）：

dyn.hs:6:11: 
    Couldn't match type `x' with `D' 
     `x' is a rigid type variable bound by 
      a type expected by the context: x -> x at dyn.hs:6:9 
    Expected type: x -> x 
     Actual type: D -> D 
    In the first argument of `D', namely `f' 
    In the expression: D f 
    In an equation for `lam': lam f = D f

改變的lam定義爲undefined（被註釋掉的行）獲取的代碼編譯，所以我懷疑，不管我做錯了或者是在林的定義或爲原始定義D數據類型。

來源

2013-09-21 hugomg

這是行不通的原因是因爲f :: D -> D。 D想要一個可以接受任何類型的功能x並返回x。這相當於

d :: forall a. a -> a

正如你所看到的，這樣做的唯一理智的實現是id。嘗試

data D = D (D -> D) 
... 
unit = D id

也許好打印：

data D = DFunc (D -> D) | DNumber Int

來源

2013-09-21 03:47:14 jozefg

現在該死的那麼明顯。在Haskell中，遞歸類型量詞是隱含的，所以我不需要像我那樣寫下來。 – hugomg

'數據D = D（D - > D）'有很多非底層居民...... –

@DanielWagner Gah，你是對的，更新.. – jozefg

的問題是，你的f具有類型D -> D（可按lam你的類型的簽名），但D構造預計forall x . x -> x類型的參數。這些不是同一類型，所以編譯器抱怨

來源

2013-09-21 03:46:44

使用遞歸類型對Haskell中的動態類型lambda積分進行編碼

回答

相關問題