haskell - tipos - ¿Qué son los cuantificadores de tipo?

reglas de cuantificadores logicos

Question

Muchas lenguas tipificadas estáticamente tienen polimorfismo paramétrico. Por ejemplo en C # se puede definir:

T Foo<T>(T x){ return x; }

En un sitio de llamadas puedes hacer:

int y = Foo<int>(3);

Estos tipos a veces también se escriben así:

Foo :: forall T. T -> T

He oído a la gente decir que "forall es como lambda-abstracción en el nivel de tipo". Entonces, Foo es una función que toma un tipo (por ejemplo, int), y produce un valor (por ejemplo, una función de tipo int -> int). Muchos idiomas infieren el parámetro de tipo, de modo que puede escribir Foo(3) lugar de Foo<int>(3) .

Supongamos que tenemos un objeto f de tipo para todos forall T. T -> T Lo que podemos hacer con este objeto es primero pasarle un tipo Q escribiendo f<Q> . Luego recuperamos un valor con el tipo Q -> Q Sin embargo, ciertas f no son válidas. Por ejemplo este f :

f<int> = (x => x+1)
f<T> = (x => x)

Entonces, si "llamamos" f<int> , recuperamos un valor con el tipo int -> int , y en general, si "llamamos" f<Q> , recuperamos un valor con el tipo Q -> Q , entonces eso es bueno. Sin embargo, generalmente se entiende que esta f no es una cosa válida de tipo para todos forall T. T -> T , porque hace algo diferente dependiendo de qué tipo de pase. La idea de forall es que esto no está permitido explícitamente. Además, si forall es lambda para el nivel de tipo, ¿entonces qué existe? (es decir, cuantificación existencial). Por estas razones, parece que para todos y para todos no existen realmente "lambda en el nivel de tipo". Pero entonces, ¿qué son? Me doy cuenta de que esta pregunta es bastante vaga, pero ¿puede alguien aclararme esto?

Una posible explicación es la siguiente:

Si observamos la lógica, los cuantificadores y lambda son dos cosas diferentes. Un ejemplo de una expresión cuantificada es:

forall n in Integers: P(n)

Así que hay dos partes para forall: un conjunto para cuantificar sobre (por ejemplo, enteros) y un predicado (por ejemplo, P). Forall puede verse como una función de orden superior:

forall n in Integers: P(n) == forall(Integers,P)

Con el tipo:

forall :: Set<T> -> (T -> bool) -> bool

Exists tiene el mismo tipo. Forall es como una conjunción infinita, donde S [n] es el n-ésimo elemento del conjunto S:

forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...

Existe como una disyunción infinita:

exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...

Si hacemos una analogía con los tipos, podríamos decir que el tipo analógico de ∧ está calculando el tipo de intersección ∩, y el tipo analógico de ∨ que calcula el tipo de unión. Entonces podríamos definir forall y existe en tipos de la siguiente manera:

forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ...
exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...

Entonces, para todos es una intersección infinita, y existe una unión infinita. Sus tipos serían:

forall, exists :: Set<T> -> (T -> Type) -> Type

Por ejemplo el tipo de la función de identidad polimórfica. Aquí, Types es el conjunto de todos los tipos, y -> es el constructor de tipos para las funciones y => es la abstracción lambda:

forall(Types, t => (t -> t))

Ahora una cosa de tipo para todo forall T:Type. T -> T forall T:Type. T -> T es un valor , no una función de tipos a valores. Es un valor cuyo tipo es la intersección de todos los tipos T -> T donde T abarca todos los tipos. Cuando usamos dicho valor, no tenemos que aplicarlo a un tipo. En su lugar, utilizamos un juicio de subtipo:

id :: forall T:Type. T -> T
id = (x => x)

id2 = id :: int -> int

Este downcasts id para tener el tipo int -> int . Esto es válido porque int -> int también aparece en la intersección infinita.

Creo que esto funciona muy bien y explica claramente qué es todo y en qué se diferencia de lambda, pero este modelo es incompatible con lo que he visto en lenguajes como ML, F #, C #, etc. Por ejemplo, en F # you do id<int> para obtener la función de identidad en ints, lo que no tiene sentido en este modelo: id es una función en valores, no una función en tipos que devuelve una función en valores.

¿Puede alguien con conocimiento de la teoría de tipos explicar qué son exactamente para todos y existe? ¿Y hasta qué punto es cierto que "forall is lambda a nivel de tipo"?

Answer 1

si forall es lambda ... entonces lo que existe

¿Por qué, tuple por supuesto!

En la teoría de tipos de Martin-Löf, usted tiene tipos Π, correspondientes a funciones / cuantificación universal y tipos Σ, correspondientes a tuplas / cuantificación existencial.

Sus tipos son muy similares a los que usted propuso (estoy usando la notación Agda aquí):

