Церковь кодирование булева и STLC

Question

Часто говорит, что

tru t f = t 
fls t f = f 

представляет ложным и истинным в том смысле, что «мы можем использовать эти условия для выполнения операции по проверке истинности логического значения».

Но это скрывает важное предостережение, поскольку оно кажется верным только в нетипизированном исчислении лямбда. Если я просто подключить эти значения в Haskell, я могу написать функцию:

tryMeOnFalse ∷ (∀ t f. t → f → t) → String 
tryMeOnFalse tr = "Hi" 
a' = tryMeOnFalse tru 
b' = tryMeOnFalse fls -- type error ! 

, отличающее Tru и FLS на уровне типа. Как неправильно/справедливо было бы сказать, что:

• в STLC tru и fls являются значение свидетелей уровня некоторых способствовало 'Boolean рода, который имеет Типы 'True и 'False
• в STLC (принуждать) набрал значения и (fls :: ∀ t . t → t → t) представляют ложные и истинные (и в нетипизированным, ну обычный)

Edit: Я теперь понимаю, благодаря ответу @Daniel Вагнера я думал второго порядка лямбда-исчисление и не STLC в моей questi на.

Answer 1

Это не только верно в нетипизированном исчислении лямбда; но в типизированных исчислениях, как обычно, нужно немного осторожно печатать. Мы должны определить:

type Boolean = forall r. r -> r -> r 

Мы, конечно, есть tru, fls :: Boolean, и должны аннотировать их как таковые. но делаем не есть tryMeOnFalse :: Boolean -> String! Таким образом, здесь нет реального противоречия.

Ваши комментарии о STLC немного странны, поскольку STLC имеет очень разную систему набора текста. Нам понадобятся отдельные булевы типы для каждого типа результата, поскольку существует no полиморфизм.

В Haskell, можно, конечно, определить типы, которые населены только tru или только fls (ну, каждый тип также заселена undefined, конечно); но это, как правило, не очень полезно.