ควรอ่านสัญกรณ์ของระบบชนิดข้อมูลอย่างไร?

• แม้สัญกรณ์ของระบบชนิดข้อมูลจะแตกต่างกันไปตามเอกสาร แต่ถ้าเข้าใจกรอบร่วมอย่าง ไวยากรณ์, ความสัมพันธ์การกำหนดชนิด, และกฎอนุมาน ก็จะตามรูปแบบส่วนใหญ่ได้
• ระบบชนิดข้อมูลทำงานบน ไวยากรณ์เชิงนามธรรม ของภาษา ดังนั้นก่อนอื่นต้องแยกพจน์ (term) ที่มีชนิดออกจากตัวชนิดเองด้วยไวยากรณ์
• ⊢ e: τ คือ การตัดสินการกำหนดชนิด ที่หมายความว่า “นิพจน์ e มีชนิด τ” และให้อ่านกฎอนุมานว่า หากเงื่อนไขทั้งหมดเหนือเส้นแนวนอนเป็นจริง ข้อสรุปด้านล่างก็เป็นจริงด้วย
• เมื่อมีตัวแปรและฟังก์ชันเข้ามา จะมี บริบท แนบมาเช่น Γ ⊢ e: τ เพื่อคอยติดตามชื่อตัวแปรและชนิดในสโคปปัจจุบัน
• กฎการกำหนดชนิดจำนวนมากอ่านได้เหมือนฟังก์ชันตรวจสอบชนิดแบบเรียกซ้ำ แต่ไม่ใช่ทุกการตัดสินเชิงตรรกะที่จะกลายเป็น อัลกอริทึม ตรวจสอบชนิดที่ตัดสินได้โดยตรง

---

สัญกรณ์ระบบชนิดข้อมูลที่เริ่มจากไวยากรณ์

• ระบบชนิดข้อมูลเป็น ระบบเชิงไวยากรณ์ ของภาษาโปรแกรม และเป็นชุดกฎที่ทำงานกับไวยากรณ์เชิงนามธรรมของภาษา
• คำอธิบายระบบชนิดข้อมูลแบบครอบคลุมมักนำเสนอโครงสร้างไวยากรณ์ที่กล่าวถึงด้วย ไวยากรณ์ ก่อน แล้วเขียนด้วยสัญกรณ์ BNF
• แม้ในภาษาชนิดข้อมูลที่ง่ายที่สุด ไวยากรณ์ก็แบ่งได้เป็นสองหมวดใหญ่
  • e: นิพจน์ (expression) ที่มีชนิด
  • τ: ชนิด (type) ที่แนบกับนิพจน์
• ภาษาตัวอย่างมีลิเทอรัลบูลีน ลิเทอรัลจำนวนเต็ม นิพจน์เงื่อนไข การดำเนินการเลขคณิต และการเปรียบเทียบเป็นนิพจน์ และใช้ Bool กับ Int เป็นชนิด
• สัญลักษณ์ชนิดอาจเขียนเป็น t, T, σ หรืออักษรกรีกตัวพิมพ์เล็กอื่น ๆ แทน τ ได้ ขึ้นอยู่กับเอกสาร แต่โครงสร้างโดยรวมคล้ายกัน
• ภาษาที่ซับซ้อนกว่านี้อาจมีหมวดไวยากรณ์เพิ่มขึ้น เช่น คำสั่ง หรือแพตเทิร์นของ pattern matching

การอ่านความสัมพันธ์และการตัดสินการกำหนดชนิด

• หลังจากกำหนดไวยากรณ์แล้ว โดยทั่วไปจะนิยาม ความสัมพันธ์การกำหนดชนิด ในรูป e : τ
  • 1 + 2 : Int หมายความว่า “1 + 2 มีชนิด Int”
  • 1 + 2 : Bool หมายความว่านิพจน์เดียวกันมีชนิด Bool ซึ่งจึงไม่ถูกต้อง
  • true + 2 : Int เป็นนิพจน์ที่ตัวมันเองไม่สมเหตุสมผล จึงไม่มีชนิดใด
