Câu đố về kiểm tra kiểu hai chiều

• Trong quá trình triển khai kiểm tra kiểu hai chiều của Grace, do cách dùng kiểu của phần tử đầu tiên trong danh sách như thể đó là kiểu của toàn bộ phần tử, trường port: 8080 đã bị loại bỏ, dẫn đến kết quả đánh giá sai
• Ví dụ gây lỗi là đoạn mã duyệt qua danh sách gồm { domain: "google.com" } và { domain: "localhost", port: 8080 }, rồi dùng cổng mặc định 443; thay vì giá trị mong đợi [ "google.com:443", "localhost:8080" ] thì lại trả về [ "google.com:443", "localhost:443" ]
• Cơ chế suy luận danh sách cũ suy ra List { domain: Text } từ phần tử đầu tiên, rồi kiểm tra các phần tử còn lại theo kiểu đó; trong quá trình tinh chỉnh (elaboration), trường port không có trong kiểu cha đã bị loại bỏ
• Cách triển khai đã sửa sẽ suy luận kiểu của từng phần tử trước, sau đó tính kiểu cha cụ thể nhất rồi kiểm tra lại từng phần tử theo kiểu đó để điền các giá trị Optional còn thiếu bằng null hoặc some
• Sau khi sửa, danh sách ban đầu được suy luận thành List { domain: Text, port: Optional Natural }; port của bản ghi đầu tiên là null, còn port: 8080 của bản ghi thứ hai được giữ lại thành some 8080, nên trả về đúng kết quả kỳ vọng

---

Lỗi suy luận kiểu danh sách trong Grace

• Grace dùng hệ thống kiểm tra kiểu hai chiều dựa trên Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism; trong quá trình chồng thêm các cách triển khai để lách giới hạn của hướng tiếp cận này, một lỗi kỳ quặc đã xuất hiện
• Chương trình gây lỗi có dạng list comprehension, duyệt qua danh sách authorities, ràng buộc domain và port của mỗi bản ghi, rồi dùng 443 làm giá trị mặc định nếu không có port

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

for { domain, port = 443 } of authorities

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

• Kết quả mong đợi là [ "google.com:443", "localhost:8080" ], nhưng phiên bản có lỗi lại trả về [ "google.com:443", "localhost:443" ], tức là hoàn toàn bỏ qua trường port: 8080 của bản ghi thứ hai
• Vấn đề không nằm ở bộ đánh giá mà ở trình kiểm tra kiểu; cả suy luận kiểu danh sách lẫn quá trình tinh chỉnh (elaboration) khi kiểm tra kiểu đều cùng tác động

Kiểm tra kiểu hai chiều và giới hạn của cách suy luận danh sách cũ

• Kiểu mà Grace kỳ vọng cho danh sách authorities là như sau

List { domain: Text, port: Optional Natural }

• Kiểu này có nghĩa là mỗi bản ghi có trường bắt buộc domain: Text, còn trường port: Optional Natural có thể có hoặc không
• Nhưng cách triển khai cũ thực tế lại suy luận ra một kiểu hẹp hơn như sau

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

• Kiểm tra kiểu hai chiều về cơ bản chia làm hai công việc
  • suy luận kiểu của biểu thức
  • kiểm tra xem biểu thức có khớp với kiểu mong đợi hay không
• Chỉ với hai thao tác này thì không dễ kết hợp kiểu của nhiều phần tử trong danh sách để tạo ra kiểu cha của toàn bộ phần tử
• Cách triển khai cũ của Grace suy luận kiểu danh sách theo quy trình sau
  • suy luận kiểu của phần tử đầu tiên trong danh sách
  • kiểm tra toàn bộ phần tử còn lại xem có khớp với kiểu suy ra từ phần tử đầu tiên hay không
• Vì kiểu của phần tử đầu tiên { domain: "google.com" } là { domain: Text }, nên kiểu phần tử của cả danh sách cũng trở thành { domain: Text }
• Nếu muốn kiểu khác thì phải thêm chú thích kiểu tường minh, nhưng JSON thực tế mà Grace hướng tới có thể có lược đồ lớn và phức tạp, nên không muốn buộc người dùng phải viết toàn bộ lược đồ thành một chú thích kiểu khổng lồ

