Curry 悖论 (以与目前的编程语言相同的人命名)是一种可能在错误逻辑中的构造,它允许人们证明任何事情。
我对逻辑一无所知,但它有多难?
module Main where
import Data.Void
import Data.Function
data X = X (X -> Void)
x :: X
x = fix \(X f) -> X f
u :: Void
u = let (X f) = x in f x
main :: IO ()
main = u `seq` print "Done!"
它肯定会循环。(GHC怎么知道?!)
% ghc -XBlockArguments Z.hs && ./Z
[1 of 1] Compiling Main ( Z.hs, Z.o )
Linking Z ...
Z: <<loop>>
- 这是忠实的翻译吗?为什么?
- 我可以在没有
fix
递归的情况下做同样的事情吗?为什么?