• ⊢ e : τ คือ การตัดสินการกำหนดชนิด และ ⊢ อ่านได้ว่า “ประโยคด้านหลังเป็นจริง”
• กฎที่ไม่มีอะไรอยู่เหนือเส้นแนวนอนคือ สัจพจน์ (axiom) ที่เป็นจริงเสมอ
  • ⊢ true : Bool
  • ⊢ false : Bool
  • กฎลิเทอรัลจำนวนเต็ม เช่น ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
• กฎที่มีทั้งด้านบนและด้านล่างของเส้นแนวนอนคือ กฎอนุมาน
  • หากเงื่อนไขด้านบนทั้งหมดเป็นจริง ข้อสรุปด้านล่างก็เป็นจริง
  • ถ้า e₁ และ e₂ เป็น Int ทั้งคู่ e₁ + e₂ จะเป็น Int
  • ถ้า e₁ และ e₂ เป็น Int ทั้งคู่ e₁ < e₂ จะเป็น Bool

นิพจน์เงื่อนไขและตัวแปรชนิด

• สองกิ่งของ if ... then ... else ... จะเป็นชนิดใดก็ได้ แต่ต้องเป็นชนิดเดียวกัน
  • if true then 1 else 2 ทำได้
  • if true then false else true ทำได้
  • if true then 1 else true ทำไม่ได้
• เพื่อแสดงสิ่งนี้ กฎจึงใช้ตัวแปร τ แทนชนิดของกิ่ง
  • นิพจน์เงื่อนไข e₁ ต้องเป็น Bool
  • กิ่ง then คือ e₂ และกิ่ง else คือ e₃ ต้องมีชนิด τ เดียวกัน
  • ชนิดของนิพจน์เงื่อนไขทั้งหมดก็เป็น τ ด้วย
• เมื่อใช้กฎ สามารถเลือกชนิดใดก็ได้ให้เป็น τ แต่ภายในกฎเดียวกันต้องรักษาการเลือกนั้นให้สอดคล้องกัน

อ่านกฎอนุมานเหมือนอัลกอริทึม

• สัญกรณ์นี้มาจากตรรกะเชิงรูปนัย และวิธีระบุระบบชนิดข้อมูลมีลักษณะคล้าย natural deduction เป็นพิเศษ
• กฎลักษณะนี้ใช้สร้างพิสูจน์เชิงรูปนัยเกี่ยวกับคุณสมบัติของระบบ และสำคัญต่อการพิสูจน์คุณสมบัติอย่าง type safety
• การตัดสินเชิงตรรกะไม่ได้สอดคล้องกับอัลกอริทึมตรวจสอบชนิดที่ตัดสินได้โดยตรงเสมอไป
• ในหลายกรณี สามารถอ่าน ⊢ e : τ เหมือน ฟังก์ชัน ที่รับนิพจน์ e แล้วได้ชนิด τ
  • โดยทั่วไปแต่ละรูปแบบของนิพจน์ในไวยากรณ์จะมีกฎหนึ่งกฎ
  • กฎการกำหนดชนิดแต่ละข้อสามารถมองเป็นแขนงหนึ่งของฟังก์ชันตรวจสอบชนิดแบบเรียกซ้ำได้
• ฟังก์ชัน infer ในตัวอย่างสอดคล้องกับลำดับต่อไปนี้
  • true หรือ false เป็น Bool
  • ลิเทอรัลจำนวนเต็มเป็น Int
  • e₁ + e₂ ตรวจสอบก่อนว่าผลอนุมานของทั้งสองฝั่งเป็น Int ทั้งคู่ แล้วจึงให้เป็น Int
  • e₁ < e₂ ตรวจสอบก่อนว่าทั้งสองฝั่งเป็น Int ทั้งคู่ แล้วจึงให้เป็น Bool
  • if e₁ then e₂ else e₃ ตรวจสอบว่าเงื่อนไขเป็น Bool และตรวจสอบว่าสองกิ่งมีชนิดเดียวกัน แล้วคืนชนิดนั้น
