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

Question

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

Предполагая следующие ограничения:

• Все жители кончаются, т.е. нет дна.
• У всех жителей отсутствуют побочные эффекты.

Например (с использованием синтаксиса Haskell):

• Bool имеет двух жителей.
• (Bool, Bool) имеет четырех жителей.
• Bool -> (Bool, Bool) имеет шестнадцать жителей.
• forall a. a -> a имеет одного жителя.
• forall a. (a, a) -> (a, a) имеет четырех жителей.
• forall a b. a -> b -> a имеет одного жителя.
• forall a. a имеет ноль жителей.

Реализация алгоритма для первых трех тривиальна, но я не могу понять, как это сделать для остальных.

Answer 1

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

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

Сначала меня тоже беспокоили такие типы, как forall a. a -> a, Затем у меня было прозрение. Я понял, что тип forall a. a -> a была кодировка Могенсена-Скотта типа единицы. Следовательно, у него был только один житель. Так же, 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

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

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

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

2. Алгебраические типы данных, заданные следующими БНФ:

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

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

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

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

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

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

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

Хотя мы могли бы сделать тип данных алгебраического списка полиморфным (т.е. ∀ α. μ β. α * β + 1) и добавьте правило ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧ но мы этого не делаем, потому что это излишне усложняет ситуацию. Мы предполагаем, что полиморфный тип был специализирован для некоторого мономорфного типа.

Таким образом, первый шаг - отбросить все универсальные квантификаторы, кроме той, которая представляет квантификатор с фиксированной точкой. Например, тип ∀ α. ∀ β. α -> β -> α становится ∀ α. α -> β -> α,

Большинство преобразований являются простыми из-за кодирования Могенсена-Скотта. Например:

∀ α. α                       = μ α. 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 - отличное начало. Надеюсь это поможет.