Teori kategori (bukan) untuk Pemrograman?

Setelah mempelajari Haskell dan bahasa FP lain yang tidak murni, saya memutuskan untuk membaca tentang teori Kategori. Setelah mendapatkan pemahaman yang baik tentang teori Kategori saya mulai berpikir tentang bagaimana konsep teori kategori dapat digunakan untuk berpikir tentang merancang program tetapi tidak peduli seberapa keras saya mencoba sepertinya ini bukan cara yang harus dilakukan.

Setelah menghabiskan banyak usaha yang gagal untuk menghubungkan teori kategori dengan merancang program, saya sampai pada kesimpulan bahwa:

• Teori kategori berguna ketika merancang bahasa pemrograman .
• Teori kategori bukanlah sesuatu yang Anda gunakan saat merancang program (bahkan ketika menggunakan bahasa yang dirancang berdasarkan prinsip-prinsip kategori). Sebagai contoh: Ketika pemrograman di Haskell Anda akan menggunakan tipe, tipe konstruktor, fungsi, fungsi tingkat tinggi dll untuk merancang program Anda, bukan konsep teori kategori.

Singkatnya, kami memiliki sistem di bawah lapisan (urutan rendah ke tinggi):

Teori kategori -> Bahasa pemrograman -> Program

Pada lapisan tertentu Anda menggunakan konsep lapisan yang mendasari langsung .

Apakah pemahaman ini benar? Jika tidak dan Anda yakin bahwa dalam merancang program kami dapat langsung menggunakan konsep teori kategori, silakan merujuk beberapa artikel atau posting blog di mana itu sedang diperagakan.

CATATAN: Dengan merancang program, maksud saya merancang program berdasarkan pada konsep yang berbeda, seperti konkurensi, paralelisme, reaktif, pengiriman pesan, dll.

Ya, tentu saja itu tergantung pada jenis program yang Anda coba desain.

Jika Anda merancang program akuntansi untuk toko cokelat bibimu, saya sangat ragu bahwa teori kategori akan banyak berguna.

Tetapi tentu saja ada situasi di mana teori kategori sangat berguna dalam merancang program (yang saya maksudkan adalah struktur data, perpustakaan, dan sebagainya). Situasi seperti itu terjadi terutama ketika program yang terlibat bersifat matematis.

Jika Anda ingin menulis program yang menghitung dengan bilangan real yang tepat dan struktur lain yang terjadi dalam analisis matematika, pertanyaan pertama yang perlu Anda jawab adalah apa artinya menerapkan dengan benar objek matematika yang rumit (seperti fungsi terdiferensiasi, bermacam-macam, dll. ). Di sini sangat membantu untuk mengetahui beberapa teori kategori dan logika, karena mereka memberi Anda cara sistematis menerjemahkan definisi struktur matematika ke spesifikasi dan implementasi struktur data yang sesuai. Kata kunci yang harus Anda cari adalah teori realisasi . Tapi ini hanya satu contoh.

Cara terbaik untuk melihat bagaimana teori kategori sangat berguna adalah dengan melihat program yang ditulis oleh orang-orang yang tahu banyak teori kategori (dan matematika secara umum). Contoh nyata dari hal ini adalah Martín Escardó dan fungsi fungsionalnya yang mustahil, misalnya:

M. Escardó dan P. Oliva: Apa Permainan Berurutan, Teorema Tychonoff dan Pergeseran Double-Negatif memiliki Pemrograman Fungsional Bersama , yang terstruktur secara matematis 2010, ACM Press. (dengan file pendamping Haskell dan Agda )

Anda mungkin mengeluh bahwa ini bukan hanya teori kategori tetapi juga logika dan topologi. Keluhan seperti itu akan sangat salah kaprah. Teori kategori terbaik selalu dicampur dengan hal-hal lain.

Terakhir, saya akan menyarankan untuk tidak menarik kesimpulan besar tentang sifat hal-hal berdasarkan sedikit bacaan yang ditugaskan sendiri.

Orang-orang menggunakan CT untuk menggambarkan tipe data.

1. Tipe data didefinisikan oleh kategori tertentu yang objeknya adalah urutan terbatas tipe (bahasa spesifikasi), dan yang panahnya adalah proyeksi atau komposisi dari operasi tipe data. Sebagai contoh, objek adalah domain dan merupakan kode dari operasi push tumpukan. Ini memberi Anda sintaks, tetapi Anda masih belum memiliki gagasan tentang semantik.
2. Aljabar, yang artinya, turunan dari tipe, adalah fungsi dari teori ke Ens, kategori set (kecil). (Kami menggunakan "kecil" untuk menghindari paradoks Russell, tetapi itu tidak terlalu penting.)
3. Ternyata sifat penutupan kategori sesuai dengan keluarga teori logis. Misalnya, jika kategori teori ditutup di bawah produk, tipe data dapat di Aksioma oleh persamaan. Jika kategori teori ditutup dengan mengambil mundurnya, maka tipe data dapat di Aksioma oleh kalimat Horn.

Saya tidak sepenuhnya yakin ada orang yang memperhatikan hal ini lagi. Saya akan berpikir bahwa ini , dan tautan di sana, akan menjelaskannya dengan lebih rinci.