ปริศนาการตรวจสอบชนิดแบบสองทิศทาง

• บั๊กในอิมพลีเมนเตชัน การตรวจสอบชนิดแบบสองทิศทาง ของ Grace เกิดจากการนำชนิดของสมาชิกตัวแรกในลิสต์ไปใช้เสมือนเป็นชนิดของสมาชิกทั้งหมด ทำให้ฟิลด์ port: 8080 ถูกตัดทิ้งและได้ผลการประเมินที่ผิด
• ตัวอย่างปัญหาคือโค้ดที่วนลูปผ่านลิสต์ { domain: "google.com" } และ { domain: "localhost", port: 8080 } แล้วใช้พอร์ตเริ่มต้น 443 โดยคาดว่าจะได้ [ "google.com:443", "localhost:8080" ] แต่กลับคืนค่า [ "google.com:443", "localhost:443" ]
• การอนุมานลิสต์แบบเดิมจะอนุมานจากสมาชิกตัวแรกเป็น List { domain: Text } แล้วตรวจสมาชิกที่เหลือให้ตรงกับชนิดนั้น และในกระบวนการ elaboration ฟิลด์ port ที่ไม่มีอยู่ในชนิดแม่ก็ถูกลบออก
• อิมพลีเมนเตชันที่แก้ไขแล้วจะอนุมานชนิดของสมาชิกทุกตัวก่อน จากนั้นคำนวณ ชนิดแม่ที่เฉพาะเจาะจงที่สุด แล้วตรวจสมาชิกแต่ละตัวใหม่ให้ตรงกับชนิดนั้น พร้อมเติมค่า Optional ที่ขาดด้วย null หรือ some
• หลังแก้ไข ลิสต์เดิมจะถูกอนุมานเป็น List { domain: Text, port: Optional Natural } โดย port ของเรคอร์ดแรกเป็น null และ port: 8080 ของเรคอร์ดที่สองถูกเก็บไว้เป็น some 8080 จึงได้ผลลัพธ์ตามที่คาด

---

บั๊กการอนุมานชนิดลิสต์ของ Grace

• Grace ใช้ระบบ การตรวจสอบชนิดแบบสองทิศทาง ที่อิงจาก Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism และเมื่อมีการสะสมวิธีแก้ข้อจำกัดของแนวทางนี้ไว้ในอิมพลีเมนเตชัน ก็กลายเป็นบั๊กประหลาด
• โปรแกรมที่มีปัญหาคือรูปแบบ list comprehension ที่วนผ่านลิสต์ authorities แล้ว bind ค่า domain และ port ของแต่ละเรคอร์ด โดยใช้ 443 เป็นค่าเริ่มต้นเมื่อไม่มี port

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• ผลลัพธ์ที่คาดไว้คือ [ "google.com:443", "localhost:8080" ] แต่เวอร์ชันที่มีบั๊กกลับคืนค่า [ "google.com:443", "localhost:443" ] โดยเมินฟิลด์ port: 8080 ของเรคอร์ดที่สองไปทั้งหมด
• ปัญหาไม่ได้เกิดจาก evaluator แต่เกิดใน ตัวตรวจสอบชนิด และได้รับผลร่วมกันจากการอนุมานชนิดลิสต์กับกระบวนการ elaboration ระหว่างการตรวจชนิด

การตรวจสอบชนิดแบบสองทิศทางและข้อจำกัดของวิธีอนุมานลิสต์แบบเดิม

• ชนิดที่ Grace คาดหวังสำหรับลิสต์ authorities คือดังนี้

List { domain: Text, port: Optional Natural }

• ชนิดนี้หมายความว่าแต่ละเรคอร์ดต้องมีฟิลด์บังคับ domain: Text และอาจมีหรือไม่มีฟิลด์ port: Optional Natural ก็ได้
• แต่อิมพลีเมนเตชันเดิมกลับอนุมานชนิดที่แคบกว่านี้

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• โดยพื้นฐานแล้ว การตรวจสอบชนิดแบบสองทิศทาง แบ่งเป็นสองงาน
  • อนุมานชนิดของ expression
  • ตรวจว่า expression ตรงกับชนิดที่คาดหวังหรือไม่
• เพียงสองงานนี้ยังไม่พอที่จะรวมชนิดของสมาชิกหลายตัวในลิสต์ให้ได้ชนิดแม่ของสมาชิกทั้งลิสต์อย่างง่ายดาย
• อิมพลีเมนเตชันเดิมของ Grace อนุมานชนิดลิสต์ด้วยวิธีนี้
  • อนุมานชนิดของสมาชิกตัวแรกในลิสต์
  • ตรวจสมาชิกที่เหลือทั้งหมดว่าเข้ากับชนิดที่อนุมานจากสมาชิกตัวแรกหรือไม่
