可以通过高阶函数对无类型 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 类型类的成员长什么样。
【问题讨论】：
标签： haskell functional-programming monads lambda-calculus untyped-variables
几乎可以表示您想要的任何类型。但由于每种类型的单子操作实现方式不同，不可能编写一次 >>= 并使其适用于每个实例。
但是，您可以编写依赖于类型类实例的证据的通用函数。将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))
然后您必须为 Monad 的每个实例定义一个“证据元组”。请注意，我们定义 bind 和 return 的方式：它们的工作方式与我们定义的其他“通用” Monad 方法一样：必须首先为它们提供 Monad 特性的证据，然后它们按预期运行。
我们可以将Maybe 表示为一个接受2 个输入的函数，第一个是Just x 时要执行的函数，第二个是一个值，如果它是Nothing 则替换它。
just = λxfz. f x
nothing = λfz. z
-- bind and return for maybes
bindMaybe = λmf. m f nothing
returnMaybe = just
maybeMonadEvidence = tuple bindMaybe returnMaybe
Lists 类似，将 List 表示为它的折叠函数。因此，列表是一个接受 2 个输入的函数，一个“cons”和一个“empty”。然后它在列表上执行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
【讨论】：
您将类型级别与价值级别混为一谈。在无类型的 lambda 演算中没有单子。可以有 monadic 操作（值级别），但不能有 monads（类型级别）。但是，操作本身可以相同，因此您不会失去任何表达能力。所以这个问题本身并没有真正的意义。
【讨论】：
好吧，我们已经有了元组和布尔值，因此我们可以表示 Either 以及基于此的任何非递归求和类型：
type Either a b = (Bool, (a, b))
type Maybe a = Either () a
Maybe 是 Monad 类型类的成员。转换为 lambda 表示法留作练习。
【讨论】：