ทำไมจึงไม่ใช้ dependent types

 (lawrencecpaulson.github.io)
1 คะแนน โดย GN⁺ 2025-11-04 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • dependent types (ทฤษฎีชนิด) มี proof objects รวมอยู่ด้วย แต่ผู้เขียนมองว่านี่เป็น โครงสร้างที่ไม่จำเป็นและไม่มีประสิทธิภาพ
  • ผู้เขียนเคยศึกษาระบบที่อิง dependent types ในอดีตโดยตรง เช่น AUTOMATH และ ระบบแบบรูปของ Martin-Löf แต่ Isabelle ได้พัฒนาไปเป็น เฟรมเวิร์กเชิงตรรกะแบบทั่วไป (generic)
  • Isabelle/HOL ซึ่งอิงบน ทฤษฎีชนิดอย่างง่าย (higher-order logic) มีจุดแข็งด้าน การทำงานอัตโนมัติ, ไลบรารีขนาดใหญ่, และความอ่านง่าย
  • ผ่าน โครงการ ALEXANDRIA ได้พิสูจน์ว่า แม้ใช้เพียง higher-order logic ก็ยังสามารถ ทำ formalization ของทฤษฎีบทคณิตศาสตร์ขั้นสูง ได้
  • แม้ระบบ dependent type อย่าง Lean จะเติบโตขึ้นมากแล้ว ผู้เขียนก็ยังคงมองว่า แนวทาง higher-order logic ใช้งานได้จริงกว่า เพราะ ปัญหาด้านประสิทธิภาพและความซับซ้อน

dependent types และ proof objects

  • ใน dependent type theory นั้น proof objects เป็นองค์ประกอบที่ขาดไม่ได้ แต่ผู้เขียนมองว่านี่เป็น การสิ้นเปลืองพื้นที่
    • ในสถาปัตยกรรมแบบ LCF สามารถบังคับให้รันได้เฉพาะขั้นตอนพิสูจน์ที่ถูกต้อง ผ่าน การตรวจสอบชนิดในระดับภาษา implementation ไม่ใช่ภายในตัวตรรกะเอง
    • จากแนวคิดของ Robin Milner จึงเกิดแนวคิด proof kernel ซึ่งกลายมาเป็นรากฐานของ Isabelle
  • เมื่อถูกถามว่าทำไม “ไม่ใช้ dependent types” ผู้เขียนตอบว่า “จริง ๆ ใช้มานานมากแล้ว”

ประสบการณ์กับ AUTOMATH

  • ในปี 1977 ที่ Caltech ผู้เขียนได้ฟังบรรยายเรื่อง AUTOMATH โดย N. G. de Bruijn แต่ไม่ได้ใช้ระบบด้วยตนเอง
    • เพราะในเวลานั้น ระบบของมหาวิทยาลัย Eindhoven ไม่ได้เชื่อมกับ ARPAnet และต้องใช้คอมพิวเตอร์ที่อิง ALGOL 60
  • AUTOMATH เป็น ระบบ dependent type แต่ไม่ได้ทำ Curry–Howard correspondence ให้เป็นรูปธรรม
    • ผู้ใช้ต้องเพิ่ม สัญลักษณ์และกฎการอนุมาน ของตรรกะที่ต้องการเองในรูปของสัจพจน์
    • de Bruijn เปรียบสิ่งนี้ว่าเป็น “ร้านอาหารขนาดใหญ่ที่มีอาหารทุกอย่างให้เลือก”
  • Isabelle รับช่วงแนวคิดนี้ต่อมา โดยมุ่งสู่ ความเป็นทั่วไปในฐานะ logical framework
    • แต่ de Bruijn ไม่ชอบทฤษฎีเซต และมองว่าคณิตศาสตร์นั้นมีธรรมชาติเป็น type-based โดยแท้
  • ผู้เขียนเคยถามถึง การตรวจสอบความถูกต้อง ของ AUTOMATH และ de Bruijn ก็ส่ง ตำราทฤษฎีภาษาขนาด 300 หน้า มาให้ แต่ก็ยังไม่เป็นที่น่าพอใจ

