Как систематически вычислять количество жителей данного типа?

Ответ 1

Я хотел решить ту же проблему. Следующее обсуждение, безусловно, помогло мне:

Нарушение алгебры алгебраических типов данных - почему это работает?

Сначала меня тоже беспокоили такие типы, как forall a. a -> a. Тогда у меня было прозрение. Я понял, что тип forall a. a -> a был кодировкой Mogensen-Scott тип устройства. Следовательно, у него был только один житель. Аналогично, forall a. a - это кодировка Могенсена-Скотта нижний тип. Следовательно, он имеет нулевых жителей. Рассмотрим следующие типы алгебраических данных:

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

Тип алгебраических данных представляет собой сумма продукты. Я использую синтаксис ⟦τ⟧ для обозначения числа жителей типа τ. Существуют два типа типов, которые я буду использовать в этой статье:

• Типы данных системы F, заданные следующим BNF:

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

• Алгебраические типы данных, заданные следующим BNF:

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

Вычисление числа жителей алгебраического типа данных довольно просто:

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

Например, рассмотрите тип данных списка μ β. α * β + 1:

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

Однако подсчет числа жителей типа данных System F не так прост. Тем не менее, это можно сделать. Для этого нам нужно преобразовать тип данных System F в эквивалентный тип алгебраических данных. Например, тип данных System F ∀ α. ∀ β. (α -> β -> β) -> β -> β эквивалентен типу данных алгебраического списка μ β. α * β + 1.

Первое, что нужно заметить, состоит в том, что хотя тип System 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 - отличное начало. Надеюсь, это поможет.