Nên đọc ký pháp hệ thống kiểu như thế nào?

 (langdev.stackexchange.com)
1 điểm bởi GN⁺ 2023-08-17 | 1 bình luận | Chia sẻ qua WhatsApp
  • Dù ký pháp hệ thống kiểu khác nhau giữa các tài liệu, nếu nắm được khung chung gồm ngữ pháp, quan hệ gán kiểu và quy tắc suy diễn thì có thể theo được hầu hết các biến thể
  • Hệ thống kiểu hoạt động trên cú pháp trừu tượng của ngôn ngữ, nên trước hết cần phân biệt bằng ngữ pháp giữa hạng (term) có kiểu và bản thân kiểu
  • ⊢ e: τ là phán đoán gán kiểu mang nghĩa “biểu thức e có kiểu τ”, và được đọc như một quy tắc suy diễn trong đó nếu mọi điều kiện phía trên gạch ngang đều đúng thì kết luận phía dưới cũng đúng
  • Khi có biến và hàm, ngữ cảnh được gắn vào như Γ ⊢ e: τ để theo dõi tên biến và kiểu trong phạm vi hiện tại
  • Nhiều quy tắc gán kiểu có thể được đọc như một hàm kiểm tra kiểu đệ quy, nhưng không phải mọi phán đoán logic đều trực tiếp trở thành thuật toán kiểm tra kiểu có thể quyết định được

Ký pháp hệ thống kiểu bắt đầu từ ngữ pháp

  • Hệ thống kiểu là một hệ thống cú pháp của ngôn ngữ lập trình, tức là một tập quy tắc hoạt động trên cú pháp trừu tượng của ngôn ngữ
  • Phần mô tả hệ thống kiểu toàn diện thường trước hết trình bày cấu trúc cú pháp được xử lý bằng ngữ pháp, rồi biểu diễn nó bằng ký pháp BNF
  • Ngay cả trong ngôn ngữ kiểu đơn giản nhất, cú pháp cũng được chia thành hai nhóm lớn
    • e: biểu thức (expression) có kiểu
    • τ: kiểu (type) gắn cho biểu thức
  • Ngôn ngữ ví dụ có các biểu thức gồm literal boolean, literal số nguyên, biểu thức điều kiện, phép toán số học và phép so sánh; còn kiểu thì dùng Bool và Int
  • Tùy tài liệu, ký hiệu kiểu có thể dùng t, T, σ hay các chữ cái Hy Lạp thường khác thay cho τ, nhưng cấu trúc tổng thể thì tương tự nhau
  • Những ngôn ngữ phức tạp hơn có thể bao gồm thêm nhiều nhóm cú pháp như câu lệnh, pattern trong pattern matching, v.v.

Đọc quan hệ gán kiểu và phán đoán

  • Sau khi xác định ngữ pháp, người ta thường định nghĩa quan hệ gán kiểu ở dạng e : τ
    • 1 + 2 : Int nghĩa là “1 + 2 có kiểu Int”
    • 1 + 2 : Bool nói rằng cùng biểu thức đó có kiểu Bool, nên là sai
    • true + 2 : Int thì bản thân biểu thức đã không hợp lệ, nên không có kiểu nào cả
  • ⊢ e : τ là phán đoán gán kiểu, và ⊢ có thể đọc là “mệnh đề phía sau là đúng”
  • Quy tắc không có gì phía trên gạch ngang là một tiên đề (axiom) luôn đúng
    • ⊢ true : Bool
    • ⊢ false : Bool
    • các quy tắc literal số nguyên như ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Quy tắc có cả phần trên và dưới gạch ngang là quy tắc suy diễn
    • Nếu mọi điều kiện phía trên đều đúng thì kết luận phía dưới đúng
    • Nếu e₁ và e₂ đều là Int thì e₁ + e₂ là Int
    • Nếu e₁ và e₂ đều là Int thì e₁ < e₂ là Bool

Biểu thức điều kiện và biến kiểu

  • Hai nhánh của if ... then ... else ... có thể mang bất kỳ kiểu nào, nhưng phải cùng một kiểu
    • if true then 1 else 2 là hợp lệ
    • if true then false else true là hợp lệ
    • if true then 1 else true là không hợp lệ
  • Để biểu diễn điều này, quy tắc dùng biến τ để chỉ kiểu của các nhánh
    • Biểu thức điều kiện e₁ phải là Bool
    • Nhánh then là e₂ và nhánh else là e₃ phải có cùng kiểu τ
    • Kiểu của toàn bộ biểu thức điều kiện cũng là τ
  • Khi áp dụng quy tắc, có thể chọn bất kỳ kiểu nào cho τ, nhưng trong cùng một quy tắc thì phải giữ lựa chọn đó nhất quán