• เพราะสมาชิกตัวแรก { domain: "google.com" } มีชนิด { domain: Text } ชนิดของสมาชิกทั้งลิสต์จึงกลายเป็น { domain: Text }
• หากต้องการชนิดอื่น เดิมทีต้องใส่ type annotation อย่างชัดเจน แต่ JSON จริงที่ Grace ต้องรองรับอาจมี schema ใหญ่และซับซ้อน จึงไม่ต้องการบังคับให้เขียน schema ทั้งหมดเป็น type annotation ขนาดใหญ่

ทำไม elaboration ถึงเปลี่ยนผลการประเมินได้ด้วย

• ตัวตรวจสอบชนิดของ Grace ไม่ได้มีหน้าที่แค่จับ type error แต่ยังทำ elaboration ซึ่งเป็นการปรับ expression ระหว่างกระบวนการตรวจชนิดด้วย
• เมื่อตรวจชนิดย่อยให้ตรงกับชนิดแม่แล้วสองชนิดไม่ตรงกัน ตัวตรวจสอบชนิดจะใส่ explicit coercion เข้าไป
• ภายใน evaluator ของ Grace ค่าทุกตัวที่เป็น Optional จะถูกแทนเป็นค่าที่ติดแท็ก null หรือ some x
• หากนำค่าที่ไม่มีแท็กไปใส่ในตำแหน่งที่คาดหวัง Optional Grace จะใส่แท็ก some ให้อัตโนมัติ

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• หากสมาชิกตัวแรกถูกอนุมานเป็น Optional Natural และสมาชิกตัวที่สองเป็น Natural ที่ไม่มีแท็ก ตัวตรวจสอบชนิดจะไม่รายงาน type mismatch แต่จะใส่แท็ก some ให้แทน
• สิ่งเดียวกันนี้เกิดขึ้นกับเรคอร์ดด้วย โดย Grace รองรับ record subtyping และสามารถ coercion เรคอร์ดให้ตรงกับชนิดแม่ได้

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• หากใส่ annotation ให้เรคอร์ดเป็นชนิดเรคอร์ดที่เล็กกว่า ตัวตรวจสอบชนิดจะยอมรับและตัดฟิลด์ที่ไม่มีในชนิดแม่ออก
• แม้ประเมินเพียงลิสต์ authorities อย่างเดียว ในอิมพลีเมนเตชันเดิมฟิลด์ port ก็จะถูกลบออกดังนี้

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• ผลลัพธ์นี้เกิดจากลำดับดังนี้
  • อนุมานชนิดของสมาชิกตัวแรกเป็น { domain: Text }
  • ตรวจสมาชิกตัวที่สองโดยใช้ชนิดที่คาดหวังนั้น
  • สมาชิกตัวที่สองเข้ากับชนิดดังกล่าว แต่มีฟิลด์เพิ่มเติมคือ port
  • ตัวตรวจสอบชนิดจึงลบฟิลด์ port เพื่อให้ตรงกับชนิดที่คาดหวัง
• การ coercion เรคอร์ดเองไม่ใช่ต้นตอหลัก ปัญหาจริงคือวิธีอนุมานชนิดลิสต์ที่นำชนิดของสมาชิกตัวแรกมาใช้เหมือนเป็นชนิดของทั้งลิสต์

วิธีแก้: คำนวณชนิดแม่ที่เฉพาะเจาะจงที่สุด

• Grace เพิ่ม โอเปอเรชันใหม่สำหรับอนุมานชนิดของทั้งลิสต์ให้ถูกต้อง
• โอเปอเรชันใหม่นี้ใช้คำนวณ ชนิดแม่ที่เฉพาะเจาะจงที่สุด (most-specific supertype) หรือ least upper bound ของชนิดสองชนิด
• การที่ C เป็นชนิดแม่ของ A และ B หมายถึง C เป็นชนิดแม่ของทั้ง A และ B
• การที่ C เป็นชนิดแม่ที่เฉพาะเจาะจงที่สุดของ A และ B หมายถึง C เป็นชนิดย่อยของชนิดแม่อื่นทุกชนิดของ A และ B
• การอนุมานชนิดลิสต์แบบใหม่จึงเปลี่ยนเป็นลำดับดังนี้
  • อนุมานชนิดของสมาชิกแต่ละตัวในลิสต์
  • คำนวณชนิดแม่ที่เฉพาะเจาะจงที่สุดของชนิดสมาชิกทั้งหมด
  • ตรวจสมาชิกแต่ละตัวว่าเข้ากับชนิดแม่ที่เฉพาะเจาะจงที่สุดนั้นหรือไม่
  • คืนค่าชนิดแม่ที่เฉพาะเจาะจงที่สุดนั้นเป็นชนิดสมาชิกของทั้งลิสต์
