Парадокс карри в хаскеле? - PullRequest
Новая
       96

Парадокс карри в хаскеле?

4 голосов
/ 12 октября 2019

парадокс Карри (назван в честь того же человека, что и нынешний язык программирования) - это конструкция, возможная в ошибочной логике, которая позволяет доказать что-либо.

Я ничего не знаю о логике, но насколько это может быть сложно? 

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 или рекурсии? Почему?

1 Ответ

4 голосов
/ 12 октября 2019

Кодировка парадокса Карри выглядит примерно так: 

x :: X
x = X (\x'@(X f) -> f x')

X действительно может быть прочитано как предложение "если X верно, то есть противоречие", или эквивалентно,«X является ложным».

Но использование fix для доказательства X на самом деле не имеет смысла, потому что fix явно неверно как принцип рассуждения. Парадокс Карри более тонкий.

Как вы на самом деле доказываете, что X? 

x :: X
x = _

X - это условное суждение, поэтому вы можете начать с предположения, что его предпосылка показывает его заключение,Этот логический шаг соответствует вставке лямбды. (Конструктивно доказательством импликации является сопоставление доказательств предпосылки с доказательствами заключения.) 

x :: X
x = X (\x' -> _)

Но теперь у нас есть предположение x' :: X, мы можем развернуть определение X снова, чтобы получить f :: X -> Void. В неофициальных описаниях парадокса Карри нет явного «шага разворачивания», но в Haskell это соответствует сопоставлению с образцом в конструкторе newtype, когда X является предположением, или применяет конструктор, когда X является целью (вфакт, как мы делали выше): 

x :: X
x = X (\x'@(X f) -> _)

Наконец, теперь у нас есть f :: X -> Void и x' :: X, поэтому мы можем вывести Void с помощью приложения функции: 

x :: X
x = X (\x'@(X f) -> f x')
...