Defina una lista utilizando solo el sistema de tipos Hindley-Milner

Estoy trabajando en un pequeño compilador de cálculo lambda que tiene un sistema de inferencia de tipo Hindley-Milner y ahora también admite recursivos Let's (no en el código vinculado), que entiendo que debería ser suficiente para completar Turing .

El problema ahora es que no tengo idea de cómo hacer que sea compatible con listas, o si ya las admite y solo necesito encontrar una manera de codificarlas. Me gustaría poder definirlos sin tener que agregar nuevas reglas al sistema de tipos.

La forma más fácil en que puedo pensar en una lista xes como algo que es null(o la lista vacía), o un par que contiene tanto una xcomo una lista de x. Pero para hacer esto necesito poder definir pares y o, que creo que son el producto y los tipos de suma.

Parece que puedo definir pares de esta manera:

pair = λabf.fab
first = λp.p(λab.a)
second = λp.p(λab.b)

Dado pairque tendría el tipo a -> (b -> ((a -> (b -> x)) -> x)), después de pasar, digamos, an inty a string, produciría algo con tipo (int -> (string -> x)) -> x, que sería la representación de un par de inty string. Lo que me molesta aquí es que si eso representa un par, ¿por qué eso no es lógicamente equivalente a, ni implica la proposición int and string? Sin embargo, es equivalente a (((int and string) -> x) -> x), como si solo pudiera tener tipos de productos como parámetros para las funciones. Esta respuestaparece abordar este problema, pero no tengo idea de qué significan los símbolos que usa. Además, si esto realmente no codifica un tipo de producto, ¿hay algo que pueda hacer con los tipos de productos que no podría hacer con mi definición de pares anterior (considerando que también puedo definir n-tuplas de la misma manera)? Si no, ¿no contradiría esto el hecho de que no puede expresar la conjunción (AFAIK) usando solo implicación?

Además, ¿qué tal el tipo de suma? ¿Puedo codificarlo de alguna manera usando solo el tipo de función? Si es así, ¿sería esto suficiente para definir listas? O bien, ¿hay alguna otra forma de definir listas sin tener que extender mi sistema de tipos? Y si no, ¿qué cambios necesitaría hacer si quiero que sea lo más simple posible?

Tenga en cuenta que soy un programador de computadoras pero no un científico de la computación ni un matemático y soy bastante malo leyendo la notación matemática.

Editar: no estoy seguro de cuál es el nombre técnico de lo que he implementado hasta ahora, pero todo lo que tengo es básicamente el código que he vinculado anteriormente, que es un algoritmo de generación de restricciones que usa las reglas para aplicaciones, abstracciones y variables tomadas del algoritmo Hinley-Milner y luego un algoritmo de unificación que obtiene el tipo principal. Por ejemplo, la expresión \a.aarrojará el tipo a -> ay \a.(a a)arrojará un error de verificación de ocurrencia. Además de esto, no existe exactamente una letregla, sino una función que parece tener el mismo efecto que le permite definir funciones globales recursivas como este pseudocódigo:

GetTypeOfGlobalFunction(term, globalScope, nameOfFunction)
{
    // Here 'globalScope' contains a list of name-value pair where every value is of class 'ClosedType', 
    // meaning their type will be cloned before unified in the unification algorithm so that they can be used polymorphically 
    tempType = new TypeVariable() // Assign a dummy type to `tempType`, say, type 'x'.
    // The next line creates an scope with everything in 'globalScope' plus the 'nameOfFunction = tempType' name-value pair
    tempScope = new Scope(globalScope, nameOfFunction, tempType) 
    type = TypeOfTerm(term, tempScope) // Calculate the type of the term 
    Unify(tempType, type)
    return type
    // After returning, the code outside will create a 'ClosedType' using the returned type and add it to the global scope.
}

Básicamente, el código obtiene el tipo del término como de costumbre, pero antes de unificar, agrega el nombre de la función que se define con un tipo ficticio en el ámbito de tipo para que pueda usarse desde dentro de sí mismo de forma recursiva.

Edición 2: Acabo de darme cuenta de que también necesitaría tipos recursivos, que no tengo, para definir una lista como quiero.

lambda-calculus type-theory type-inference Juan
fuente

