ประเภทพิสูจน์ได้อย่างไร — ระบบประเภทของ TypeScript และความสอดคล้องแบบ Curry–Howard

สรุป:

• นำเสนอมุมมองที่ตีความระบบประเภทของ TypeScript ไม่ใช่แค่ตัวตรวจสอบประเภทแบบสถิตอย่างง่าย แต่เป็นระบบการพิสูจน์ของตรรกะ
• อธิบายในเชิงแนวคิดว่าเหตุใดการอนุมานประเภทจึงเป็นไปได้ โดยอิงจากความสอดคล้องแบบ Curry–Howard (Type = Proposition, Program = Proof)
• อธิบายโดยจับคู่ความสามารถของ TypeScript เช่น ประเภทฟังก์ชัน, generic, conditional type, การทำ type narrowing เข้ากับนัยเชิงตรรกะ, การหาปริมาณแบบสากล, และการวิเคราะห์เป็นกรณี
• ตีความกระบวนการตรวจสอบประเภทว่าไม่ใช่การใช้กฎทีละข้อ แต่เป็นกระบวนการตรวจสอบความสัมพันธ์ระหว่างประพจน์
• โฟกัสที่ฉากหลังด้านการออกแบบและโครงสร้างทางคณิตศาสตร์ของระบบประเภทใน TypeScript มากกว่ารายละเอียดของการติดตั้งใช้งาน

สรุปโดยละเอียด:

1. พื้นหลัง: ทำไมการอนุมานประเภทจึงเป็นไปได้?
   ในภาษาแบบ static type การอนุมานประเภทมักถูกอธิบายว่าเป็นปัญหาเชิง implementation ว่า “คอมไพเลอร์จับคู่ประเภทได้อย่างไร”
   บทความนี้ถอยออกไปอีกหนึ่งระดับ และตั้งคำถามว่าทำไมการอนุมานประเภทจึงเป็นสิ่งที่เป็นไปได้ตั้งแต่ต้น
   คำตอบที่นำเสนอคือการมองระบบประเภทในฐานะระบบการพิสูจน์ของตรรกะ

2. พื้นฐานทางทฤษฎี: ความสอดคล้องแบบ Curry–Howard
   ตามความสอดคล้องแบบ Curry–Howard ประเภท (Type) สอดคล้องกับประพจน์ (Proposition) และโปรแกรม (Program) สอดคล้องกับบทพิสูจน์ (Proof) ของประพจน์นั้น
   จากมุมมองนี้ การตรวจสอบประเภทสามารถตีความได้ว่าเป็นกระบวนการตรวจสอบว่าโปรแกรมสอดคล้องกับประพจน์ที่กำหนดหรือไม่

3. การจับคู่ระหว่างความสามารถของ TypeScript กับโครงสร้างเชิงตรรกะ
   บทความเชื่อมโยงความสามารถหลักของ TypeScript ดังนี้

• ประเภทฟังก์ชัน → นัยเชิงตรรกะ (Implication)
• generic → การหาปริมาณแบบสากล (Universal Quantification)
• conditional type / การทำ type narrowing → การวิเคราะห์เป็นกรณี (Case Analysis)
  ผ่านสิ่งนี้ บทความอธิบายว่าทำไมรูปแบบการแสดงประเภทบางอย่างจึงดูเป็นธรรมชาติ
  และทำไมบางประเภทจึงแสดงออกมาในเชิงโครงสร้างได้ยาก

4. ข้อจำกัดของระบบประเภทและทางเลือกในการออกแบบ
   จากมุมมองนี้ ข้อจำกัดและขอบเขตของ TypeScript ไม่ได้ถูกเข้าใจว่าเป็น “การขาดฟีเจอร์” แต่เป็นทางเลือกในการออกแบบเพื่อรักษาความสอดคล้องทางตรรกะ
   บทความนี้ไม่ได้เน้นเทคนิคหรือทริกสำหรับงานจริง แต่เน้นอธิบายว่าระบบประเภทถูกสร้างขึ้นบนปรัชญาและฉากหลังทางคณิตศาสตร์แบบใด

[pjh2568]

อ่านได้สนุกมาก ขอบคุณครับ

[devjeonghwan]

แม้จะบอกว่าไม่ใช่การลินต์ก็ตาม.. แต่ถ้าจะพิสูจน์ว่าการตรวจสอบประเภทเป็นการบังคับให้ทำตาม Contract อย่างเคร่งครัด ก็น่าจะต้องมีการบังคับใช้ Contract นั้นในระดับไบนารีและรันไทม์ด้วยไม่ใช่หรือ? ถ้าไม่เป็นเช่นนั้น ผมก็รู้สึกว่ามันยังคงเป็นเพียง type linting ในสภาพที่ลอยๆ ทางวากยสัมพันธ์อยู่ดี

[tsboard]

เป็นเนื้อหาที่น่าประทับใจมากครับ เพิ่งรู้เป็นครั้งแรกเลยว่ามองในมุมนี้ได้ด้วย ผมเลยแชร์ลิงก์บล็อกนี้ในบริษัท พร้อมบอกเพื่อนร่วมงานให้ลองอ่านกันดูด้วย ขอบคุณครับ!