• แม้จะย้ายไปเป็นอัลกอริทึมโดยตรงไม่ได้ แต่ถ้าคิดว่าใน judgment นั้น e เป็นอินพุต และ τ เป็นเอาต์พุต ก็จะเข้าใจการไหลของข้อมูลได้ง่ายขึ้น

ตัวแปรและบริบท

• หากต้องการ扱กับภาษาโปรแกรมที่ใช้งานได้จริง จำเป็นต้องมี ตัวแปร และตัวอย่างจะขยายด้วยการเพิ่มฟังก์ชันให้เป็นรูปแบบ simply typed lambda calculus
• ไวยากรณ์ที่ขยายแล้วประกอบด้วย
  • ตัวแปร x
  • การนิยามฟังก์ชันแบบนามธรรม λx:τ. e
  • การประยุกต์ใช้ฟังก์ชัน e e
  • ชนิดฟังก์ชัน τ → τ
• λx:τ. e สอดคล้องกับ (x:τ) => e ใน TypeScript และ f x สอดคล้องกับ f(x)
• ชนิดของตัวแปรขึ้นอยู่กับ บริบท ที่ตัวแปรปรากฏ ดังนั้นจึงไม่สามารถเขียนกฎในรูปง่าย ๆ อย่าง ⊢ x : ??? ได้
• ดังนั้นการตัดสินการกำหนดชนิดจึงขยายเป็น Γ ⊢ e : τ
  • Γ คือบริบทหรือสภาพแวดล้อมของชนิด
  • ⊢ แยกสมมติฐานตามบริบททางซ้ายออกจากประโยคที่ต้องพิสูจน์ทางขวา
  • อ่านว่า “ภายใต้บริบท Γ นิพจน์ e มีชนิด τ”
• ในเชิงอัลกอริทึม Γ มองได้เหมือนอินพุตเพิ่มเติมในรูป Map<Variable, Type>
• ในเชิงรูปนัย บริบทเองก็ถูกระบุเป็นโครงสร้างไวยากรณ์ด้วย
  • ∅: บริบทว่าง
  • Γ, x:τ: บริบทที่เพิ่ม binding ของตัวแปร
  • บางครั้งใช้ • เป็นบริบทว่างแทน ∅
• ในการแทนแบบนี้ บริบทมีลักษณะใกล้เคียงกับ association list ที่แมปชื่อตัวแปรไปยังชนิด

สิ่งที่บริบททำภายในกฎ

• กฎการกำหนดชนิดจำนวนมากไม่เปลี่ยนบริบท แต่ส่งต่อไปตามเดิม
  • Γ ⊢ true : Bool
  • ถ้า Γ ⊢ e₁ : Int และ Γ ⊢ e₂ : Int แล้ว Γ ⊢ e₁ + e₂ : Int
• ในกฎของการใช้ตัวแปรและนิพจน์แลมบ์ดา บริบทมีบทบาทสำคัญ
  • ถ้า x:τ ∈ Γ แล้ว Γ ⊢ x : τ
  • ถ้า Γ, x:τ₁ ⊢ e : τ₂ แล้ว Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