Đọc quy tắc suy diễn như thuật toán

  • Ký pháp này đến từ logic hình thức, và cách đặc tả hệ thống kiểu đặc biệt giống với natural deduction
  • Những quy tắc như vậy được dùng để xây dựng chứng minh hình thức về các thuộc tính của hệ thống, và rất quan trọng để chứng minh các tính chất như type safety
  • Một phán đoán logic không phải lúc nào cũng tương ứng trực tiếp với một thuật toán kiểm tra kiểu có thể quyết định được
  • Trong nhiều trường hợp, ⊢ e : τ có thể được đọc như một hàm nhận biểu thức e và cho ra kiểu τ
    • Mỗi dạng biểu thức trong ngữ pháp thường có một quy tắc tương ứng
    • Mỗi quy tắc gán kiểu có thể xem như một nhánh của hàm kiểm tra kiểu đệ quy
  • Hàm infer trong ví dụ tương ứng với luồng sau
    • true hoặc false cho ra Bool
    • literal số nguyên cho ra Int
    • e₁ + e₂ kiểm tra kết quả suy ra của hai vế đều là Int, rồi cho ra Int
    • e₁ < e₂ kiểm tra cả hai đều là Int, rồi cho ra Bool
    • if e₁ then e₂ else e₃ kiểm tra điều kiện có phải Bool không, kiểm tra hai nhánh có cùng kiểu không, rồi trả về kiểu đó
  • Dù không phải lúc nào cũng chuyển thẳng thành thuật toán được, nếu xem e là đầu vào và τ là đầu ra trong phán đoán thì sẽ dễ hiểu luồng thông tin hơn

Biến và ngữ cảnh

  • Để xử lý ngôn ngữ lập trình hữu dụng thì cần có biến, và ví dụ mở rộng thêm hàm để thành dạng simply typed lambda calculus
  • Ngữ pháp mở rộng bao gồm
    • biến x
    • trừu tượng hàm λx:τ. e
    • áp dụng hàm e e
    • kiểu hàm τ → τ
  • λx:τ. e tương ứng với (x:τ) => e trong TypeScript, còn f x tương ứng với f(x)
  • Kiểu của biến phụ thuộc vào ngữ cảnh nơi biến xuất hiện, nên không thể viết quy tắc chỉ bằng dạng đơn giản ⊢ x : ???
  • Vì vậy phán đoán gán kiểu được mở rộng thành Γ ⊢ e : τ
    • Γ là ngữ cảnh hoặc môi trường kiểu
    • ⊢ phân tách các giả định ngữ cảnh ở bên trái với mệnh đề cần chứng minh ở bên phải
    • Có thể đọc là “dưới ngữ cảnh Γ, biểu thức e có kiểu τ”
  • Về mặt thuật toán, Γ có thể được xem như một đầu vào bổ sung dạng Map<Variable, Type>
  • Về mặt hình thức, ngữ cảnh cũng được mô tả như một cấu trúc cú pháp
    • ∅: ngữ cảnh rỗng
    • Γ, x:τ: ngữ cảnh có thêm ràng buộc biến
    • Đôi khi • được dùng thay cho ∅ để chỉ ngữ cảnh rỗng
  • Trong cách biểu diễn này, ngữ cảnh gần với một association list ánh xạ tên biến sang kiểu

Ngữ cảnh làm gì trong quy tắc

  • Nhiều quy tắc gán kiểu không thay đổi ngữ cảnh mà chỉ truyền nó đi nguyên vẹn
    • Γ ⊢ true : Bool
    • Nếu Γ ⊢ e₁ : Int và Γ ⊢ e₂ : Int thì Γ ⊢ e₁ + e₂ : Int
  • Trong quy tắc dùng biến và lambda, ngữ cảnh đóng vai trò then chốt
    • Nếu x:τ ∈ Γ thì Γ ⊢ x : τ
    • Nếu Γ, x:τ₁ ⊢ e : τ₂ thì Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Khi kiểm tra kiểu phần thân e của lambda, ngữ cảnh được mở rộng bằng ràng buộc mới x:τ₁
  • Quy tắc biến nói rằng nếu có ràng buộc cho biến trong ngữ cảnh hiện tại thì biến đó mang kiểu tương ứng
  • Ngữ cảnh được dùng như một cơ chế truyền thông tin giữa quy tắc lambda và quy tắc biến
  • Để đơn giản hóa, kiểu đặc tả hệ thống kiểu này thường giả định mọi biến đã được phân giải và làm cho duy nhất từ trước, nên không xử lý variable shadowing
  • Quy tắc áp dụng hàm kiểm tra đồng thời kiểu của biểu thức hàm và biểu thức đối số
    • e₁ phải có kiểu τ₁ → τ₂
    • e₂ phải có kiểu τ₁
    • Kiểu của toàn bộ phép áp dụng e₁ e₂ sẽ là τ₂