ทฤษฎีแบบรูปของ Martin-Löf

  • ผู้เขียนศึกษาทฤษฎีแบบรูปของ Martin-Löf ที่ มหาวิทยาลัย Chalmers ใน Göteborg และหลงใหลในความเป็นไปได้ของ program synthesis
    • ผู้เขียนมองว่านี่ “ถูกต้อง” อย่างชัดเจน เพราะเป็นการทำให้หลักของ ตรรกะญาณทัศน์นิยมของ Heyting กลายเป็นระบบที่ใช้งานได้จริงโดยตรง
  • ผู้เขียนทำวิจัยเรื่องนี้อยู่หลายปี และเคยสร้าง Isabelle เวอร์ชันแรก ๆ บนพื้นฐานของทฤษฎี Martin-Löf
    • ปัจจุบันยังรวมอยู่ในการแจกจ่ายในชื่อ Isabelle/CTT
  • แต่ต่อมางานวิจัยนี้ก็สะดุดลงจากทั้ง บรรยากาศเชิงยึดติดแนวคิดของ Per Martin-Löf และการบังคับให้เปลี่ยนไปใช้ intensional equality
  • ระบบที่ตามมาภายหลัง เช่น Calculus of Constructions (CoC), Rocq, และ Lean ก็ยังทิ้งคำถามลักษณะเดียวกันไว้
    • CoC ผ่านการเปลี่ยนแปลงหลายรูปแบบและการเพิ่มสัจพจน์แบบเลือกใช้มาตลอดหลายทศวรรษ

การเลือกแนวทางวิจัยและทิศทางของ Isabelle

  • นักวิจัยต้องเลือกระหว่าง การพัฒนาระบบแบบรูปใหม่ กับ การขยายและใช้งานระบบเดิมให้กว้างขึ้น
    • Isabelle ถูกออกแบบให้เป็น เฟรมเวิร์กแบบทั่วไป ที่รองรับตรรกะได้หลากหลายแบบ
  • ในปี 1985 Mike Gordon ใช้ ทฤษฎีชนิดอย่างง่ายของ Church สำหรับการตรวจพิสูจน์ฮาร์ดแวร์
    • ต่อมา John Harrison ได้คิดวิธี encoding มิติของเวกเตอร์ขึ้นมา
  • Isabelle/HOL ได้เพิ่ม axiomatic type classes และ ระบบโมดูล locale เข้าไปบนทฤษฎีของ Church
  • ฝั่งชุมชน Lean ซึ่งอิง CoC ก็ประสบความสำเร็จในการสร้าง mathlib ซึ่งเป็นงาน formalization ทางคณิตศาสตร์ขนาดมหาศาล

โครงการ ALEXANDRIA และการทดสอบขีดจำกัดของ higher-order logic

  • โครงการ ALEXANDRIA ที่ได้รับทุนจาก ERC เน้นจุดเด่นของ Isabelle ด้าน automation, ไลบรารี, และความอ่านง่าย
  • ในตอนแรกคาดว่า higher-order logic น่าจะมีข้อจำกัด แต่ในทางปฏิบัติกลับสามารถทำ formalization ของคณิตศาสตร์ระดับสูงอย่าง Grothendieck schemes ได้สำเร็จ
    • Paulo Emílio de Vilhena และ Martin Baillon ได้พิสูจน์ว่า ทุก field มี algebraically closed extension
  • โครงการยังขยายไปถึงผลลัพธ์ขั้นสูงอย่าง ทฤษฎีบท Balog–Szemerédi–Gowers
    • ข้ออ้างที่ว่า “หากไม่มี dependent types ก็ทำ formalization คณิตศาสตร์ไม่ได้” จึงแทบหายไป เหลือเพียงข้ออ้างว่า “dependent types ดูสะอาดกว่า”

Lean และมุมมองปัจจุบันต่อ dependent types

  • ผู้เขียนอิจฉาขนาดของ ชุมชน Lean และเครื่องมือ Blueprint แต่เห็นว่า ปัญหาด้านประสิทธิภาพและความซับซ้อน ยังไม่ได้หายไป
    • มีการรายงานซ้ำ ๆ ถึงปัญหาการปะทะกับ intensional equality และความยากในการตัดสินใจว่า เมื่อใดควรใช้ dependent types
  • ผู้เขียนเปรียบ dependent types กับ ระบบขับขี่อัตโนมัติเต็มรูปแบบ (Full Self-Driving) ของ Tesla เพื่อชี้ให้เห็นถึง ความคาดหวังที่สูงเกินจริงและความไม่สะดวกในการใช้งานจริง

ภาคผนวก: ข้อจำกัดเชิงทฤษฎีของ higher-order logic

  • บางคนอ้างว่า higher-order logic อ่อนกว่าในเชิง proof theory แต่สิ่งนี้หมายถึงเพียงว่า อ่อนกว่าเมื่อเทียบกับทฤษฎีเซต ZF
  • ตามผลลัพธ์ของ ALEXANDRIA higher-order logic ก็ยังสามารถรับมือกับ โครงสร้างคณิตศาสตร์ที่ซับซ้อนอย่าง Grothendieck schemes ได้
    • มีเพียงสองบทพิสูจน์เท่านั้นที่ต้อง เพิ่มสัจพจน์ ZF และทั้งสองกรณีก็เป็น ทฤษฎีบทที่กล่าวถึงวัตถุของ ZF โดยตรง