• เมื่อตรวจสอบชนิดของเนื้อหา e ในแลมบ์ดา บริบทจะถูกขยายด้วย binding ใหม่ x:τ₁
• กฎตัวแปรตัดสินว่า หากมี binding ของตัวแปรในบริบทปัจจุบัน ตัวแปรนั้นก็มีชนิดดังกล่าว
• บริบทถูกใช้เป็น กลไกสื่อสาร ที่ส่งข้อมูลระหว่างกฎแลมบ์ดากับกฎตัวแปร
• เพื่อความเรียบง่าย การระบุระบบชนิดข้อมูลด้วยวิธีนี้มักสมมติว่าตัวแปรทั้งหมดถูกแก้ความหมายแล้วและทำให้เป็นเอกลักษณ์แล้ว โดยไม่扱กับ variable shadowing
• กฎการประยุกต์ใช้ฟังก์ชันตรวจสอบชนิดของนิพจน์ฟังก์ชันและนิพจน์อาร์กิวเมนต์ร่วมกัน
  • e₁ ต้องมีชนิด τ₁ → τ₂
  • e₂ ต้องมีชนิด τ₁
  • ชนิดของการประยุกต์ทั้งหมด e₁ e₂ จะเป็น τ₂

สัญกรณ์เพิ่มเติมที่พบบ่อย

• กฎอนุมานไม่ได้เขียนในแนวตั้งเสมอไป
  • เงื่อนไขหลายข้ออาจวางเรียงกันในแนวนอนได้
  • การจัดวางแนวตั้งและแนวนอนอาจผสมกันภายในกฎเดียวกันได้
• เงื่อนไขเหนือเส้นแนวนอนมักเป็น judgment อื่น แต่ก็อาจเป็น เงื่อนไขประกอบ (side condition) ที่เป็นเงื่อนไขบูลีนใด ๆ ได้
  • x:τ ∈ Γ ในกฎตัวแปรเป็นตัวอย่าง
  • ในระบบชนิดข้อมูลเชิงอัลกอริทึม อาจใช้ α fresh ซึ่งหมายความว่า α ต้องเป็นตัวแปรชนิดใหม่ที่แยกจากตัวแปรชนิดอื่น

Subtyping

• Subtyping เป็นความสัมพันธ์ที่扱ความเข้ากันได้ระหว่างชนิดอย่างผ่อนคลายกว่าความเท่ากันแบบเคร่งครัด และต้องนิยามไว้อย่างชัดเจน
• โดยทั่วไปเขียนเป็น τ₁ <: τ₂ และอ่านว่า “τ₁ เป็น subtype ของ τ₂”
• ความสัมพันธ์ subtyping แบบง่ายอาจแนะนำชนิดบนสุด ⊤ และชนิดล่างสุด ⊥
  • τ <: τ: ทุกชนิดเป็น subtype ของตัวเอง
  • τ <: ⊤: ทุกชนิดเป็น subtype ของ ⊤
  • ⊥ <: τ: ⊥ เป็น subtype ของทุกชนิด
• กฎแรกคือกฎสะท้อน และมักย่อว่า refl
• หากต้องการอนุญาต subtyping ต้องใช้ความสัมพันธ์นี้อย่างชัดเจนในกฎการกำหนดชนิดแต่ละกฎที่อนุญาต
  • ในกฎการประยุกต์ใช้ฟังก์ชัน สามารถอนุญาตการประยุกต์ได้ถ้าชนิดของอาร์กิวเมนต์ τ₁ เป็น subtype ของชนิดพารามิเตอร์ τ₂

หลายบริบทและการตรวจสอบชนิดแบบสองทิศทาง

• ระบบชนิดข้อมูลบางระบบนิยามการตัดสินการกำหนดชนิดที่มีบริบทมากกว่าหนึ่งตัว
  • บริบทที่สองมักเรียกว่า Δ
  • Γ;Δ ⊢ e : τ มักใช้เมื่อบริบททั้งสองถูกใช้เหมือนอินพุต
  • Γ ⊢ e : τ ⊣ Δ มักใช้เมื่อ Δ ถูกใช้เหมือนเอาต์พุต
• บริบทที่สองถูกใช้ต่างกันตามวัตถุประสงค์
  • อาจใช้ให้ตัวแปรบางตัวอ้างอิงได้เฉพาะภายในนิพจน์บางอย่าง
  • ในภาษาโปรแกรมที่รับรู้ทรัพยากร อาจใช้เป็นบริบทเอาต์พุตเพื่อติดตามว่าตัวแปรใดถูกใช้หมดไปแล้ว
