Часто говорят, что
tru t f = t
fls t f = f
представляют True и False в том смысле, что «мы можем использовать эти термины для выполнения операции по проверке истинности логического значения».
Но за этим скрывается важное предостережение, поскольку оно кажется истинным только в нетипизированном лямбда-исчислении. Если я просто подставлю эти значения в 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 (принудительно) типизированные значения
(tru :: ∀ t . t → t → t)и(fls :: ∀ t . t → t → t)представляют собой True и False (а в нетипизированных, как обычно)
Изменить: теперь я понимаю, благодаря ответу @Daniel Wagner, что я думал о лямбда-исчислении второго порядка, а не о STLC в своем вопросе.