Π : (A : Set) -> (A -> Set) -> Set
Σ : (A : Set) -> (A -> Set) -> Set

De hecho, Π es un producto infinito y Σ es suma infinita. Sin embargo, tenga en cuenta que no son "intersección" y "unión", como propuso, ya que no puede hacer eso sin definir además dónde se intersecan los tipos. (qué valores de un tipo corresponden a qué valores del otro tipo)

De estos dos constructores de tipo, puede tener todas las funciones normales, polimórficas y dependientes, las tuplas normales y dependientes, así como las declaraciones cuantificadas existencial y universalmente:

-- Normal function, corresponding to "Integer -> Integer" in Haskell
factorial : Π ℕ (λ _ → ℕ)

-- Polymorphic function corresponding to "forall a . a -> a"
id : Π Set (λ A -> Π A (λ _ → A))

-- A universally-quantified logical statement: all natural numbers n are equal to themselves
refl : Π ℕ (λ n → n ≡ n)


-- (Integer, Integer)
twoNats : Σ ℕ (λ _ → ℕ)

-- exists a. Show a => a
someShowable : Σ Set (λ A → Σ A (λ _ → Showable A))

-- There are prime numbers
aPrime : Σ ℕ IsPrime

Sin embargo, esto no aborda la parametricidad en absoluto y la parametricidad de AFAIK y la teoría de tipos de Martin-Löf son independientes.

Por parametricidad, la gente usualmente se refiere al trabajo de Philip Wadler .

Answer 2

Algunas observaciones para complementar las dos respuestas ya excelentes.

Primero, no se puede decir que forall es lambda en el nivel de tipo porque ya existe una noción de lambda en el nivel de tipo, y es diferente de forall . Aparece en el sistema F_omega, una extensión del Sistema F con cómputo a nivel de tipo, que es útil para explicar los sistemas de módulos ML por ejemplo ( módulos F-ing , de Andreas Rossberg, Claudio Russo y Derek Dreyer, 2010).

En (una sintaxis para) Sistema F_omega puede escribir, por ejemplo:

type prod =
  lambda (a : *). lambda (b : *).
    forall (c : *). (a -> b -> c) -> c