เชิงอรรถ

  • ญาณทัศน์นิยม เป็นปรัชญาที่มองภาษาเป็นเพียงเครื่องมือสำหรับการบันทึก ซึ่งต่างจาก constructive mathematics ในความหมายปัจจุบัน

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2025-11-04
ความคิดเห็นบน Hacker News

  • dependent types มีประโยชน์มากในบางสถานการณ์
    ตัวอย่างเช่น คิดว่าน่าจะดีถ้า Python สามารถแสดงและตรวจชนิดของ “เมทริกซ์ float32 ขนาด 10×5” เป็น type ได้
    แต่แนวคิดที่มองว่าการพิสูจน์กับ type เป็นสิ่งเดียวกัน เช่น Curry–Howard correspondence นั้น ทำให้คนสับสนได้
    type error ให้ความรู้สึกเหมือนเป็นแค่ความผิดพลาดที่แก้ได้ แต่ proof error เป็นปัญหาที่ซับซ้อนกว่าและต้องใช้การคิดมากกว่า
    เพราะแบบนั้นจึงมองว่าจุดแข็งที่แท้จริงของ Lean ไม่ใช่ระบบ type แต่เป็น ชุมชนและโครงสร้างโอเพนซอร์สของ mathlib
    ขณะที่ AFP ของ Isabelle ดำเนินการคล้ายวารสารวิชาการ Lean กลับมีการทำงานร่วมกันผ่าน pull request อย่างคึกคัก
    ตอนนี้ฉันกำลังพัฒนา theorem prover ตัวใหม่ชื่อ Acorn(acornprover.org) และพยายามรวมข้อดีของ Lean กับ Isabelle เข้าด้วยกัน
    ความสามารถในการแสดงออกของ dependent types แบบเรียบง่ายใน Lean นั้นดี แต่ถ้าใช้ลึกเกินไปจะดีบักยาก

    • ใน C++ หรือ Rust ก็สามารถแสดง type แบบนี้ได้เช่นกัน ถ้าเป็นอาร์เรย์ขนาดคงที่
      เพียงแต่ไม่สามารถรับประกันช่วงของดัชนีที่รู้ได้เฉพาะตอนรันไทม์ตั้งแต่ตอนคอมไพล์ได้
      ภาษา dependent type ที่แท้จริงสามารถ ป้องกัน runtime error ในระดับ type ได้
    • ด้วย const generics ของ Rust หรือ non-type template parameter ของ C++ ก็ทำได้เพียงพอแล้ว
      ในทางปฏิบัติ แม้แต่ในภาษา dependent type เองก็ไม่ค่อยใช้ dependent type เพื่อป้องกัน runtime error
      แต่จะใช้หลัก ๆ กับ invariant ของโครงสร้างข้อมูล หรือการตรวจพิสูจน์ภายหลังการนิยามโปรแกรม
      ดูเพิ่มเติม: division-by-zero in type theory FAQ, สไลด์ของ Xavier Leroy
    • ใน TypeScript ก็พอเลียนแบบ dependent type ได้เล็กน้อย
      ตัวอย่างเช่น สามารถใช้ type แสดงขนาดเมทริกซ์ได้เหมือนที่บรรทัด 38 ของโค้ดนี้
      และยังทำ นิยาม type ของเวกเตอร์ หรือ
      type ของผลลัพธ์การคูณเมทริกซ์ ได้ด้วย
      แต่ตอนนี้ยังเป็นแค่การทดลองในระดับโปรเจกต์ส่วนตัว และอาจไม่เหมาะกับโปรเจกต์ข้อมูลขนาดใหญ่
    • คำพูดที่ว่า “proof เท่ากับ type” น่าสนใจมาก
      เรื่องนี้เกี่ยวข้องกับแนวคิด Propositions as Types
      จึงสงสัยว่า dependent type ทำงานอย่างไรในรันไทม์ และจำเป็นต้องมีทั้งการคอมไพล์และการตรวจ type ตอนรันไทม์หรือไม่
      อีกทั้งยังสงสัยว่าตอน implement จะเกิด ความซับซ้อนจากการอ้างอิงทางอ้อมจำนวนมาก หรือเปล่า
    • คำพูดว่า “อยากแสดง type ของเมทริกซ์ 10×5 ใน Python” สุดท้ายก็หมายถึงแค่ให้สร้างเป็นคลาสขึ้นมาเองไม่ใช่หรือ?

  • ข้อโต้แย้งของ Dr. Paulson ไม่ใช่ว่า dependent type แย่ แต่คือ มันไม่จำเป็นเสมอไป
    น่าจะดีถ้ามีการพูดถึงปัญหาด้านประสิทธิภาพของ Lean หรือประเด็นเรื่อง intensional equality มากกว่านี้
    กรณีอย่าง HEq ของ Isabelle(ลิงก์) ซึ่งไม่ใช่ definitional equality อาจก่อปัญหาได้
    เพราะอย่างนั้นฉันจึงคิดว่าควรใช้ dependent type ให้น้อยที่สุดเท่าที่ทำได้
    แม้แต่ระบบอย่าง ACL2 ที่ไม่มี static type ก็ยังตรวจพิสูจน์ได้เพียงพอ
    ท้ายที่สุด สิ่งสำคัญคือ สมดุลระหว่างการใช้งานจริงกับความสามารถในการตรวจพิสูจน์

    • ในมุมของ software verification นั้น Isabelle (non-dependent type) ก็ทรงพลังเพียงพออยู่แล้ว
      ส่วน Lean หรือ Agda ยังถูกใช้กับงานตรวจพิสูจน์ระดับอุตสาหกรรมน้อยกว่า
      การเปรียบเทียบ Concrete Semantics(ลิงก์) กับ Logical Verification 2025(ลิงก์) ก็น่าสนใจ
      ในโลกจริง refinement types อาจใช้งานได้จริงมากกว่า
      ตัวอย่าง: Rust Creusot, Dafny, และ ตัวอย่างพิสูจน์ leftpad ของ LiquidHaskell
    • ในคณิตศาสตร์ dependent type ทำงานได้ดี เพราะเราไม่ได้ใช้ proof เป็นโปรแกรม
      แต่ในการตรวจพิสูจน์โปรแกรม จะต้องมี lemma ที่ซับซ้อน อย่างเช่น “proof สองอันนี้เหมือนกัน” ซึ่งมักพิสูจน์ไม่ได้
    • อยากรู้เหตุผลว่าทำไมถึงบอกว่า “ควรใช้ dependent type ให้น้อยที่สุดเท่าที่ทำได้”
    • คำกล่าวว่า “ไม่จำเป็น” ฟังดูเหมือนการหลบประเด็น
      ประเด็นสำคัญไม่ใช่ว่ามันจำเป็นต่อการมีอยู่หรือไม่ แต่คือ มันมีประโยชน์แค่ไหน
      สุดท้ายแล้วการเลือกเครื่องมือก็เป็นเรื่องของ รสนิยมของนักพัฒนาและประสิทธิภาพ

  • น่าสนใจที่ข้อถกเถียงในตรรกศาสตร์สมัยใหม่จำนวนมากลงเอยที่ ความชอบเชิงสุนทรียะ
    ถ้ามีข้อดีเชิงปฏิบัติที่เหนือกว่ามากจริง ก็คงไม่มีการถกเถียงกัน
    อนึ่ง งานเขียนปี 1999 ของ Paulson และ Lamport “Typing in Specification Languages” เป็นงานอ่านที่ดีมาก
    หลังจากนั้นก็มีแนวทางอย่าง TLA+ ของ Lamport ซึ่งเป็น formalism แบบไม่เป็นทางการ พัฒนาต่อมา

    • ฉันมองว่านี่ไม่ใช่แค่เรื่องของความงาม แต่เป็น เรื่องของ trade-off
      เราได้ประโยชน์จากหลักประกันตอนคอมไพล์ แต่ต้องแลกกับความซับซ้อนและเวลา build ที่เพิ่มขึ้น
      สุดท้ายคำถามสำคัญคือ “การแลกเปลี่ยนนั้นคุ้มค่าหรือไม่”

  • ปัญหาของ HOL (simple type theory) ไม่ใช่เรื่องการพึ่งพา แต่คือ ความแข็งแรงทางตรรกะที่ไม่พอ
    มันเทียบเท่ากับทฤษฎีเซตของ Zermelo แบบจำกัด และอ่อนเกินไปสำหรับการทำให้คณิตศาสตร์สมัยใหม่เป็นแบบ formal อย่างสมบูรณ์
    โดยเฉพาะอย่างยิ่ง จัดการปัญหาเรื่องขนาดใน category theory ได้ยาก

    • มีกรณีที่ใช้ ฟีเจอร์ locales ของ Isabelle เพื่อ formalize Grothendieck scheme
      จึงสงสัยว่ามันต่างจากสไตล์ของนักคณิตศาสตร์จริง ๆ มากแค่ไหน
    • หากต้องการเพิ่มความแข็งแรงทางตรรกะ ก็สามารถ เพิ่มสัจพจน์ ได้
      ตัวอย่างเช่น การเพิ่ม ‘inaccessible cardinal’ จะทำให้คล้ายกับแนวคิดเรื่อง ‘universe’ ใน type theory

  • ฉันเคยเรียนด้าน formal methods และเคยคิดว่า dependent type เท่มาก แต่พอใช้จริงกลับ เป็นงานที่ฝ่าความยากตลอดเวลา
    ตอนใช้ F# ก็เคยพยายามนำ F* เข้ามา แต่เพื่อนร่วมทีมรู้สึกว่าช่วงการเรียนรู้ทางคณิตศาสตร์นั้นหนักเกินไป
    สุดท้ายเลยได้ข้อสรุปแบบประชด ๆ ว่า เครื่องมือที่มีคณิตศาสตร์เยอะ ๆ วิศวกรมักไม่ค่อยเรียนกัน

    • F* เน้น software verification มากกว่าคณิตศาสตร์ จึงคนละแนวกับ Lean
      มันใช้การแก้ constraint แบบอาศัย SMT เพื่อให้ใช้ dependent type แบบเบา ๆ ได้
      แต่ก็ไม่ได้ตอบคำถามเชิงปรัชญาว่า “นี่ถูกต้องจริงหรือไม่”
      โลกของการพิสูจน์ทางคณิตศาสตร์กับการตรวจพิสูจน์ซอฟต์แวร์นั้นต่างกันพอสมควร
    • คนเราไม่ได้ไม่เรียนสิ่งใหม่ แต่แค่ ตัดสินว่าผลตอบแทนต่อการลงทุนนั้นไม่คุ้ม
      ท้ายที่สุดเวลาเป็นทรัพยากรที่จำกัด

  • ที่บริษัท Phosphor ของเรา กำลังทดลองผสาน dependent type เข้ากับคำสั่ง query ฐานข้อมูล/กราฟ
    เพื่อชดเชยข้อจำกัดของ RDF และสร้าง ระบบ query ที่อิงตรรกะ ได้
    ในทางปฏิบัติ เราใช้ TypeDB(typedb.com) ซึ่งเร็วกว่า MongoDB และมีประโยชน์กับการทำ data modeling ที่ซับซ้อน
    แนวคิดนี้ก็คล้ายกับ ontology ของ Palantir

    • อยากให้ช่วยอธิบายข้อความ “สร้าง growth engine แบบ non-dilutive” ให้เป็นรูปธรรมกว่านี้ได้ไหม
    • อยากรู้เหตุผลที่เลือก TypeDB และ ตัวเลขประสิทธิภาพ ที่ใช้งานจริง

  • สุดท้ายแล้วความลับของ dependent type เหมือนจะอยู่ที่ การรู้ว่าเมื่อไรไม่ควรใช้มัน
    แทนที่จะวิจารณ์ Lean หรือ Rocq อาจเป็นไปได้ไหมว่าในบางสถานการณ์ควรใช้แนวทางแบบ Isabelle

  • โปรเจกต์ Alexandria(ลิงก์) ของทีมวิจัย Paulson น่าประทับใจมาก
    โดยเฉพาะ งาน formalize อัลกอริทึมควอนตัมคอมพิวติ้ง(ลิงก์บทความ) ที่น่าสนใจ

  • เมื่อก่อนฉันเชื่อว่า dependent type คืออนาคต แต่ในโปรเจกต์จริง ผลกระทบต่อ productivity สูงมากในทางลบ
    ตอนนี้ฉันชอบโซลูชันที่ชัดเจนและดูแลรักษาง่ายมากกว่า
    ถ้าทีมเข้าใจและขยายต่อได้ เครื่องมือนั้นก็คือเครื่องมือที่ดี

  • ฉันชอบระบบ type ที่อยู่ บริเวณขอบเขตของ dependent type มากกว่าตัวเต็มรูปแบบ
    ตัวอย่างเช่น Purescript มี row-type ที่ทรงพลังกว่า Haskell มาให้เป็นพื้นฐาน
    และยังรองรับ list, string, และ regular expression ระดับ type ด้วย
    สามารถนำไปใช้ในลักษณะของ logic programming ที่อิง typeclass ได้