Một số ký pháp bổ sung thường gặp

  • Quy tắc suy diễn không phải lúc nào cũng chỉ được viết theo chiều dọc
    • Nhiều điều kiện có thể được đặt song song theo hàng ngang
    • Cách bố trí dọc và ngang có thể trộn lẫn trong cùng một quy tắc
  • Các điều kiện phía trên gạch ngang thường là những phán đoán khác, nhưng cũng có thể là điều kiện phụ (side condition), tức một điều kiện boolean bất kỳ
    • x:τ ∈ Γ trong quy tắc biến là một ví dụ
    • Trong hệ thống kiểu mang tính thuật toán, có thể xuất hiện α fresh, nghĩa là α phải là một biến kiểu mới, khác với các biến kiểu khác

Subtyping

  • Subtyping là quan hệ xử lý tính tương thích giữa các kiểu theo cách yếu hơn sự bằng nhau nghiêm ngặt, và phải được định nghĩa tường minh
  • Thường được viết là τ₁ <: τ₂ và đọc là “τ₁ là subtype của τ₂”
  • Một quan hệ subtyping đơn giản có thể đưa vào kiểu cao nhất ⊤ và kiểu thấp nhất ⊥
    • τ <: τ: mọi kiểu là subtype của chính nó
    • τ <: ⊤: mọi kiểu là subtype của ⊤
    • ⊥ <: τ: ⊥ là subtype của mọi kiểu
  • Quy tắc đầu tiên là quy tắc phản xạ, thường được viết tắt là refl
  • Muốn cho phép subtyping thì mỗi quy tắc gán kiểu có hỗ trợ nó phải dùng quan hệ này một cách tường minh
    • Trong quy tắc áp dụng hàm, nếu kiểu đối số τ₁ là subtype của kiểu tham số τ₂ thì có thể cho phép áp dụng

Nhiều ngữ cảnh và kiểm tra kiểu hai chiều

  • Một số hệ thống kiểu định nghĩa phán đoán gán kiểu có chứa nhiều hơn một ngữ cảnh
    • Ngữ cảnh thứ hai thường được gọi là Δ
    • Γ;Δ ⊢ e : τ thường dùng khi cả hai ngữ cảnh đều đóng vai trò đầu vào
    • Γ ⊢ e : τ ⊣ Δ thường dùng khi Δ đóng vai trò đầu ra
  • Ngữ cảnh thứ hai được dùng khác nhau tùy mục đích
    • Nó có thể cho phép chỉ được tham chiếu một số biến nhất định bên trong một biểu thức nào đó
    • Trong ngôn ngữ lập trình có ý thức về tài nguyên, nó có thể được dùng làm ngữ cảnh đầu ra để theo dõi biến nào đã bị tiêu thụ
  • Kiểm tra kiểu hai chiều là một cách tiếp cận để thực hiện suy diễn kiểu không cục bộ ở mức hạn chế mà không cần bộ giải ràng buộc
  • Hệ thống hai chiều tách phán đoán thông thường Γ ⊢ e : τ thành hai phán đoán chuyên biệt
    • Γ ⊢ e ⇐ τ: phán đoán kiểm tra (checking) xác nhận biểu thức e có kiểu kỳ vọng τ; về mặt thuật toán, τ là đầu vào
    • Γ ⊢ e ⇒ τ: phán đoán suy diễn (inference) dùng khi không có thông tin về kiểu kỳ vọng; về mặt thuật toán, τ là đầu ra
  • Hai phán đoán này được định nghĩa đệ quy lẫn nhau để truyền thông tin kiểu theo cả hai hướng
  • Với cách này, có thể lược bỏ một phần chú thích kiểu; quy tắc kiểm tra cho lambda abstraction có thể lấy kiểu tham số từ kiểu hàm kỳ vọng, nên có thể bỏ chú thích ở biến ràng buộc

