とよく言われます
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ではなく2次ラムダ計算を考えていたことに気づきました。