• การตรวจสอบชนิดแบบสองทิศทาง เป็นแนวทางที่ทำ type inference แบบไม่เป็นท้องถิ่นในขอบเขตจำกัดโดยไม่ใช้ตัวแก้ constraint
• ระบบแบบสองทิศทางแบ่ง judgment ทั่วไป Γ ⊢ e : τ ออกเป็น judgment เฉพาะสองแบบ
  • Γ ⊢ e ⇐ τ: judgment สำหรับ การตรวจสอบ (checking) ว่านิพจน์ e มีชนิดที่คาดหวัง τ หรือไม่ โดยในเชิงอัลกอริทึม τ เป็นอินพุต
  • Γ ⊢ e ⇒ τ: judgment สำหรับ การอนุมาน (inference) ที่ใช้เมื่อไม่มีข้อมูลชนิดที่คาดหวัง โดยในเชิงอัลกอริทึม τ เป็นเอาต์พุต
• judgment ทั้งสองถูกนิยามแบบเรียกซ้ำร่วมกัน เพื่อส่งต่อข้อมูลชนิดในสองทิศทาง
• วิธีนี้ช่วยละ annotation ของชนิดบางส่วนได้ และกฎการตรวจสอบของ lambda abstraction สามารถรับชนิดพารามิเตอร์จากชนิดฟังก์ชันที่คาดหวังได้ จึงละ annotation ของ binder ตัวแปรได้

[GN⁺]

ความคิดเห็นบน Hacker News

• Guy Steele เคยบรรยายเรื่องนี้มาก่อน เขายังตั้งชื่อที่ค้นหาได้ให้กับสัญกรณ์บางแบบด้วย เช่น ไดอะแกรมกฎอนุมานแบบสองมิติ
  เขาเรียกสิ่งนี้ว่า เมตาสัญกรณ์ของวิทยาการคอมพิวเตอร์ แต่โดยส่วนตัวแล้วดูเหมือนจะใกล้กับทฤษฎีภาษาโปรแกรมมากกว่า https://m.youtube.com/watch?v=dCuZkaaou0Q

  • ตามคำพูดของ Guy Steele น่าเสียดายจริง ๆ ที่ “ภาษาโปรแกรมที่ได้รับความนิยมที่สุดในวิทยาการคอมพิวเตอร์” ไม่มีทั้งคอมไพเลอร์ อินเทอร์พรีเตอร์ หรือสเปกที่สมบูรณ์ และมีแต่ตัวแปรย่อยเพิ่มขึ้นมาตลอดหลายสิบปี
    https://en.wikipedia.org/wiki/Guy_Steele Guy Steele
    https://www.codemesh.io/codemesh2017/guy-l-steele ทอล์ก "A Cobbler's Child" ที่ Code Mesh 2017
    https://www.youtube.com/watch?v=qNPlDnX6Mio "A Cobbler's Child" (วิดีโอบน youtube)
    https://www.youtube.com/watch?v=dCuZkaaou0Q "It's Time for a New Old Language" (วิดีโอบน youtube)
    https://news.ycombinator.com/item?id=15473199 การอภิปรายบน HN
    https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150... สไลด์
    แปลกที่คนซึ่งพยายามพูดถึงศิลปะเชิงช่างของมนุษย์ที่แม่นยำที่สุดให้แม่นยำที่สุด กลับใช้ สัญกรณ์ที่คลุมเครือและไม่สอดคล้องกัน
  • ตอนนั้นก็มีการพูดถึงแล้ว: It's Time for a New Old Language – Guy Steele [video] - https://news.ycombinator.com/item?id=15473199 - Oct 2017 (45 comments)
  • หาไฟล์สไลด์เป็น PDF ไม่เจอ เลยสงสัยว่าเคยมีอัปโหลดไว้ที่ไหนหรือเปล่า
  • การที่ Rich Hickey เป็นคนเกริ่นนำพอดีนี่ค่อนข้างทรงพลังทีเดียว

