algorithm - 如何系统地计算给定类型的居民数量？

Question

如何系统地计算系统 F 中给定类型的居民数量？

假设有以下限制:

• 所有居民都终止，即没有底部。
• 所有居民都没有副作用。

例如(使用 Haskell 语法):

• Bool 有两个居民。
• (Bool, Bool) 有四个居民。
• Bool -> (Bool, Bool) 有 16 个居民。
• forall a. a -> a 有一个居民。
• forall a. (a, a) -> (a, a) 有四个居民。
• forall a b。 a -> b -> a 有一个居民。
• forall a. a 有零个居民。

为前三个实现算法很简单，但我不知道如何为其他的实现。

Answer 1

我想解决同样的问题。下面的讨论对我帮助很大:

Abusing the algebra of algebraic data types - why does this work?

起初，我也被诸如 forall a 这样的类型所困扰。一个 -> 一个。然后，我顿悟了。我意识到类型 forall a。 a -> a 是 Mogensen-Scott encoding的 unit type .因此，它只有一个居民。同样，forall a。 a 是 bottom type 的 Mogensen-Scott 编码.因此，它的居民为零。考虑以下代数数据类型:

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

代数数据类型是 sum的 products .我将使用语法 ⟦τ⟧ 来表示 τ 类型的居民数量。我将在本文中使用两种类型:

1. 系统 F 数据类型，由以下 BNF 给出:

   τ = α
     | τ -> τ
     | ∀ α. τ
   

2. 代数数据类型，由以下 BNF 给出:

   τ = 𝕟
     | α
     | τ + τ
     | τ * τ
     | μ α. τ
   

计算代数数据类型的居民数非常简单:

⟦𝕟⟧       = 𝕟
⟦τ¹ + τ²⟧ = ⟦τ¹⟧ + ⟦τ²⟧
⟦τ¹ * τ²⟧ = ⟦τ¹⟧ * ⟦τ²⟧
⟦μ α. τ⟧  = ⟦τ [μ α. τ / α]⟧

例如，考虑列表数据类型 μ β。 α * β + 1:

⟦μ β. α * β + 1⟧ = ⟦(α * β + 1) [μ β. α * β + 1 / β]⟧
                 = ⟦α * (μ β. α * β + 1) + 1⟧
                 = ⟦α * (μ β. α * β + 1)⟧ + ⟦1⟧
                 = ⟦α⟧ * ⟦μ β. α * β + 1⟧ + ⟦1⟧
                 = ⟦α⟧ * ⟦μ β. α * β + 1⟧ +  1

但是，计算 System F 数据类型的居民数并不是那么简单。然而，这是可以做到的。为此，我们需要将 System F 数据类型转换为等效的代数数据类型。例如，系统 F 数据类型 ∀ α。 ∀ β。 (α -> β -> β) -> β -> β 等同于代数列表数据类型 μ β。 α * β + 1.

首先要注意的是，虽然系统F类型∀α。 ∀ β。 (α -> β -> β) -> β -> β 有两个通用量词，但代数列表数据类型 μ β。 α * β + 1 只有一个(定点)量词(即代数列表数据类型是单态的)。

尽管我们可以使代数列表数据类型成为多态的(即 ∀ α. μ β. α * β + 1)并添加规则 ⟦∀ α。 τ⟧ = ∀ α。 ⟦τ⟧ 但我们不这样做，因为它不必要地使事情复杂化。我们假设多态类型已经专门化为一些单态类型。

因此，第一步是删除所有通用量词，除了代表“不动点”量词的量词。例如，类型 ∀ α。 ∀ β。 α -> β -> α 变成 ∀ α。 α -> β -> α.

由于 Mogensen-Scott 编码，大多数转换都很简单。例如:

∀ α. α                       = μ α. 0                   -- bottom type

∀ α. α -> α                  = μ α. 1 + 0               -- unit type

∀ α. α -> α -> α             = μ α. 1 + 1 + 0           -- boolean type

∀ α. (α -> α) -> α -> α      = μ α. (α * 1) + 1 + 0     -- natural number type

∀ β. (α -> β -> β) -> β -> β = μ β. (α * β * 1) + 1 + 0 -- list type

但是，有些转换并不是那么简单。例如，∀α。 α -> β -> α 不代表有效的 Mogensen-Scott 编码数据类型。尽管如此，我们还是可以通过稍微调整一下类型来得到正确的答案:

⟦∀ α. α -> β -> α⟧ = ⟦β -> ∀ α. α -> α⟧
                   = ⟦∀ α. α -> α⟧ ^ ⟦β⟧ 
                   = ⟦μ α. 1 + 0⟧ ^ ⟦β⟧ 
                   = ⟦μ α. 1⟧ ^ ⟦β⟧ 
                   = ⟦1⟧ ^ ⟦β⟧ 
                   =  1 ^ ⟦β⟧
                   =  1

对于其他类型，我们需要使用一些技巧:

∀ α. (α, α) -> (α, α) = (∀ α. (α, α) -> α, ∀ α. (α, α) -> α)
                      = (∀ α. α -> α -> α, ∀ α. α -> α -> α)

⟦∀ α. α -> α -> α⟧ = ⟦μ α. 1 + 1 + 0⟧
                   = ⟦μ α. 2⟧
                   = ⟦2⟧
                   =  2

⟦∀ α. (α, α) -> (α, α)⟧ = ⟦∀ α. α -> α -> α⟧ * ⟦∀ α. α -> α -> α⟧
                        = 2 * 2
                        = 4

虽然有一个简单的算法可以为我们提供 Mogensen-Scott 编码类型的居民数量，但我想不出任何通用算法可以为我们提供任何多态类型的居民数量。

事实上，我有一种非常强烈的直觉，即计算任何多态类型的居民数量通常是一个不可判定的问题。因此，我相信没有任何算法可以为我们提供任何多态类型的居民数量。

不过，我相信使用 Mogensen-Scott 编码类型是一个很好的开始。希望这会有所帮助。