Apakah ada kalkulus SKI yang diketik?

Sebagian besar dari kita tahu korespondensi antara logika kombinasi dan kalkulus lambda . Tapi saya belum pernah melihat (mungkin saya belum melihat cukup dalam) setara dengan "combinator yang diketik", sesuai dengan kalkulus lambda yang diketik sederhana. Apakah hal seperti itu ada? Di mana orang dapat menemukan informasi tentang itu?

Kelengkapan ekspresif dari combinator yang diketik dibandingkan dengan kalkulus lambda yang diketik sederhana telah ditunjukkan . Untuk setiap combinator yang tidak diketik, seseorang membutuhkan seluruh keluarga dari combinator yang diketik. Sebagai contoh, seseorang memiliki

• $\mathbf{I}_{\alpha\to\alpha}$
• $\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
• $\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$

untuk semua kombinasi tipe sederhana , dan γ .$\alpha,\beta$$\gamma$

Atau, anggap saja tipe-tipe tersebut sebagai skema tipe (atau tipe polimorfik) dan masukkan ke dalam Haskell dan voila: combinators .