• สัญกรณ์นี้ย้อนกลับไปได้ถึง Frege ถ้าไม่รู้ว่าต้องค้นหาอะไร ก็หายาก แต่บทความนี้ดูเป็นสรุปที่ค่อนข้างดี: https://plato.stanford.edu/entries/frege-logic
  สัญลักษณ์ turnstile |- ถูกใช้มาก่อนแล้ว และเส้นแนวนอนที่ในชั้นเรียนเรียกว่า “Fregescher Schlussstrich” หรือเส้นขีดสรุปของ Frege เดิมทีน่าจะเป็นส่วนหนึ่งของ turnstile เอง ก่อนจะแยกออกมาเป็นองค์ประกอบต่างหากในสัญกรณ์สมัยใหม่

  • “Schlussstrich” น่าจะแปลได้ใกล้เคียงกว่าเป็น เส้นขีดนิรนัย หรือ เส้นขีดอนุมาน

• Types and Programming Languages ของ Benjamin C. Pierce เป็นตำราที่ดีที่ครอบคลุมเรื่องแบบนี้

  • น่าขันที่ TAPL เองกลับอธิบายความหมายพื้นฐานของไวยากรณ์ที่ตัวเองใช้อยู่ได้ค่อนข้างไม่ชัด คำตอบนี้ชัดกว่า TAPL หลายลำดับขั้น

• แม้จะเรียนเอกวิทยาการคอมพิวเตอร์ ผมก็ยังสับสนกับความแตกต่างของความหมายระหว่าง |– กับ |= และตัวแปรที่ใช้ว่าแต่ละตัวอยู่ใน ระดับเมตาไวยากรณ์ ไหน
  ที่ย้อนแย้งคือ เหตุผลหนึ่งเป็นเพราะสัญกรณ์เองไม่มีไทป์ที่ระบุชัดเจน

  • https://philosophy.stackexchange.com/questions/10785/semanti...

• สำหรับคนที่ลังเลว่าจะอ่านดีไหม: บทความนี้เป็นคำอธิบาย สัญกรณ์ระบบชนิดข้อมูล ที่พบในเปเปอร์วิทยาการคอมพิวเตอร์ และโดยพื้นฐานแล้วเป็นบทนำเรื่องสัญกรณ์ BNF สำหรับระบบชนิดข้อมูล กฎอนุมาน ฯลฯ
  ดูเหมือนเป็นสรุปที่ดี

  • พูดตรง ๆ คืออยากได้แค่ ชีตสรุป ที่บอกว่าสัญลักษณ์พวกนี้อ่านเป็นคำภาษาอังกฤษว่าอย่างไร
    ผมเข้าใจแนวคิดเชิงตรรกะของการนำไทป์ไปใช้ แต่ไม่ได้อ่านเปเปอร์วิทยาการคอมพิวเตอร์บ่อยนัก เลยยังจับคู่สัญลักษณ์กับความหมายในหัวได้ไม่ค่อยติด
  • การที่สิ่งเหล่านี้ถูกทำให้เป็นนามธรรมอย่างละเอียดตลอดหลายปี แสดงให้เห็นถึง ความเป็นวิทยาการคอมพิวเตอร์ จริง ๆ