• ด้วยวิธีนี้ ลิสต์ต่อไปนี้จะถูกอนุมานชนิดได้อย่างถูกต้อง

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• การทำงานภายในมีดังนี้
  • { x: 1 } ถูกอนุมานเป็นชนิด { x: Natural }
  • { y: true } ถูกอนุมานเป็นชนิด { y: Bool }
  • ชนิดแม่ที่เฉพาะเจาะจงที่สุดของทั้งสองชนิดคือ { x: Optional Natural, y: Optional Bool }
  • จากนั้นตรวจสมาชิกแต่ละตัวอีกครั้งให้ตรงกับชนิดแม่ดังกล่าว
• เหตุผลที่ต้องตรวจสมาชิกแต่ละตัวใหม่กับชนิดแม่ก็เพื่อให้เกิด elaboration ที่ถูกต้อง เช่น เติม some และ null ที่หายไป

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

ชนิดและผลการประเมินของ authorities หลังแก้ไข

• หลังแก้ตัวตรวจสอบชนิด ลิสต์ authorities เดิมจะถูกอนุมานเป็นชนิดที่คาดหวัง

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• ผลการประเมินหลัง elaboration ก็ยังคงเก็บ port ไว้ในฐานะฟิลด์ทางเลือก

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• port ที่หายไปในเรคอร์ดแรกจะถูกเติมเป็น null ส่วน port: 8080 ในเรคอร์ดที่สองจะถูกเก็บไว้เป็น some 8080
• ตัวอย่าง list comprehension เดิมจึงคืนค่าตามที่คาดไว้

[ "google.com:443", "localhost:8080" ]

การรองรับ JSON กับการเลือกความซับซ้อนของอิมพลีเมนเตชัน

• เหตุผลที่ Grace ผลักดันการตรวจสอบชนิดแบบสองทิศทางอย่างจริงจังคือ มองว่านี่เป็นเฟรมเวิร์กการตรวจชนิดที่แม้ซับซ้อน แต่ทรงพลังพอสำหรับอนุมานชนิดของ JSON ที่พบในโลกจริง
• การอนุมานแบบ Hindley-Milner หรือเฟรมเวิร์กตรวจชนิดที่ง่ายกว่านั้นมีข้อจำกัดในการจัดการรูปแบบข้อมูลที่พบได้ใน JSON จริง
• Grace ไม่ได้ถูกสร้างมาเพื่อเป็นภาษาที่ ergonomic สำหรับงาน JSON เพียงอย่างเดียว แต่ก็ไม่ได้ละเลยการรองรับ JSON
• จากประสบการณ์กับ Dhall ผู้พัฒนาพบว่าผู้ใช้ให้ความสำคัญกับ JSON interoperability ที่ใช้งานสะดวกมาก ดังนั้นไวยากรณ์และระบบชนิดของ Grace จึงถูกออกแบบโดยคำนึงถึงความเข้ากันได้กับ JSON แม้จะเพิ่มความซับซ้อนของอิมพลีเมนเตชันก็ตาม

แหล่งข้อมูลที่เกี่ยวข้องน่าสนใจ

• Datatype unification using Monoids: ว่าด้วยอัลกอริทึมอนุมานชนิดสำหรับข้อมูลธรรมดา ซึ่งโดยแก่นแล้วเป็นอัลกอริทึมเดียวกับที่ Grace ใช้คำนวณชนิดแม่ที่เฉพาะเจาะจงที่สุด
• The appeal of bidirectional typechecking: อธิบายว่าทำไมจึงควรเรียนรู้การตรวจสอบชนิดแบบสองทิศทาง หากต้องการอิมพลีเมนต์ภาษาที่ใช้ subtyping ไม่ว่ารูปแบบใดก็ตาม
• Local Type Inference: หนึ่งในงานวิจัยบุกเบิกด้านการตรวจสอบชนิดแบบสองทิศทาง และเป็นแหล่งที่มาของเทคนิคอย่าง least upper bound กับการทำ elaboration ของ expression ไปเป็นภาษาแกนภายใน