Vì sao tinh chỉnh lại làm thay đổi cả kết quả đánh giá

• Trình kiểm tra kiểu của Grace không chỉ bắt lỗi kiểu mà còn thực hiện tinh chỉnh (elaboration) để điều chỉnh biểu thức ngay trong lúc kiểm tra kiểu
• Khi kiểm tra một kiểu con theo một kiểu cha mà hai kiểu không hoàn toàn giống nhau, trình kiểm tra kiểu sẽ chèn ép kiểu tường minh (coercion)
• Bộ đánh giá của Grace biểu diễn mọi giá trị Optional nội bộ dưới dạng có gắn nhãn null hoặc some x
• Nếu đặt một giá trị không có nhãn vào vị trí đang mong đợi Optional, Grace sẽ tự động chèn nhãn some

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

• Nếu phần tử đầu tiên được suy luận là Optional Natural còn phần tử thứ hai là Natural không có nhãn, trình kiểm tra kiểu sẽ chèn nhãn some thay vì báo lỗi không khớp kiểu
• Điều tương tự cũng xảy ra với bản ghi; Grace hỗ trợ kiểu con cho bản ghi và ép kiểu bản ghi để khớp với kiểu cha

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

• Khi chú thích một bản ghi bằng một kiểu bản ghi nhỏ hơn, trình kiểm tra kiểu vẫn chấp nhận nhưng sẽ loại bỏ các trường không có trong kiểu cha
• Chỉ cần đánh giá riêng danh sách authorities, ở cách triển khai cũ ta cũng đã thấy trường port bị xóa như sau

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

• Kết quả này xảy ra theo luồng sau
  • kiểu của phần tử đầu tiên được suy luận là { domain: Text }
  • phần tử thứ hai được kiểm tra theo kiểu kỳ vọng đó
  • phần tử thứ hai phù hợp với kiểu này nhưng có thêm trường port
  • trình kiểm tra kiểu loại bỏ trường port để khớp với kiểu kỳ vọng
• Bản thân việc ép kiểu bản ghi không phải nguyên nhân gốc rễ; nguyên nhân thật sự là cách suy luận kiểu danh sách đã coi kiểu của phần tử đầu tiên như kiểu của cả danh sách

Giải pháp: tính kiểu cha cụ thể nhất

• Grace đã bổ sung một phép toán mới để suy luận đúng kiểu của toàn bộ danh sách
• Phép toán mới này tính kiểu cha cụ thể nhất (most-specific supertype), tức cận trên nhỏ nhất (least upper bound), của hai kiểu
• Nói C là kiểu cha của A và B nghĩa là C là kiểu cha của cả A lẫn B
• Nói C là kiểu cha cụ thể nhất của A và B nghĩa là C là kiểu con của mọi kiểu cha khác của A và B
• Với phép toán mới, quy trình suy luận kiểu danh sách được đổi thành
  • suy luận kiểu của từng phần tử trong danh sách
  • tính kiểu cha cụ thể nhất của toàn bộ các kiểu phần tử
  • kiểm tra từng phần tử xem có khớp với kiểu cha cụ thể nhất đó hay không
  • trả về kiểu cha cụ thể nhất đó làm kiểu phần tử của cả danh sách
• Theo cách này, danh sách sau được suy luận đúng kiểu

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

• Luồng xử lý nội bộ như sau
  • { x: 1 } được suy luận là kiểu { x: Natural }
  • { y: true } được suy luận là kiểu { y: Bool }
  • kiểu cha cụ thể nhất của hai kiểu này là { x: Optional Natural, y: Optional Bool }
  • từng phần tử sau đó được kiểm tra lại theo kiểu cha này
• Lý do phải kiểm tra lại từng phần tử theo kiểu cha là để áp dụng đúng quá trình tinh chỉnh, chẳng hạn bổ sung some và null còn thiếu

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

Kiểu và kết quả đánh giá của authorities sau khi sửa

• Sau khi sửa trình kiểm tra kiểu, danh sách authorities ban đầu được suy luận đúng như kỳ vọng

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

• Kết quả đánh giá sau tinh chỉnh cũng giữ lại port như một trường tùy chọn

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