• ในตัวอย่าง 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 หมายถึง “𝗍𝗋𝗎𝖾+2 มีไทป์เป็น 𝖨𝗇𝗍” แต่บอกว่าประหลาดยิ่งกว่าเดิมเพราะนิพจน์ 𝗍𝗋𝗎𝖾+2 เองก็ไม่สมเหตุสมผลและไม่มีไทป์
  แต่ใน Python นั้น True + 2 เป็นจำนวนเต็มจริง ๆ และค่าก็เป็น 3 ไม่ว่าจะควรเป็นแบบนั้นหรือไม่ แต่มันเป็นอย่างนั้นจริง ๆ

  • ถ้าคิดว่า True + 2 สมเหตุสมผล ก็แค่นิยาม กฎการตัดสิน ที่อนุญาตแบบนั้นเอง
    ตรรกะและทฤษฎีระบบชนิดข้อมูลไม่ได้สนใจในตัวเองว่าคุณใช้สัจพจน์และกฎอนุมานแบบไหน เพียงแต่ช่วยให้อนุมานกฎเหล่านั้นและปฏิสัมพันธ์ระหว่างกันได้ เช่น อาจกำหนด |- True : Bool, |- True : Int หรือถ้าต้องการอนุญาตเฉพาะในนิพจน์บางอย่าง ก็สร้างกฎให้ดึง |- True + x: Int ออกมาจาก |- x : Int ได้
  • นี่ไม่ได้ขึ้นกับแต่ละภาษาหรือ? เช่นใน C นั้น true ถูกแมปเป็น 1 ดังนั้น true+1=2
  • แม้ใน Python หรือ C True + 2 จะไม่เกิดข้อผิดพลาด แต่ก็ยังเป็นเรื่องโง่อยู่ดี เพราะทำให้ความหมายเชิงนัยของภาษายากต่อการอนุมาน เพียงเพื่อให้โปรแกรมเมอร์ได้ syntax sugar เล็กน้อย

• ดีเลย สงสัยมาหลายปีแล้ว แต่ไม่รู้ว่าจะตั้งคำค้นอย่างไรถ้าจะหาข้อมูลเพิ่ม

• บางครั้งก็รู้สึกไม่ชอบขึ้นมาเฉย ๆ เวลามีคนเอา ความรู้ลับ ที่อุตส่าห์เรียนมาอย่างยากลำบากมาแจกฟรี ;) ถ้าตอนผมเรียนมีบทความแบบนี้ก็คงดีมาก หวังว่าพอเข้าถึงได้ง่ายขึ้นแล้ว ภาษาแย่ ๆ จะลดลง

• ตอนอ่าน Ada Reference Manual ผมจำไวยากรณ์แบบนี้ได้ทันที แม้จะไม่รู้ชื่อ แต่พอเห็นกรณีใช้งานจริงก็รู้สึกน่าสนใจ และทั้งภาษาก็ถูกนิยามด้วยสัญกรณ์แบบนั้น
  ตัวอย่าง: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • http://www.ada-auth.org/standards/22rm/html/RM-1-1-4.html
    Ada Reference Manual ระบุสัญกรณ์ที่ตนใช้ไว้อย่างชัดเจน โดยใช้รูปแบบดัดแปลงของ Backus-Naur Form และในหัวข้อที่ลิงก์ไว้ก็อธิบายรูปแบบดัดแปลงเฉพาะนั้น