Bài viết liên quan

1 bình luận

 
GN⁺ 2023-08-17
Ý kiến trên Hacker News

  • Guy Steele từng có một bài nói về chủ đề này. Ông cũng đặt tên để có thể tìm kiếm cho một số ký pháp, chẳng hạn như sơ đồ quy tắc suy luận hai chiều
    Ông gọi chúng là siêu ký pháp khoa học máy tính, nhưng cá nhân tôi thấy chúng gần với lý thuyết ngôn ngữ lập trình hơn. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Ký pháp này có thể truy ngược tới Frege. Nếu không biết cần tìm gì thì rất khó tìm, nhưng bài này có vẻ là một bản tóm tắt khá tốt: https://plato.stanford.edu/entries/frege-logic
    Ký hiệu turnstile |- đã được dùng, và đường ngang trong lớp học được gọi là “Fregescher Schlussstrich”, tức nét kết luận của Frege, dường như ban đầu là một phần của chính turnstile rồi trong ký pháp hiện đại mới trở thành một thành phần riêng

    • “Schlussstrich” có lẽ nên dịch gần hơn là nét diễn dịch hoặc nét suy luận

  • Types and Programming Languages của Benjamin C. Pierce là một giáo trình hay có đề cập các nội dung như thế này

    • Trớ trêu là TAPL lại khá mơ hồ khi giải thích ý nghĩa cơ bản của cú pháp mà chính nó dùng. Câu trả lời này rõ ràng hơn TAPL vài bậc độ lớn

  • Dù học chuyên ngành khoa học máy tính, tôi vẫn bối rối về khác biệt ý nghĩa giữa |– và |=, cũng như các biến được dùng nằm ở mức siêu cú pháp nào
    Trớ trêu thay, một nguyên nhân là bản thân ký pháp lại không có kiểu tường minh

  • Với những ai còn phân vân có nên đọc không: bài này giải thích ký pháp hệ thống kiểu xuất hiện trong các bài báo khoa học máy tính, về cơ bản là phần nhập môn về ký pháp BNF, quy tắc suy luận, v.v. dành cho hệ thống kiểu
    Có vẻ là một bản tóm tắt tốt

    • Thành thật mà nói, tôi chỉ cần một cheatsheet cho biết các ký hiệu được đọc thành từ tiếng Anh như thế nào
      Tôi hiểu khái niệm logic của việc áp dụng kiểu, nhưng vì không thường xuyên đọc bài báo khoa học máy tính nên liên hệ giữa ký hiệu và ý nghĩa không thật sự bám trong đầu
    • Việc những thứ như thế này đã được trừu tượng hóa kỹ lưỡng qua nhiều năm cho thấy một khía cạnh rất đúng chất khoa học máy tính

  • Trong ví dụ, 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 có nghĩa là “𝗍𝗋𝗎𝖾+2 có kiểu 𝖨𝗇𝗍”, nhưng bài viết nói nó còn kỳ lạ hơn vì bản thân biểu thức 𝗍𝗋𝗎𝖾+2 là vô nghĩa và cũng không có kiểu
    Tuy nhiên trong Python, True + 2 thực sự là số nguyên và giá trị là 3. Chuyện có nên như vậy hay không là một vấn đề khác, nhưng thực tế là như vậy

    • Nếu bạn cho rằng True + 2 là hợp lý, thì chỉ cần tự định nghĩa quy tắc phán đoán cho phép điều đó
      Logic và lý thuyết hệ thống kiểu không quan tâm bản thân bạn dùng các tiên đề và quy tắc suy luận nào, chúng chỉ giúp suy luận về các quy tắc đó và sự tương tác giữa chúng. Ví dụ có thể đặt |- True : Bool, |- True : Int, hoặc nếu chỉ muốn cho phép trong một biểu thức cụ thể thì có thể tạo quy tắc suy ra |- True + x: Int từ |- x : Int
    • Cái này chẳng phải khác nhau tùy ngôn ngữ sao? Ví dụ trong C, true được ánh xạ thành 1 nên true+1=2
    • Dù True + 2 không gây lỗi trong Python hay C, nó vẫn là điều ngớ ngẩn vì làm cho ngữ nghĩa của ngôn ngữ khó suy luận hơn chỉ để cho lập trình viên một chút đường cú pháp

  • Hay đấy. Tôi đã thắc mắc suốt mấy năm nhưng không biết nên dùng từ khóa nào để tìm hiểu thêm

  • Đôi khi thấy khó chịu vô cớ khi ai đó đem kiến thức bí truyền mà mình vất vả học được ra chia sẻ miễn phí ;) Giá mà lúc tôi học có bài như thế này thì tốt biết mấy. Hy vọng việc dễ tiếp cận hơn sẽ làm giảm số ngôn ngữ tệ hại

  • Khi đọc Ada Reference Manual, tôi nhận ra ngay loại cú pháp này. Dù không biết tên của nó, nhưng thấy trong một trường hợp sử dụng thực tế thì khá thú vị, và toàn bộ ngôn ngữ được định nghĩa bằng kiểu ký pháp đó
    Ví dụ: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Có vẻ đây là chỗ thích hợp để truyền bá một “ngọn đồi” mà tôi đã quyết định sẽ theo đến cùng. Trong định dạng chú thích kiểu dùng dấu hai chấm, khoảng trắng ở hai bên dấu hai chấm phải bằng nhau
    Với tôi, tình cờ có hai ký hiệu khác nhau trông giống nhau, tức đều được viết bằng hai dấu chấm. Một cái là dấu hai chấm nhãn, nơi phần trước giới thiệu phần sau, hoặc bên trái là nhãn của bên phải, như trong tiếng Anh; phần mở đầu block của Python, cặp khóa-giá trị, cặp tên-giá trị trong struct của C hay Rust thuộc loại này
    Cái còn lại là chú thích kiểu mượn từ toán học. Đây là một quan hệ nhị phân, và quan hệ nhị phân thì đặt khoảng trắng hai bên trái phải như nhau. Cũng như ta không viết x= 1, x> y, x+ z, nên viết x : X mới tự nhiên chứ không phải x: X
    Khi thấy a: b, tôi lập tức đọc nó như dấu hai chấm nhãn; nếu đó là chú thích kiểu, lần nào cũng cần một bước chuyển đổi tinh thần rất nhỏ nhưng bổ sung. Đây là chuyện về cú pháp ngôn ngữ lập trình, và cá nhân tôi thích x : X hơn X x rất nhiều
    [1] “Evangelion” là một từ hay bắt nguồn từ εὐαγγέλιον, nghĩa là tin mừng. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Có thể có vài hiểu nhầm. Trong văn bản toán học cũng thật sự có ký pháp đặt nhiều khoảng trắng hơn bên phải dấu hai chấm như f: X->Y; trong 3 cuốn sách tôi kiểm tra, 1 cuốn chỉ dùng ký pháp đó
      Ngoài ra, cái đó vẫn gần với việc gắn nhãn, tức là gắn nhãn cho một dạng ánh xạ cụ thể. Trường hợp dấu hai chấm trong toán học thật sự được dùng với nghĩa khác là khi dùng như viết tắt của such that, ví dụ trong định nghĩa tập hợp như { x : x \in IN and x | 2} hoặc thường dùng cùng lượng từ
    • Một góc nhìn thú vị. Điều nói về bước tinh thần bổ sung giống với cảm giác của tôi khi đọc ký pháp X x phổ biến. x: X với tôi tự nhiên hơn nhiều, và cũng cảm thấy gần với cách dùng dấu hai chấm trong ngôn ngữ tự nhiên
      Kiểu như có một mệnh đề, rồi phần sau dấu hai chấm giải thích chi tiết hơn mệnh đề đó; type cũng là thông tin bổ sung về thứ ở bên trái, nên rất khớp
    • Trong type theory, tôi nghĩ thông lệ chuẩn thường là đặt khoảng trắng bằng nhau hai bên dấu hai chấm như t[khoảng trắng]:[khoảng trắng]T
      Toàn bộ type theory có nhiều mặt lộn xộn và thiếu nhất quán, nhưng riêng trường hợp này thì là một ví dụ hiếm hoi nơi mọi người khá nhất quán. Tôi tò mò hồi đại học mình đã viết thế nào nên xem lại, và thấy mình cũng viết đối xứng khá đẹp: https://dvt.name/logic/horse2.pdf
    • x: X tương ứng với cách dùng “phần giải thích nằm sau dấu hai chấm”
      Tức là kiểu như variable x: It’s an X.
    • age: int có thể dễ dàng đọc lại sang tiếng Anh thành “person’s age: an integer”
      Vì vậy dấu hai chấm chưa bao giờ khiến tôi thấy quá khó chịu