• Trường port bị thiếu ở bản ghi đầu tiên được điền bằng null, còn port: 8080 của bản ghi thứ hai được giữ nguyên thành some 8080
• Ví dụ list comprehension ban đầu cũng trả về kết quả đúng như mong đợi

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

Lựa chọn giữa hỗ trợ JSON và độ phức tạp triển khai

• Lý do Grace vẫn đẩy mạnh kiểm tra kiểu hai chiều là vì cách này, dù phức tạp, vẫn được xem là một khung kiểm tra kiểu đủ mạnh để suy luận các kiểu JSON trong thực tế
• Suy luận Hindley-Milner hoặc các khung kiểm tra kiểu đơn giản tương tự khó xử lý được các hình dạng dữ liệu thường thấy trong JSON thật
• Grace không được tạo ra chỉ để làm một ngôn ngữ tiện dụng cho thao tác JSON, nhưng cũng không phớt lờ hỗ trợ JSON
• Từ kinh nghiệm với Dhall, tác giả nhận thấy người dùng rất nhạy cảm với tính tiện dụng khi tương tác với JSON, nên cú pháp và hệ kiểu của Grace được thiết kế để cân nhắc tính tương thích với JSON dù điều đó làm tăng độ phức tạp triển khai

Tài liệu liên quan đáng tham khảo

• Datatype unification using Monoids: trình bày một thuật toán suy luận kiểu cho dữ liệu đơn giản, về bản chất giống với thuật toán Grace dùng để tính kiểu cha cụ thể nhất
• The appeal of bidirectional typechecking: giải thích vì sao nên học kiểm tra kiểu hai chiều nếu bạn muốn triển khai một ngôn ngữ có dùng kiểu con dưới bất kỳ hình thức nào
• Local Type Inference: một trong những bài báo tiên phong về kiểm tra kiểu hai chiều, được nêu là nguồn gốc của các kỹ thuật như cận trên nhỏ nhất và tinh chỉnh biểu thức sang ngôn ngữ nội bộ

Phụ lục: Vì sao cần ép kiểu bản ghi

• Biểu thức Grace sau đây cho thấy vì sao cần đến ép kiểu bản ghi

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

in  f { x: 1 }

• Nếu biểu thức này được kiểm tra kiểu, câu hỏi đặt ra là kiểu trả về của f phải là gì
• Kiểu trả về không thể là Natural

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

in  f { x: 1 }

• f nhận input có kiểu bản ghi rỗng { }, nên không thể lấy ra một giá trị Natural từ bản ghi đó
• Dù lúc gọi có vô tình truyền vào một bản ghi có trường x, hàm f vẫn phải hoạt động với mọi đầu vào thuộc kiểu { }
• Việc để trình kiểm tra kiểu từ chối truy cập các trường không có trong kiểu đầu vào đã khai báo cũng là một lựa chọn hợp lý, nhưng như vậy sẽ mất đi khả năng cần thiết để xử lý dữ liệu JSON thật
• Ví dụ authorities ban đầu về bản chất tương đương với đoạn biểu thức đã được viết tường minh hơn sau đây

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)}"

• Nếu từ chối truy cập trường bị thiếu, bạn sẽ không thể ràng buộc các trường có thể vắng mặt hoặc xử lý chúng bằng giá trị mặc định
• Lựa chọn thiết kế để xử lý tốt JSON thực tế là như sau
  • nếu thiếu trường thì trả về null
  • gán kiểu truy cập là forall (a: Type) . Optional a
• Đây là một kiểu chỉ có thể chứa null
• Nếu đi theo hướng này thì bắt buộc phải loại bỏ các trường không có trong kiểu cha khỏi bản ghi
• Nếu không loại bỏ các trường thừa, ví dụ sau sẽ trả về 1 : forall (a: Type) . Optional a

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

in  f { x: 1 }