¿Puedes ser un poco más específico sobre lo que has implementado exactamente? ¿Ha implementado el cálculo lambda de tipo simple (con definiciones recursivas) y le dio polimorfismos paramétricos al estilo Hindley-Milner? ¿O ha implementado el cálculo lambda polimórfico de segundo orden?

Andrej Bauer

Tal vez pueda preguntar de una manera más fácil: si tomo OCaml o SML y lo restringe a términos lambda puros y definiciones recursivas, ¿es eso de lo que estás hablando?

Andrej Bauer

@AndrejBauer: he editado la pregunta. No estoy seguro acerca de OCaml y SML, pero estoy bastante seguro de que si toma Haskell y lo restringe a términos lambda y permisos recursivos de alto nivel (como let func = \x -> (func x)) obtendrá lo que tengo.

Juan

Para mejorar su pregunta, consulte esta meta publicación .

Juho

Respuestas:

Pares

Esta codificación es la codificación de pares de la Iglesia . Técnicas similares pueden codificar booleanos, enteros, listas y otras estructuras de datos.

Bajo el contexto x:a; y:b, el término pair x ytiene el tipo (a -> b -> t) -> t. La interpretación lógica de este tipo es la siguiente fórmula (uso anotaciones matemáticas estándar: es implicación, es o, es y, es negación; es equivalencia de fórmulas): ¿Por qué “ y o ”? Intuitivamente, porque $\to$ $\vee$ $\wedge$ $\neg$ $\iff$

\begin{aligned} (a \to b \to t) \to t & ⟺ \neg (\neg a \lor \neg b \lor t) \lor t \\ ⟺ (a \land b \land \neg t) \lor t \\ ⟺ (a \land b) \lor t \end{aligned}

$\begin{align} (a \to b \to t) \to t & \quad\iff\quad \neg (\neg a \vee \neg b \vee t) \vee t \\ & \quad\iff\quad (a \wedge b \wedge \neg t) \vee t \\ & \quad\iff\quad (a \wedge b) \vee t \\ \end{align}$ ab tpaires una función que toma una función como argumento y la aplica al par. Hay dos maneras en que esto puede ir: la función de argumento puede hacer uso del par, o puede producir un valor de tipo tsin usar el par en absoluto.

paires un constructor para el tipo de par firsty secondson destructores. (Estas son las mismas palabras que se usan en la programación orientada a objetos; aquí las palabras tienen un significado que está relacionado con la interpretación lógica de los tipos y términos que no entraré aquí.) Intuitivamente, los destructores le permiten acceder a lo que está en el objeto y los constructores allanan el camino para el destructor tomando como argumento una función que aplican a las partes del objeto. Este principio se puede aplicar a otros tipos.

Sumas

La codificación de la Iglesia de una unión discriminada es esencialmente dual a la codificación de la Iglesia de un par. Cuando un par tiene dos partes que se deben juntar y puede optar por extraer una u otra, puede optar por construir la unión de cualquiera de las dos maneras y cuando la usa, debe permitir ambas. Por lo tanto, hay dos constructores, y hay un solo destructor que toma dos argumentos.

let case w = λf. λg. w f g           case : ((a->t) -> (b->t) -> t) -> (a->t) -> (b->t) -> t
  (* or simply let case w = w *)
let left x = λf. λg. f x             left : a -> ((a->t) -> (b->t) -> t)
let right y = λf. λg. g x            right : b -> ((a->t) -> (b->t) -> t)

Permítanme abreviar el tipo (a->t) -> (b->t) -> tcomo SUM(a,b)(t). Entonces los tipos de destructores y constructores son:

case : SUM(a,b)(t) -> (a->t) -> (b->t) -> t
left : a -> SUM(a,b)(t)
right : b -> SUM(a,b)(t)

Así

case (left x) f g → f x
case (rightt y) f g → g y

Liza

Para una lista, aplique nuevamente el mismo principio. Una lista cuyos elementos tienen el tipo ase puede construir de dos maneras: puede ser una lista vacía, o puede ser un elemento (el encabezado) más una lista (la cola). En comparación con los pares, hay un pequeño giro en lo que respecta a los destructores: no puede tener dos destructores separados heady tailporque solo funcionarían en listas no vacías. Necesita un solo destructor, con dos argumentos, uno de los cuales es una función de argumento 0 (es decir, un valor) para el caso nulo, y el otro una función de 2 argumentos para el caso contras. Funciones como is_empty, heady tailse pueden derivar de eso. Como en el caso de las sumas, la lista es directamente su propia función destructora.