ภาคผนวก: ทำไมจึงต้องมีการ coercion เรคอร์ด

• expression ต่อไปนี้ใน Grace เป็นตัวอย่างที่แสดงว่าทำไมจึงจำเป็นต้องมีการ coercion เรคอร์ด

let f (input: { }) = input.x

in  f { x: 1 }

• หาก expression นี้ผ่านการตรวจชนิดได้ คำถามคือชนิดคืนค่าของ f ควรเป็นอะไร
• ชนิดคืนค่าไม่ควรเป็น Natural

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• เพราะ f รับ input ที่มีชนิดเป็นเรคอร์ดว่าง { } จึงไม่อาจดึงค่า Natural ออกจากเรคอร์ดนั้นได้
• ต่อให้ตอนเรียกใช้งานบังเอิญส่งเรคอร์ดที่มีฟิลด์ x เข้ามา ฟังก์ชัน f ก็ยังต้องทำงานได้กับอินพุตทุกตัวที่มีชนิด { }
• การให้ตัวตรวจสอบชนิดปฏิเสธการเข้าถึงฟิลด์ที่ไม่มีในชนิดอินพุตที่ประกาศไว้ก็เป็นทางเลือกที่ sound แต่จะสูญเสียความสามารถที่จำเป็นต่อการจัดการข้อมูล JSON จริง
• ตัวอย่าง authorities เดิมโดยเนื้อแท้แล้วเทียบได้กับ syntactic sugar ของ expression ต่อไปนี้

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• หากปฏิเสธการเข้าถึงฟิลด์ที่อาจไม่มีอยู่ ก็จะไม่สามารถ bind ฟิลด์ที่อาจหายไปหรือกำหนดค่าเริ่มต้นให้มันได้
• สำหรับการออกแบบเพื่อรองรับข้อมูล JSON จริง ทางเลือกที่ใช้คือ
  • หากไม่มีฟิลด์ ให้คืนค่า null
  • กำหนดชนิดของการเข้าถึงเป็น forall (a: Type) . Optional a
• ชนิดนี้เป็นชนิดที่มีได้เพียง null เท่านั้น
• เมื่อเลือกแนวทางนี้ ก็จำเป็นต้องตัดฟิลด์ที่ไม่มีในชนิดแม่ออกจากเรคอร์ดเสมอ
• หากไม่ลบฟิลด์ส่วนเกิน ตัวอย่างต่อไปนี้จะคืนค่า 1 : forall (a: Type) . Optional a

let f (input: { }) = input.x

in  f { x: 1 }

• ซึ่งจะกลายเป็น expression ที่มีชนิดผิด เพราะชนิดที่ควรมีได้แค่ null กลับมีค่า 1 อยู่ข้างใน
• expression ที่มีชนิดผิดเช่นนี้อาจทำให้ evaluator พังได้

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• ใน Grace ที่ใช้กับข้อมูล JSON จริง การ coercion เรคอร์ดอย่างชัดเจนให้ตรงกับชนิดแม่จึงเป็นพฤติกรรมที่สมเหตุสมผล และบั๊กจริงก็ไม่ได้อยู่ที่ coercion แต่อยู่ที่วิธีแก้ชั่วคราวเดิมสำหรับการอนุมานชนิด List

[GN⁺]

ความคิดเห็นจาก Lobste.rs

• น่ายินดีที่ทำให้บทความ Complete And Easy ออกมาอยู่ในรูปแบบที่ใช้งานได้จริง นี่ก็เป็นตัวอย่างที่ดีด้วยว่า ธรรมชาติแบบละโมบของ การตรวจสอบชนิดแบบสองทิศทาง สามารถก่อปัญหาที่ละเอียดอ่อนได้
  ไม่ได้จะตำหนินะ เพราะการอนุมานย่อมมีปัญหาอยู่เสมอ และสุดท้ายก็ใกล้เคียงกับการเลือกว่าจะยอมรับปัญหาแบบไหน ดังนั้นโดยส่วนตัวแล้วผมมองว่า subtyping และการบังคับแปลงชนิดมักจะค่อนข้างเป็น anti-pattern
  ถ้าใช้ข้อมูลเป็นแหล่งความจริงของชนิด ก็จะตรวจสอบได้ยากว่าข้อมูลนั้นผิดหรือไม่ และแทนที่จะได้ข้อผิดพลาดที่มีประโยชน์แบบในตัวอย่าง ก็กลับได้ชนิดที่ผิดแทน แต่คนทำ Dhall ก็น่าจะรู้เรื่องฝั่งนี้ดีกว่าผมมากอยู่แล้ว แนวคิดในการรับข้อมูลหลายชุดแล้วสร้างสคีมาขึ้นมาเองก็น่าสนใจพอจะวิจัยต่อได้ เพียงแต่เมื่อชนิดมักถูกมองว่าเป็นข้อกำหนดมากกว่าคำบรรยาย ผมก็ไม่แน่ใจนักว่าควรเรียกสิ่งนี้ว่า “การตรวจสอบชนิด” หรือเปล่า