• Đây sẽ là một biểu thức có kiểu sai: 1 lại nằm trong một kiểu vốn chỉ nên có null
• Một biểu thức sai kiểu như vậy thậm chí có thể làm hỏng bộ đánh giá

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`

• Trong Grace, vốn được thiết kế để làm việc với dữ liệu JSON thật, việc ép kiểu bản ghi tường minh theo kiểu cha là hành vi hợp lý; lỗi thực sự không nằm ở ép kiểu mà ở giải pháp tạm thời trước đây cho suy luận kiểu List

[GN⁺]

Ý kiến trên Lobste.rs

• Việc biến bài báo Complete And Easy thành một thứ thực sự chạy được là rất đáng chúc mừng. Đây cũng là một ví dụ hay cho thấy bản chất tham lam của kiểm tra kiểu hai chiều có thể tạo ra những vấn đề tinh vi
  Đây không phải là lời chỉ trích; suy luận lúc nào cũng có vấn đề, và rốt cuộc gần như là chuyện chọn xem mình chấp nhận loại vấn đề nào. Vì vậy cá nhân tôi thường xem subtyping và ép kiểu là những anti-pattern
  Khi lấy dữ liệu làm nguồn chân lý cho kiểu, sẽ khó kiểm tra liệu dữ liệu có sai hay không, và như ví dụ cho thấy, ta nhận được kiểu sai thay vì lỗi hữu ích. Tuy vậy, vì người làm ra Dhall nói điều này nên có lẽ họ hiểu mảng này hơn tôi rất nhiều. Bản thân ý tưởng nhận nhiều dữ liệu rồi sinh ra schema là đáng để nghiên cứu, nhưng vì kiểu thường được xem là có tính quy định hơn là mô tả, tôi không chắc có nên gọi đây là “kiểm tra kiểu” hay không

• Tôi không thực sự hiểu vì sao lại không просто từ chối f. Bạn đang truy cập một trường từ một record có kiểu chắc chắn không thể nào có trường đó, nên gần như chắc chắn đây là bug của chương trình và có vẻ là lúc trình kiểm tra kiểu nên báo cho bạn biết
  Điểm khác với ví dụ authority là kiểu của port không phải là bị thiếu mà là Optional. Việc từ chối trường bị thiếu không có nghĩa là phải từ chối cả trường tùy chọn. Nếu đã đang ép giá trị dựa trên kiểu thì { domain: "google.com" } cũng có thể được ép thành giá trị { domain: "google.com", port: null }

  • Nói ngắn gọn thì không nhất thiết phải từ chối f, và đó là một hạn chế không cần thiết. Tôi cho rằng để truy cập trường sai trả về null : forall (a : Type) . Optional a tốt hơn hẳn so với việc từ chối truy cập trường sai
    Nó cho phép nhiều chương trình hợp lệ hơn, còn các chương trình được gán kiểu sai thì vẫn thất bại. Ví dụ, chương trình cố dùng giá trị đã truy cập mà không xử lý null vẫn sẽ giữ nguyên lỗi kiểu

• Ý nghĩ xuất hiện ngay là row types giải quyết được chuyện này. Có lẽ điều đó đã được xem xét rồi. Ở đây có phải row types bị phá vỡ khi tương tác với subtyping không?

  • Grace có row types và row polymorphism. Trong Grace, row được gọi là “fields”, nhưng ngoài chuyện đó ra thì hoàn toàn giống nhau
    Thực tế, thuật toán kiểu siêu cấp cụ thể nhất cũng xét đến row types
    Ví dụ, nếu viết như sau:

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

    Grace sẽ suy ra cho biểu thức này kiểu sau:

    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 }  
    

• Đây chẳng phải là ví dụ của vấn đề khởi tạo tham lam được nói đến ở mục 5.1.1 của bài báo Bidirectional Typing sao?
  “Trong thiết lập ban đầu, thật khá đáng tiếc khi cách tiếp cận tham lam này lại nhạy cảm với thứ tự đối số. Tuy nhiên, nó có thể hoạt động tốt trong bối cảnh đa hình bậc cao có tính vị từ mà không có các dạng subtyping khác. ‘Vấn đề tabby-first’ không thể phát sinh, bởi cách duy nhất để một kiểu trở nên nhỏ hơn một cách nghiêm ngặt là trở nên đa hình hơn một cách nghiêm ngặt, và nếu đối số đầu tiên là đa hình thì phải khởi tạo 𝛼 bằng một kiểu đa hình, điều này vi phạm tính vị từ”