Logika Combinatory Cukup Diketik?

Karena ada kalkulus lambda yang tidak diketik, dan kalkulus lambda yang diketik sederhana (seperti yang dijelaskan, misalnya, dalam buku Jenis dan Bahasa Pemrograman Benjamin Pierce), apakah ada logika kombinatorik yang diketik secara sederhana?

Sebagai contoh, akan terlihat bahwa tipe alami untuk kombinator S, K, dan saya adalah

S : (a -> b -> c) -> (a -> b) -> a -> c
K : a -> b -> a
I : a -> a

di mana a, b, dan c adalah variabel tipe mulai dari beberapa set tipe T. Sekarang, mungkin kita bisa mulai dengan tipe basis tunggal, Bool. Set tipe T kami kemudian Bool bersama dengan tipe apa pun yang dapat dibentuk menggunakan tiga pola

(a -> b -> c) -> (a -> b) -> a -> c
a -> b -> a
a -> a

di mana a, b, c dalam T.

Akan ada dua konstanta baru dalam bahasa tersebut.

T : Bool
F : Bool

Jadi, bahasa ini terdiri dari simbol S, K, I, T, dan F, bersama dengan tanda kurung. Ia memiliki satu tipe dasar Bool, dan "tipe fungsi" yang dapat dibuat dari pola kombinator S, K, dan I.

Apakah sistem ini dapat berfungsi? Misalnya, apakah ada konstruksi if-then-else yang diketik dengan baik yang dapat dibentuk hanya dari S, K, I, T, F?

Catatan cepat, saya izinkan parametrik polimorfisme (Sistem F) dalam sistem ini sehingga S, Kdan Idapat bekerja di semua jenis.

Perhatikan bahwa tanpa pencocokan pola, kita tidak dapat menulis ifapa pun yang kita lakukan. Kami sama sekali tidak memiliki operasi pada boolean. Tidak ada cara untuk membedakan Truedari False. Alih-alih mencoba

true : a -> a -> a
true = \t -> \f -> t

false : a -> a -> a
false = \t -> \f -> f

Mari kita biarkan Bool = a -> a -> auntuk kejelasan.

 if : Bool -> a -> a -> a
 if = \bool -> \a -> \b -> bool a b

Sekarang tinggal mengkompilasi beberapa ekspresi kalkulus lambda ke kombinator, yang cukup sepele.

if : Bool -> a -> a -> a -- Or just Bool -> Bool
if    = I

true : a -> a -> a
true  = K

false : a -> a -> a
false = K I