let nil = λn. λc. n
let cons h t = λn. λc. c h t
let is_empty l = l true (λh. λt. false) 
let head l default = l default (λh. λt. h)
let tail l default = l default (λh. λt. t)

Cada una de estas funciones es polimórfica. Si trabaja los tipos de estas funciones, notará que consno es uniforme: el tipo del resultado no es el mismo que el tipo del argumento. El tipo de resultado es una variable; es más general que el argumento. Si encadena consllamadas, las llamadas sucesivas para crear una lista se instancian consen diferentes tipos. Esto es crucial para que las listas funcionen en ausencia de tipos recursivos. Puede hacer listas heterogéneas de esa manera. De hecho, los tipos que puede expresar no son "lista de ", sino "lista cuyos primeros elementos son de los tipos ". $T$ $T_1,\ldots,T_n$

Como supones, si quieres definir un tipo que solo contenga listas homogéneas, necesitas tipos recursivos. ¿Por qué? Veamos el tipo de una lista. Una lista se codifica como una función que toma dos argumentos: el valor para devolver en listas vacías y la función para calcular el valor para devolver en una celda de contras. Sea ael tipo de elemento, bel tipo de la lista y cel tipo devuelto por el destructor. El tipo de una lista es

a -> (a -> b -> c) -> c

Hacer la lista homogénea es decir que si se trata de una celda de contras, la cola debe tener el mismo tipo que el conjunto, es decir, agrega la restricción

a -> (a -> b -> c) -> c = b

El sistema de tipos Hindley-Milner puede ampliarse con tales tipos recursivos, y de hecho los lenguajes de programación prácticos lo hacen. Los lenguajes de programación prácticos tienden a rechazar tales ecuaciones "desnudas" y requieren un constructor de datos, pero este no es un requisito intrínseco de la teoría subyacente. Requerir un constructor de datos simplifica la inferencia de tipos, y en la práctica tiende a evitar aceptar funciones que en realidad son defectuosas pero que pueden ser tipables con alguna restricción involuntaria que causa un error de tipo difícil de entender cuando se utiliza la función. Esta es la razón por la cual, por ejemplo, OCaml acepta tipos recursivos sin protección solo con la -rectypesopción de compilador no predeterminada . Aquí están las definiciones anteriores en la sintaxis OCaml, junto con una definición de tipo para listas homogéneas usando la notación paratipos recursivos con alias : type_expression as 'asignifica que el tipo type_expressionestá unificado con la variable 'a.