• ตรงนี้ดูเหมือนเป็นโอกาสดีที่จะเผยแพร่ “จุดยืนที่ผมจะยืนหยัดไปจนสุดทาง” ข้อหนึ่ง ใน รูปแบบ type annotation ที่ใช้โคลอน ช่องว่างสองข้างโคลอนควรเท่ากัน
  สำหรับผม มันเหมือนมีสัญลักษณ์สองแบบที่บังเอิญมีรูปร่างเหมือนกัน คือจุดสองจุด แบบหนึ่งคือ label colon ซึ่งเหมือนในภาษาอังกฤษ คือส่วนหน้าทำหน้าที่แนะนำส่วนหลัง หรือด้านซ้ายเป็นป้ายกำกับของด้านขวา เช่น การเริ่มบล็อกใน Python, คู่ key-value, คู่ชื่อ-ค่าใน struct ของ C หรือ Rust
  อีกแบบคือ type annotation ที่ยืมมาจากคณิตศาสตร์ มันเป็นความสัมพันธ์ทวิภาค และความสัมพันธ์ทวิภาคควรเว้นวรรคซ้ายขวาเท่ากัน เราไม่เขียน x= 1, x> y, x+ z ฉันใด ก็ไม่ควรเขียน x: X แต่ควรเขียน x : X ถึงจะเป็นธรรมชาติ
  พอเห็น a: b ผมจะอ่านเป็น label colon ทันที และถ้ามันเป็น type annotation ก็ต้องมีการแปลงทางความคิดเพิ่มขึ้นเล็กน้อยทุกครั้ง นี่เป็นเรื่องของไวยากรณ์ภาษาโปรแกรม และโดยส่วนตัวผมชอบ x : X มากกว่า X x มาก
  [1] “Evangelion” เป็นคำเท่ ๆ ที่มาจาก εὐαγγέλιον ซึ่งแปลว่าข่าวดี [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

  • อาจมีความเข้าใจผิดได้อยู่บ้าง แม้ในงานเขียนคณิตศาสตร์ก็มีสัญกรณ์อย่าง f: X->Y ที่เว้นวรรคด้านขวาของโคลอนมากกว่าอยู่จริง และในหนังสือ 3 เล่มที่ผมตรวจดู มี 1 เล่มที่ใช้แต่สัญกรณ์แบบนั้น
    อีกทั้งแบบนั้นก็ยังค่อนข้างใกล้กับการติดป้ายกำกับอยู่ดี คือเป็นการติดป้ายกำกับสาทิศสัณฐานชนิดหนึ่ง กรณีที่โคลอนถูกใช้ในคณิตศาสตร์ด้วยความหมายที่ต่างออกไปจริง ๆ คือเมื่อใช้เป็นตัวย่อของ such that เช่นในการนิยามเซตแบบ { x : x \in IN and x | 2} หรือใช้ร่วมกับตัวบ่งปริมาณ ซึ่งพบได้บ่อย
  • เป็นมุมมองที่น่าสนใจ เรื่องขั้นตอนทางความคิดที่เพิ่มขึ้นนั้นเหมือนกับสิ่งที่ผมรู้สึกตอนอ่านสัญกรณ์ X x ที่พบได้ทั่วไปเลย x: X สำหรับผมเป็นธรรมชาติกว่ามาก และยังรู้สึกใกล้เคียงกับวิธีใช้โคลอนในภาษาธรรมชาติด้วย
    คือมีประพจน์หนึ่ง แล้วสิ่งที่ตามหลังโคลอนมาอธิบายประพจน์นั้นให้ละเอียดขึ้น ซึ่งก็เข้ากับ type พอดี เพราะ type ก็เป็นข้อมูลเพิ่มเติมเกี่ยวกับสิ่งที่อยู่ทางซ้าย
  • ในทฤษฎีชนิดข้อมูล โดยทั่วไปถือว่าแนวปฏิบัติมาตรฐานคือเว้นวรรคสองข้างโคลอนเท่ากัน เช่น t[ช่องว่าง]:[ช่องว่าง]T
    ทฤษฎีชนิดข้อมูล โดยรวมมีด้านที่ยุ่งเหยิงและไม่ค่อยสอดคล้องกันอยู่ แต่เฉพาะกรณีนี้เป็นตัวอย่างที่หาได้ยากซึ่งทุกคนค่อนข้างสอดคล้องกัน ผมสงสัยว่าสมัยปริญญาตรีตัวเองเขียนอย่างไร เลยไปดู แล้วก็พบว่าผมเองก็เขียนแบบสมมาตรสวยงามไว้เหมือนกัน: https://dvt.name/logic/horse2.pdf
  • x: X สอดคล้องกับการใช้แบบ “มีคำอธิบายตามหลังโคลอน”
    กล่าวคือคล้ายกับ variable x: It’s an X.
  • age: int สามารถอ่านแปลงเป็นภาษาอังกฤษได้ง่าย ๆ ว่า “person’s age: an integer”
    ดังนั้นโคลอนจึงไม่เคยทำให้ผมรู้สึกขัดตามากนัก