• ผมไม่ค่อยเข้าใจว่าทำไมถึงไม่ปฏิเสธ f ไปเลย กำลังเข้าถึงฟิลด์จากเรคคอร์ดที่มีชนิดซึ่งไม่มีทางมีฟิลด์นั้นได้ แบบนี้แทบจะแน่นอนว่าเป็นบั๊กของโปรแกรม และดูเป็นกรณีที่ ตัวตรวจสอบชนิด ควรบอกให้รู้
  จุดที่ต่างจากตัวอย่าง authority คือไม่ใช่ว่าชนิดของ port หายไป แต่เป็นว่า port เป็น Optional การปฏิเสธฟิลด์ที่ไม่มีอยู่ไม่ได้แปลว่าต้องปฏิเสธฟิลด์แบบเลือกได้ไปด้วย ถ้าคุณบังคับแปลงค่าโดยอิงจากชนิดอยู่แล้ว ก็สามารถบังคับแปลง { domain: "google.com" } ให้เป็นค่า { domain: "google.com", port: null } ได้เช่นกัน

  • พูดสั้น ๆ คือไม่จำเป็นต้องปฏิเสธ f เลย และนั่นเป็น ข้อจำกัดที่ไม่จำเป็น ผมคิดว่าการให้การเข้าถึงฟิลด์ที่ผิดคืนค่า null : forall (a : Type) . Optional a ดีกว่าการปฏิเสธการเข้าถึงฟิลด์ที่ผิดอย่างเคร่งครัด
    มันยอมรับโปรแกรมที่ใช้ได้มากกว่า และโปรแกรมที่กำหนดชนิดผิดก็ยังคงล้มเหลวอยู่ดี ตัวอย่างเช่น โปรแกรมที่พยายามใช้ค่าที่เข้าถึงมาโดยไม่จัดการ null ก็ยังคงได้ type error เหมือนเดิม

• ความคิดแรกที่นึกออกคือ row types น่าจะแก้ปัญหานี้ได้ คิดว่าน่าจะเคยพิจารณาไปแล้ว หรือว่าในที่นี้ row types พังลงเพราะปฏิสัมพันธ์กับ subtyping?

  • Grace มีทั้ง row types และ row polymorphism ใน Grace จะเรียก row ว่า “fields” แต่ที่เหลือก็เหมือนกันทุกอย่าง
    จริง ๆ แล้วอัลกอริทึม least upper bound ที่เจาะจงที่สุดก็พิจารณา row types ด้วย
    ตัวอย่างเช่น ถ้าเขียนแบบนี้:

    \record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    Grace จะอนุมานชนิดต่อไปนี้ให้กับนิพจน์นี้:

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• นี่ไม่ใช่ตัวอย่างของปัญหา greedy instantiation ที่พูดถึงในหัวข้อ 5.1.1 ของบทความ Bidirectional Typing หรอกหรือ?
  “ในสถานการณ์เดิม วิธีแบบละโมบนี้นับว่าโชคร้ายพอสมควรที่ไวต่อการเรียงลำดับอาร์กิวเมนต์ อย่างไรก็ตาม มันอาจใช้งานได้ในบริบทของพหุสัณฐานระดับสูงแบบ predicative ที่ไม่มี subtyping รูปแบบอื่น ‘ปัญหา tabby-first’ จะเกิดขึ้นไม่ได้ เพราะวิธีเดียวที่ทำให้ชนิดเล็กลงอย่างเคร่งครัดได้ คือทำให้มันเป็นพหุสัณฐานมากขึ้นอย่างเคร่งครัด และถ้าอาร์กิวเมนต์ตัวแรกเป็นพหุสัณฐาน เราก็ต้อง instantiate 𝛼 ด้วยชนิดพหุสัณฐาน ซึ่งจะละเมิดความเป็น predicative”