标签: lambda-calculus

我正在阅读皮尔斯的类型和编程语言一书,在关于递归类型的章节中,他提到它们可以用于用类型语言编码动态lambda演算.作为练习,我正在尝试在Haskell中编写该编码,但我无法通过typechecker:

{-# 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' …

t2 = (\x y z-> x.y.x)

GHCI告诉我这个:

t2 :: (b1 -> b2) -> (b2 -> b1) -> p -> b1 -> b2

我无法理解这种类型的签名是如何形成的.到目前为止,我已经认为r-most-x基本上是一个函数,它接受a b2并返回a b1,那么这b1是中间函数的输入y,并b2再次输出？它不应该返回新类型的值b3或什么？

我是 lambda 演算的新手，我发现语法有时对我来说不明确。\n具体来说，我想知道如何理解 Z 组合器：

Z = \xce\xbb f. (\xce\xbb x. f (\xce\xbb v. xxv)) (\xce\xbb x. f (\xce\xbb v. xxv))\n

如何在 OCaml 中编写它？\n更新：\n这样写时出现错误：

 fun f-> let g = fun x -> f(fun v-> x x v)in g g;;\n

错误：此表达式的类型为 'a -> 'b -> 'c\n但预期的表达式为 'a\n类型变量 'a 出现在 'a -> 'b -> 'c 内

我问的原因或原则.

我发现Java8中"流"接口的大多数方法都没有声明为"默认",因此它们没有方法体.例如:

boolean anyMatch(谓词谓词);

boolean allMatch(谓词谓词);

流映射(Function mapper);

正如您在源文件Stream.java中看到的那样.

但是这些没有实体的方法似乎能够在java程序中执行.

你知道为什么吗？

谢谢.