algorithm - ¿Cómo calcular sistemáticamente el número de habitantes de un tipo dado?

type-theory system-f

Question

¿Cómo calcular sistemáticamente el número de habitantes de un tipo dado en el Sistema F?

Asumiendo las siguientes restricciones:

• Todos los habitantes terminan, es decir, sin fondo.
• Todos los habitantes carecen de efectos secundarios.

Por ejemplo (usando la sintaxis de Haskell):

• Bool tiene dos habitantes.
• (Bool, Bool) tiene cuatro habitantes.
• Bool -> (Bool, Bool) tiene dieciséis habitantes.
• forall a. a -> a forall a. a -> a tiene un habitante.
• forall a. (a, a) -> (a, a) forall a. (a, a) -> (a, a) tiene cuatro habitantes.
• forall a b. a -> b -> a forall a b. a -> b -> a tiene un habitante.
• forall a. a forall a. a tiene cero habitantes.

Implementar un algoritmo para los primeros tres es trivial, pero no puedo averiguar cómo hacerlo para los otros tres.

Answer 1

Quería resolver el mismo problema. La siguiente discusión sin duda me ayudó mucho:

Abusar del álgebra de los tipos de datos algebraicos: ¿por qué funciona esto?

Al principio, yo también estaba preocupado por tipos como el de todos forall a. a -> a forall a. a -> a . Entonces, tuve una epifanía. Me di cuenta de que el tipo para todos forall a. a -> a forall a. a -> a era la codificación Mogensen-Scott del tipo de unidad . Por lo tanto, tenía un solo habitante. Del mismo modo, para todos forall a. a forall a. a es la codificación Mogensen-Scott del tipo inferior . Por lo tanto, tiene cero habitantes. Considere los siguientes tipos de datos algebraicos:

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

Un tipo de datos algebraico es una sum de products . ⟦τ⟧ la sintaxis ⟦τ⟧ para indicar el número de habitantes del tipo τ . Hay dos tipos de tipos que usaré en este artículo:

1. Tipos de datos del sistema F, dados por el siguiente BNF:

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

2. Tipos de datos algebraicos, dados por el siguiente BNF:

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

El cálculo del número de habitantes de un tipo de datos algebraico es bastante sencillo:

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

Por ejemplo, considere el tipo de datos de lista μ β. α * β + 1 μ β. α * β + 1 :

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

Sin embargo, calcular el número de habitantes de un tipo de datos del Sistema F no es tan sencillo. Sin embargo, se puede hacer. Para hacerlo, necesitamos convertir el tipo de datos del Sistema F en un tipo de datos algebraico equivalente. Por ejemplo, el tipo de datos del Sistema F ∀ α. ∀ β. (α -> β -> β) -> β -> β ∀ α. ∀ β. (α -> β -> β) -> β -> β ∀ α. ∀ β. (α -> β -> β) -> β -> β es equivalente al tipo de datos de la lista algebraica μ β. α * β + 1 μ β. α * β + 1 .

Lo primero que hay que notar es que a pesar del sistema F tipo type ∀ α. ∀ β. (α -> β -> β) -> β -> β ∀ α. ∀ β. (α -> β -> β) -> β -> β ∀ α. ∀ β. (α -> β -> β) -> β -> β tiene dos cuantificadores universales pero el tipo de datos de la lista algebraica μ β. α * β + 1 μ β. α * β + 1 tiene un solo cuantificador (punto fijo) (es decir, el tipo de datos de la lista algebraica es monomórfico).

Aunque podríamos hacer el tipo de datos de lista algebraica polimórfico (es decir, ∀ α. μ β. α * β + 1 ) y agregar la regla ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧ ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧ ⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧ embargo, no lo hacemos porque complica innecesariamente las cosas. Suponemos que el tipo polimórfico se ha especializado a algún tipo monomórfico.

Por lo tanto, el primer paso es eliminar todos los cuantificadores universales, excepto el que representa el cuantificador de "punto fijo". Por ejemplo, el tipo ∀ α. ∀ β. α -> β -> α ∀ α. ∀ β. α -> β -> α ∀ α. ∀ β. α -> β -> α convierte en ∀ α. α -> β -> α ∀ α. α -> β -> α .

La mayoría de las conversiones son sencillas debido a la codificación Mogensen-Scott. Por ejemplo:

∀ α. α = μ α. 0 -- bottom type
∀ α. α -> α = μ α. 1 + 0 -- unit type
∀ α. α -> α -> α = μ α. 1 + 1 + 0 -- boolean type
∀ α. (α -> α) -> α -> α = μ α. (α * 1) + 1 + 0 -- natural number type
∀ β. (α -> β -> β) -> β -> β = μ β. (α * β * 1) + 1 + 0 -- list type

Sin embargo, algunas conversiones no son tan sencillas. Por ejemplo, ∀ α. α -> β -> α ∀ α. α -> β -> α no representa un tipo de datos codificado de Mogensen-Scott válido. Sin embargo, podemos obtener la respuesta correcta haciendo malabares con los tipos un poco:

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

Para otros tipos necesitamos usar algunos trucos:

∀ α. (α, α) -> (α, α) = (∀ α. (α, α) -> α, ∀ α. (α, α) -> α)
= (∀ α. α -> α -> α, ∀ α. α -> α -> α)
⟦∀ α. α -> α -> α⟧ = ⟦μ α. 1 + 1 + 0⟧
= ⟦μ α. 2⟧
= ⟦2⟧
= 2
⟦∀ α. (α, α) -> (α, α)⟧ = ⟦∀ α. α -> α -> α⟧ * ⟦∀ α. α -> α -> α⟧
= 2 * 2
= 4

Aunque hay un algoritmo simple que nos dará el número de habitantes de un tipo codificado de Mogensen-Scott, no puedo pensar en ningún algoritmo general que nos dé el número de habitantes de cualquier tipo polimórfico.

De hecho, tengo el presentimiento muy fuerte de que calcular el número de habitantes de cualquier tipo polimórfico en general es un problema indecidible. Por lo tanto, creo que no hay algoritmo que nos dé el número de habitantes de cualquier tipo polimórfico en general.

Sin embargo, creo que usar tipos codificados de Mogensen-Scott es un gran comienzo. Espero que esto ayude.