Esta es una definición del "constructor de tipo" prod , como prod ab es el tipo de codificación de la iglesia del tipo de producto (a, b) . Si hay un cálculo a nivel de tipo, entonces necesita controlarlo si quiere asegurar la terminación de la verificación de tipo (de lo contrario, podría definir el tipo (lambda t. tt) (lambda t. tt) . Esto se hace usando un "sistema de tipos en el nivel de tipos", o un sistema de tipo . prod sería de tipo * -> * -> * . Solo los tipos en tipo * pueden estar habitados por valores, los tipos en clase superior solo pueden aplicarse en el nivel de tipo. lambda (c : k) . .... es una abstracción de nivel de tipo que no puede ser el tipo de un valor y puede vivir en cualquier tipo de la forma k -> ... , mientras que para todos forall (c : k) . .... clasificar los valores que son polimórficos en algunos tipos c : k y son necesariamente de tipo suelo * .

En segundo lugar, hay una diferencia importante entre el sistema F y los tipos Pi de la teoría de tipos de Martin-Löf. En el Sistema F, los valores polimórficos hacen lo mismo en todos los tipos . Como primera aproximación, podría decir que un valor de tipo para todos forall a . a -> a forall a . a -> a (implícitamente) tomará un tipo t como entrada y devolverá un valor de tipo t -> t . Pero eso sugiere que puede haber algún cálculo en el proceso, lo cual no es el caso. Moralmente, cuando creas un valor de tipo para todos forall a. a -> a forall a. a -> a en un valor de tipo t -> t , el valor no cambia. Hay tres maneras (relacionadas) de pensar en ello:

• La cuantificación del sistema F tiene borrado de tipo, puede olvidarse de los tipos y aún sabrá qué es la semántica dinámica del programa. Cuando utilizamos la inferencia de tipo ML para dejar la abstracción y la creación de instancias de polimorfismo implícitas en nuestros programas, realmente no permitimos que el motor de inferencia "llene los orificios en nuestro programa", si piensa en "programa" como el objeto dinámico que se ejecutará y computar.

• Un forall a . foo forall a . foo no es algo que "produce una instancia de foo para cada tipo a , sino un tipo foo que es" genérico en un tipo desconocido a ".

• Puede explicar la cuantificación universal como una conjunción infinita, pero existe una condición de uniformidad de que todos los conjuntos tienen la misma estructura y, en particular, que sus pruebas son todas iguales.

Por el contrario, los tipos pi en la teoría de tipos de Martin-Löf son en realidad más bien tipos de funciones que toman algo y devuelven algo. Esa es una de las razones por las que se pueden usar fácilmente no solo para depender de los tipos , sino también para depender de los términos (tipos dependientes).

Esto tiene implicaciones muy importantes una vez que te preocupa la solidez de esas teorías formales. El sistema F es imprevisivo (un tipo cuantificado para todos cuantifica en todos los tipos, incluido él mismo), y la razón por la que todavía es sólido es esta uniformidad de cuantificación universal. Si bien la introducción de construcciones no paramétricas es razonable desde el punto de vista de un programador (y todavía podemos razonar sobre la parametricidad en un lenguaje generalmente no paramétrico), destruye muy rápidamente la consistencia lógica del sistema de razonamiento estático subyacente. La teoría predicativa de Martin-Löf es mucho más sencilla de demostrar correcta y de extender de manera correcta.

Para una descripción de alto nivel de este aspecto de uniformidad / genérico del Sistema F, vea el artículo 97 de Fruchart y Longo sobre las observaciones de Carnap sobre las definiciones impredicativas y el teorema de la genericidad . Para un estudio más técnico de la falla del Sistema F en presencia de construcciones no paramétricas, vea Parametricidad y variantes del operador J de Girard por Robert Harper y John Mitchell (1999). Finalmente, para una descripción, desde el punto de vista del diseño de un lenguaje, sobre cómo abandonar la parametricidad global para introducir construcciones no paramétricas pero aún así poder discutir localmente la parametricidad, consulte Parametricidad no paramétrica por George Neis, Derek Dreyer y Andreas Rossberg, 2011.

Esta discusión de la diferencia entre "abstracción computacional" y "resumen uniforme" ha sido revivida por la gran cantidad de trabajo en la representación de carpetas variables. Una construcción vinculante se siente como una abstracción (y puede ser modelada por una lambda-abstracción en el estilo HOAS) pero tiene una estructura uniforme que lo hace más bien un esqueleto de datos que una familia de resultados. Esto se ha discutido mucho, por ejemplo, en la comunidad de LF, "flechas representativas" en Twelf, "flechas positivas" en el trabajo de Licata y Harper, etc.

Recientemente, ha habido varias personas trabajando en la noción relacionada de "irrelevancia" (lambda-abstracciones donde el resultado "no depende" del argumento), pero aún no está del todo claro en qué medida se relaciona esto con el polimorfismo paramétrico. Un ejemplo es el trabajo de Nathan Mishra-Linger con Tim Sheard (por ejemplo, Erasure y Polymorphism in Pure Type Systems ).

Answer 3

Permítanme abordar sus preguntas por separado.

• Llamar a todo "un lambda en el nivel de tipo" es incorrecto por dos razones. Primero, es el tipo de un lambda, no el lambda en sí. Segundo, la lambda vive en el nivel de término, aunque se abstrae sobre los tipos (las lambdas en el nivel de tipo también existen, proporcionan lo que a menudo se denomina tipos genéricos).

• La cuantificación universal no implica necesariamente "el mismo comportamiento" para todas las instancias. Esa es una propiedad particular llamada "parametricidad" que puede o no estar presente. El cálculo lambda polimórfico plano es paramétrico, porque simplemente no puede expresar ningún comportamiento no paramétrico. Pero si agrega construcciones como typecase (también conocido como análisis de tipo intensional) o conversiones controladas como una forma más débil de eso, perderá parametricidad. La parametrización implica buenas propiedades, por ejemplo, permite implementar un lenguaje sin ninguna representación de tipos en tiempo de ejecución. E induce principios de razonamiento muy fuertes, ver, por ejemplo, el artículo de Wadler "¡Teoremas gratis!". Pero es una compensación, a veces quieres envíos de tipos.

• Los tipos existenciales esencialmente denotan pares de un tipo (el llamado testigo) y un término, a veces llamado paquetes . Una forma común de verlos es como la implementación de tipos de datos abstractos. Aquí hay un ejemplo simple:

  paquete ( Int , (λ x . x , λ x . x )): ∃ T. ( Int → T ) × ( T → Int )

  Este es un ADT simple cuya representación es Int y que solo proporciona dos operaciones (como una tupla anidada), para convertir ints dentro y fuera del tipo abstracto T. Esta es la base de las teorías de tipos para módulos, por ejemplo.

• En resumen, la cuantificación universal proporciona la abstracción de datos del lado del cliente, mientras que los tipos existenciales proporcionan la abstracción de datos del lado del implementador.

• Como observación adicional, en el llamado cubo lambda , todo y la flecha se generalizan a la noción unificada del tipo ((donde T1 → T2 = Π (x: T1) .T2 y ∀AT = Π (A: *) .T) y de la misma manera existe y el agrupamiento puede generalizarse a los tipos Σ (donde T1 × T2 = Σ (x: T1) .T2 y ∃AT = Σ (A: *). T). Aquí, el tipo * es el "tipo de tipos".