Tôi muốn giải quyết cùng một vấn đề. Các cuộc thảo luận sau đây chắc chắn đã giúp tôi rất nhiều:
Abusing the algebra of algebraic data types - why does this work?
Lúc đầu, tôi cũng đã gặp rắc rối bởi các loại như forall a. a -> a. Sau đó, tôi đã có một hiển linh. Tôi nhận ra rằng loại forall a. a -> a là số Mogensen-Scott encoding của số unit type. Do đó, nó chỉ có một cư dân. Tương tự, forall a. a là mã hóa Mogensen-Scott của bottom type. Do đó, nó có số dân không. Hãy xem xét các kiểu dữ liệu đại số sau:
data Bottom -- forall a. a
data Unit = Unit -- forall a. a -> a
data Bool = False | True -- forall a. a -> a -> a
data Nat = Succ Nat | Zero -- forall a. (a -> a) -> a -> a
data List a = Cons a (List a) | Nil -- forall a b. (a -> b -> b) -> b -> b
Một kiểu dữ liệu đại số là một sum của products. Tôi sẽ sử dụng cú pháp ⟦τ⟧ để biểu thị số lượng dân cư thuộc loại τ.Có hai loại định dạng tôi sẽ sử dụng trong bài viết này:
Hệ thống loại F liệu, được đưa ra bởi BNF sau đây:
τ = α
| τ -> τ
| ∀ α. τ
đại số kiểu dữ liệu, được đưa ra bởi BNF sau đây:
τ =
| α
| τ + τ
| τ * τ
| μ α. τ
Tính toán số lượng cư dân của một kiểu dữ liệu đại số là khá đơn giản:
⟦⟧ =
⟦τ¹ + τ²⟧ = ⟦τ¹⟧ + ⟦τ²⟧
⟦τ¹ * τ²⟧ = ⟦τ¹⟧ * ⟦τ²⟧
⟦μ α. τ⟧ = ⟦τ [μ α. τ/α]⟧
Ví dụ, hãy xem xét các kiểu dữ liệu danh sách μ β. α * β + 1:
⟦μ β. α * β + 1⟧ = ⟦(α * β + 1) [μ β. α * β + 1/β]⟧
= ⟦α * (μ β. α * β + 1) + 1⟧
= ⟦α * (μ β. α * β + 1)⟧ + ⟦1⟧
= ⟦α⟧ * ⟦μ β. α * β + 1⟧ + ⟦1⟧
= ⟦α⟧ * ⟦μ β. α * β + 1⟧ + 1
Tuy nhiên, tính toán số lượng cư dân của một kiểu dữ liệu hệ thống F không phải là quá đơn giản. Tuy nhiên, nó có thể được thực hiện. Để làm như vậy, chúng ta cần phải chuyển đổi kiểu dữ liệu System F thành một kiểu dữ liệu đại số tương đương. Ví dụ, kiểu dữ liệu Hệ thống F ∀ α. ∀ β. (α -> β -> β) -> β -> β tương đương với kiểu dữ liệu danh sách đại số μ β. α * β + 1. Điều đầu tiên cần lưu ý là mặc dù hệ thống F loại ∀ α. ∀ β. (α -> β -> β) -> β -> β có hai định lượng phổ nhưng kiểu dữ liệu danh sách đại số μ β. α * β + 1 chỉ có một (số điểm cố định) định lượng (tức là loại dữ liệu danh sách đại số là đơn).
Mặc dù chúng tôi có thể làm cho loại dữ liệu danh sách đại số đa hình (tức là ∀ α. μ β. α * β + 1) và thêm quy tắc ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧ nhưng chúng tôi không làm như vậy bởi vì nó không cần thiết làm phức tạp vấn đề. Chúng tôi giả định rằng các loại đa hình đã được chuyên môn hóa cho một số loại đơn hình.
Do đó, bước đầu tiên là xóa tất cả các số lượng phổ dụng ngoại trừ số lượng đại diện cho định lượng "điểm cố định". Ví dụ: loại ∀ α. ∀ β. α -> β -> α trở thành ∀ α. α -> β -> α.
Hầu hết các chuyển đổi rất đơn giản do mã hóa Mogensen-Scott. Ví dụ:
∀ α. α = μ α. 0 -- bottom type
∀ α. α -> α = μ α. 1 + 0 -- unit type
∀ α. α -> α -> α = μ α. 1 + 1 + 0 -- boolean type
∀ α. (α -> α) -> α -> α = μ α. (α * 1) + 1 + 0 -- natural number type
∀ β. (α -> β -> β) -> β -> β = μ β. (α * β * 1) + 1 + 0 -- list type
Tuy nhiên, một số chuyển đổi không đơn giản như vậy. Ví dụ: ∀ α. α -> β -> α không đại diện cho loại dữ liệu mã hóa Mogensen-Scott hợp lệ. Tuy nhiên, chúng tôi có thể nhận được câu trả lời chính xác bằng cách tung hứng các loại một bit:
⟦∀ α. α -> β -> α⟧ = ⟦β -> ∀ α. α -> α⟧
= ⟦∀ α. α -> α⟧^⟦β⟧
= ⟦μ α. 1 + 0⟧^⟦β⟧
= ⟦μ α. 1⟧^⟦β⟧
= ⟦1⟧^⟦β⟧
= 1^⟦β⟧
= 1
Đối với các loại khác mà chúng tôi cần phải sử dụng một số thủ đoạn gian trá:
∀ α. (α, α) -> (α, α) = (∀ α. (α, α) -> α, ∀ α. (α, α) -> α)
= (∀ α. α -> α -> α, ∀ α. α -> α -> α)
⟦∀ α. α -> α -> α⟧ = ⟦μ α. 1 + 1 + 0⟧
= ⟦μ α. 2⟧
= ⟦2⟧
= 2
⟦∀ α. (α, α) -> (α, α)⟧ = ⟦∀ α. α -> α -> α⟧ * ⟦∀ α. α -> α -> α⟧
= 2 * 2
= 4
Mặc dù có một thuật toán đơn giản mà sẽ cho chúng ta những số của những cư dân thuộc loại mã hóa Mogensen-Scott nhưng tôi không thể nghĩ ra bất kỳ thuật toán chung nào sẽ cho chúng ta số lượng cư dân của bất kỳ loại đa hình nào.
Trong thực tế, tôi có cảm giác ruột rất mạnh để tính số lượng cư dân của bất kỳ loại đa hình nào nói chung là một vấn đề không thể giải quyết được. Do đó, tôi tin rằng không có thuật toán nào sẽ cho chúng ta số lượng cư dân của bất kỳ loại đa hình nào nói chung.
Tuy nhiên, tôi tin rằng việc sử dụng các loại mã hóa Mogensen-Scott là một khởi đầu tuyệt vời. Hi vọng điêu nay co ich.