# let nil = fun n c -> n;;
val nil : 'a -> 'b -> 'a = <fun>
# let cons h t = fun n c -> c h t;;
val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = <fun>
# let is_empty l = l true (fun h t -> false);;
val is_empty : (bool -> ('a -> 'b -> bool) -> 'c) -> 'c = <fun>
# let head l default = l default (fun h t -> h);;
val head : ('a -> ('b -> 'c -> 'b) -> 'd) -> 'a -> 'd = <fun>
# let tail l default = l default (fun h t -> t);;
val tail : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd = <fun>
# type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c;;
type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c
# is_empty (cons 1 nil);;
- : bool = false
# head (cons 1 nil) 0;;
- : int = 1
# head (tail (cons 1 (cons 2.0 nil)) nil) 0.;;
- : float = 2.

(* -rectypes is required for what follows *)
# type ('a, 'b, 'c) rlist = 'c -> ('a -> 'b -> 'c) -> 'c as 'b;;
type ('a, 'b, 'c) rlist = 'b constraint 'b = 'c -> ('a -> 'b -> 'c) -> 'c
# let rcons = (cons : 'a -> ('a, 'b, 'c) rlist -> ('a, 'b, 'c) rlist);;
val rcons :
  'a ->
  ('a, 'c -> ('a -> 'b -> 'c) -> 'c as 'b, 'c) rlist -> ('a, 'b, 'c) rlist =
  <fun>
# head (rcons 1 (rcons 2 nil)) 0;;
- : int = 1
# tail (rcons 1 (rcons 2 nil)) nil;;
- : 'a -> (int -> 'a -> 'a) -> 'a as 'a = <fun>
# rcons 1 (rcons 2.0 nil);;
Error: This expression has type
         (float, 'b -> (float -> 'a -> 'b) -> 'b as 'a, 'b) rlist = 'a
       but an expression was expected of type
         (int, 'b -> (int -> 'c -> 'b) -> 'b as 'c, 'b) rlist = 'c

Pliegues

Mirando esto un poco más en general, ¿cuál es la función que representa la estructura de datos?

Para un número natural: se representa como la función que itera su argumento veces. $n$ $n$
Para un par: se representa como una función que aplica su argumento a e . $(x,y)$ $x$ $y$
Para una suma: se representa como una función que aplica su ésimo argumento a . $\mathrm{in}_i(x)$ $i$ $x$
Para una lista: se representa como una función que toma dos argumentos, el valor que se devuelve para la lista vacía y la función que se aplica a las celdas cons. $[x_1,\ldots,x_n]$

En términos generales, la estructura de datos se representa como su función de plegado . Este es un concepto general para las estructuras de datos: una función de plegado es una función de orden superior que atraviesa la estructura de datos. Hay un sentido técnico en el que fold es universal : todos los recorridos de la estructura de datos "genéricos" se pueden expresar en términos de fold. Que la estructura de datos se pueda representar como su función de pliegue muestra esto: todo lo que necesita saber sobre una estructura de datos es cómo atravesarla, el resto es un detalle de implementación.

Gilles 'SO- deja de ser malvado'
fuente

Usted menciona la " codificación de la Iglesia " de enteros, pares, sumas, pero para las listas le da la codificación de Scott . Creo que puede ser un poco confuso para aquellos que no están familiarizados con las codificaciones de tipos inductivos.

Stéphane Gimenez

Básicamente, mi tipo de par no es realmente un tipo de producto, ya que una función con este tipo podría regresar te ignorar el argumento que se supone que debe tomar ay b(que es exactamente lo (a and b) or tque dice). Y parece que tendría el mismo tipo de problemas con las sumas. Y también, sin tipos recursivos no tendré una lista homogénea. En pocas palabras, ¿estás diciendo que debería agregar reglas de suma, producto y tipo recursivo para obtener listas homogéneas?

Juan

¿Querías decir case (right y) f g → g yal final de tu sección de Sumas ?

Juan

@ StéphaneGimenez no me había dado cuenta. No estoy acostumbrado a trabajar en estas codificaciones en un mundo escrito. ¿Puedes dar una referencia para la codificación de la Iglesia frente a la codificación de Scott?

Gilles 'SO- deja de ser malvado'

@JuanLuisSoldi Probablemente haya escuchado que "no hay ningún problema que no pueda resolverse con un nivel adicional de indirección". Las codificaciones de la iglesia codifican las estructuras de datos como funciones agregando un nivel de llamada a la función: una estructura de datos se convierte en una función de segundo orden que se aplica a la función para actuar sobre las partes. Si desea un tipo de lista homogénea, tendrá que lidiar con el hecho de que el tipo de la cola es el mismo que el de toda la lista. Creo que esto tiene que implicar una forma de recursión tipo.

Gilles 'SO- deja de ser malvado'

Puede representar tipos de suma como tipos de productos con etiquetas y valores. En este caso, podemos hacer trampa un poco y usar una etiqueta para representar nulo o no, teniendo la segunda etiqueta representando el par cabeza / cola.

Definimos booleanos de la manera habitual:

true = λi.λe.i
false = λi.λe.e
if = λcond.λthen.λelse.(cond then else)

Una lista es entonces un par con el primer elemento como un booleano, y el segundo elemento como un par de cabeza / cola. Algunas funciones básicas de la lista:

isNull = λl.(first l)
null = pair false false     --The second element doesn't matter in this case
cons = λh.λt.(pair true (pair h t ))
head = λl.(fst (snd l))   --This is a partial function
tail = λl.(snd (snd l))   --This is a partial function  

map = λf.λl.(if (isNull l)
                 null 
                 (cons (f (head l)) (map f (tail l) ) )

jmite
fuente

Pero esto no me daría una lista homogénea, ¿es correcto?

Juan