在無類型lambda微積分中嵌入更高kinded類型（monads！）

Question

可以通過高階函數在無類型lambda微積分中編碼各種類型。

Examples: 
zero = λfx.  x 
one = λfx.  fx 
two = λfx. f(fx) 
three = λfx. f(f(fx)) 
etc 

true = λtf. t 
false = λtf. f 

tuple = λxyb. b x y 
null = λp. p (λxy. false) 

我想知道是否有任何研究嵌入其他不太常規的類型。如果存在一些斷言可以嵌入任何類型的定理，那將是非常光明的。也許有限制，例如只有類型*可以嵌入。

如果確實可以表示不太常規的類型，那麼看到一個例子就太棒了。我特別熱衷於看到monad類型的成員是什麼樣的。

Answer 1

您正在將類型級別與值級別混合在一起。在無類型的lambda微積分中，沒有單子。可以有monadic操作（值級別），但不是monad（類型級別）。該操作本身可以是相同的，但是，這樣你就不會丟失任何的表現力。所以這個問題本身並不合理。

Answer 2

好了，我們已經擁有的元組和布爾值，因此我們可以代表Either，進而基於任何非遞歸和類型：

type Either a b = (Bool, (a, b)) 
type Maybe a = Either() a 

，也許是單子類型類的成員。將lambda表示法翻譯爲練習。

Answer 3

它可能代表幾乎任何你想要的類型。但是，由於每種類型的一元操作的實施方式不同，因此可以將而不是寫入>>=一次，並使其適用於每個實例。

但是，您可以可以編寫依賴於類型類實例的證據的通用函數。考慮這裏的e是一個元組，其中fst e包含「綁定」定義，並且snd e包含「返回」定義。

bind = λe. fst e -- after applying evidence, bind looks like λmf. ___ 
return = λe. snd e -- after applying evidence, return looks like λx. ___ 

fst = λt. t true 
snd = λt. t false 

-- join x = x >>= id 
join = λex. bind e x (λz. z) 

-- liftM f m1 = do { x1 <- m1; return (f x1) } 
-- m1 >>= \x1 -> return (f x1) 
liftM = λefm. bind e m (λx. return e (f x)) 

你將不得不定義一個「證據元組」的單子的每個實例。請注意，在路上，我們定義bind和return：他們的工作就像其他「通用」單子我們定義的方法：他們首先必須得到單子岬的證據，然後他們按預期。

我們可以表示Maybe作爲需要2個輸入的函數，第一個是執行，如果它是Just x一個函數，第二個是與如果是沒有替換它的值。

just = λxfz. f x 
nothing = λfz. z 

-- bind and return for maybes 
bindMaybe = λmf. m f nothing 
returnMaybe = just 

maybeMonadEvidence = tuple bindMaybe returnMaybe 

列表相似，代表List作爲其摺疊功能。因此，列表是一個函數，需要2個輸入，一個「缺點」和一個「空白」。然後它在列表上執行foldr myCons myEmpty。

nil = λcz. z 
cons = λhtcz. c h (t c z) 

bindList = λmf. concat (map f m) 
returnList = λx. cons x nil 

listMonadEvidence = tuple bindList returnList 

-- concat = foldr (++) [] 
concat = λl. l append nil 

-- append xs ys = foldr (:) ys xs 
append = λxy. x cons y 

-- map f = foldr ((:) . f) [] 
map = λfl. l (λx. cons (f x)) nil 

Either也很簡單。將任一類型表示爲具有兩個功能的函數：如果它是Left，則應用一個;如果是Right，則應用另一個類型。

left = λlfg. f l 
right = λrfg. g r 

-- Left l >>= f = Left l 
-- Right r >>= f = f r 
bindEither = λmf. m left f 
returnEither = right 

eitherMonadEvidence = tuple bindEither returnEither 

不要忘記，職能自己(a ->)形式的單子。而lambda演算中的所有內容都是一個函數......所以......不要太想它。 ;）直接從啓發的Control.Monad.Instances

-- f >>= k = \ r -> k (f r) r 
bindFunc = λfkr. k (f r) r 
-- return = const 
returnFunc = λxy. x 

funcMonadEvidence = tuple bindFunc returnFunc