Pengkodean tipe rekursif pada Sistem F (dan sistem tipe murni lainnya)

Saya sedang mempelajari sistem tipe murni, khususnya kalkulus konstruksi, dan mencoba menggunakan pengkodean untuk tipe rekursif di atasnya, yang, menurut Philip Wadler, adalah mungkin . Sebagai contoh, saya menggunakan perpustakaan Morte Haskell untuk menyandikan angka Scott seperti yang diberikan oleh Cardelli .

Ringkasan pengkodean adalah seperti itu: diberi jenis rekursif (positif) ...

... kita dapat menyandikannya sebagai tipe pada Sistem F sebagai ...

... atau, menggunakan notasi sistem tipe murni (dengan eksplisit ) ...$F$

... karena adalah konstruktor tipe ( adalah tipe tipe).$F$$*$

Untuk mengkodekan seperti itu, kita perlu mendeklarasikan tiga fungsi, , dan , menurut Wadler, dan digunakan oleh Cardelli pada pengkodean untuk angka Scott.$fold$$in$$out$

lipat: Semua X. (FX -> X) -> T -> X

lipat = \ X. \ k: FX -> X. \ t: T. t X k

di: FT -> T

dalam = \ s: F T. \ X. \ k: FX -> X. k (F (lipat X k) s).

(Di mana adalah )$T$$Lfix\ X. F\ X$

Itu sepele untuk menulis fungsi seperti yang diberikan. Tetapi ketika mencoba untuk menulis fungsi , sepertinya tidak mengetik centang. Ekspresi memiliki tipe , dan harus dari jenis . Kemudian kita menyimpulkan bahwa harus bertipe (terlihat seperti a ). Ini bukan typecheck, karena merupakan konstruktor tipe (bertipe ).$fold$$in$$(fold\ X\ k)$$T\rightarrow X$$(F\ (fold\ X\ k)\ s)$$F\ X$$F$$(T\rightarrow X)\rightarrow F\ T\rightarrow F\ X$fmapF$*\rightarrow*$

Ini tidak terlihat seperti kesalahan ketik ... apakah saya melewatkan sesuatu?

Ada konvensi dalam teori kategori bahwa simbol yang sama digunakan untuk konstruktor tipe dan fungsi peta di atas konstruktor tipe tersebut. Karenanya, jika f: X -> Y maka F f: FX -> F Y.