Bagaimana tipe dibuktikan — sistem tipe TypeScript dan korespondensi Curry–Howard

Ringkasan:

• Menyajikan sudut pandang yang menafsirkan sistem tipe TypeScript bukan sekadar pemeriksa tipe statis sederhana, melainkan sebagai sistem pembuktian dalam logika.
• Menjelaskan secara konseptual mengapa inferensi tipe dimungkinkan berdasarkan korespondensi Curry–Howard (Type = Proposition, Program = Proof).
• Menjelaskan fitur-fitur TypeScript seperti tipe fungsi, generik, conditional type, dan type narrowing dengan memetakannya ke implikasi logis, kuantifikasi universal, dan analisis kasus.
• Menafsirkan proses type checking bukan sebagai penerapan aturan, melainkan sebagai proses memverifikasi relasi antarproposisi.
• Berfokus pada latar belakang desain dan struktur matematis sistem tipe TypeScript, alih-alih detail implementasi.

Ringkasan detail:

1. Latar belakang: mengapa inferensi tipe dimungkinkan?
   Dalam bahasa dengan tipe statis, inferensi tipe sering dijelaskan sebagai persoalan implementasi tentang “bagaimana compiler mencocokkan tipe”.
   Tulisan ini mundur selangkah lebih jauh dari itu dan mempertanyakan alasan mendasar mengapa inferensi tipe pada dasarnya bisa dilakukan.
   Sebagai jawabannya, tulisan ini menawarkan sudut pandang yang melihat sistem tipe sebagai sistem pembuktian dalam logika.

2. Landasan teoretis: korespondensi Curry–Howard
   Menurut korespondensi Curry–Howard, tipe (Type) berkorespondensi dengan proposisi (Proposition), dan program (Program) berkorespondensi dengan pembuktian (Proof) atas proposisi tersebut.
   Dalam sudut pandang ini, type checking ditafsirkan sebagai proses memverifikasi apakah sebuah program memenuhi proposisi tertentu.

3. Korespondensi antara fitur TypeScript dan struktur logika
   Tulisan ini menghubungkan fitur-fitur utama TypeScript sebagai berikut.

• tipe fungsi → implikasi logis (Implication)
• generik → kuantifikasi universal (Universal Quantification)
• conditional type / type narrowing → analisis kasus (Case Analysis)
  Melalui ini, dijelaskan mengapa ekspresi tipe tertentu terasa alami,
  dan mengapa beberapa tipe sulit diekspresikan secara struktural.

4. Batasan sistem tipe dan pilihan desain
   Dari sudut pandang ini, pembatasan dan keterbatasan TypeScript dipahami bukan sebagai “kekurangan fitur”, melainkan sebagai pilihan desain untuk menjaga konsistensi logis.
   Tulisan ini tidak berfokus pada teknik atau trik praktis, melainkan pada filsafat dan latar belakang matematis yang membentuk sistem tipe tersebut.

[pjh2568]

Saya sangat menikmati membacanya, terima kasih.

[devjeonghwan]

Meski dibilang ini bukan linting.. kalau ingin membuktikan bahwa pemeriksaan tipe adalah pemenuhan Contract yang ketat, bukankah kontrak itu seharusnya dipaksakan pada biner dan runtime? Kalau tidak, saya rasa itu tetap hanya linting tipe pada level sintaks yang masih mengambang.

[tsboard]

Ini konten yang sangat mengesankan. Saya baru tahu bahwa ini bisa dilihat dari sudut pandang seperti ini. Saya juga membagikan tautan blog ini di kantor agar rekan-rekan saya juga sempat membacanya. Terima kasih!