将更高的kinded类型(monads!)嵌入到无类型的lambda演算中

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

它可以代表你想要的任何类型.但由于一元操作对每种类型的实现方式不同,它是不是可以写>>=一次,有它的每个实例工作.

但是,您可以编写依赖于类型类实例的证据的泛型函数.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-ness的证据,然后它们按预期运行.

我们可以表示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

列表类似,表示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也很简单.将任一类型表示为具有两个函数的函数:如果它是a Left,则应用一个函数;如果是a ,则应用另一个函数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 ->)就是monad.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

Answer 2

您正在将类型级别与值级别混合.在无类型的lambda演算中,没有monad.可以有monadic操作(值级别),但不能使用monad(类型级别).但是,操作本身可以是相同的,因此您不会失去任何表达能力.所以问题本身并没有多大意义.