Funciones de ML desde listas polimórficas a listas polimórficas

8

Estoy aprendiendo programación en ML (OCaml), y antes pregunté sobre las funciones de tipo ML'a -> 'b . Ahora he estado experimentando un poco con funciones de tipo 'a list -> 'b list. Hay algunos ejemplos simples obvios:

let rec loop l = loop l
let return_empty l = []
let rec loop_if_not_empty = function [] -> []
                                   | l -> loop_if_not_empty l

Lo que no puedo entender es cómo hacer una función que haga algo más que devolver la lista vacía o el bucle (sin usar ninguna función de biblioteca). Se puede hacer esto? ¿Hay alguna manera de devolver listas no vacías?

Editar: Sí, si tengo una función de tipo 'a -> 'b, entonces puedo hacer otra, o una función de tipo 'a list -> 'b list, pero lo que me pregunto aquí es cómo hacer la primera.

programming-languages typing functional-programming Gilles 'SO- deja de ser malvado'
fuente

1

Al igual que con la pregunta anterior, dirija la programación de aprendizaje del estudiante CS101 en su respuesta, no el tipo teórico en el que su respuesta podría inspirarlo para que se convierta más tarde.

Gilles 'SO- deja de ser malvado'

Tenga en cuenta que si tuviera una función f con este tipo que devuelve una lista no vacía, entonces divertido a -> List.hd (f [a]) tendría el tipo 'a ->' b sin ser sin terminación ni generar una excepción.

gallais

6

Bueno, algo conocido como parametricidad nos dice que si consideramos el subconjunto puro de ML (es decir, sin recursión infinita refy todas esas cosas raras), no hay forma de definir una función con este tipo que no sea la que devuelve el vacío lista.

Todo esto comenzó con el artículo de Wadler "¡ Teoremas gratis! ". Este artículo, básicamente, nos dice dos cosas:

Si consideramos lenguajes de programación que satisfacen ciertas condiciones, podemos deducir algunos teoremas geniales simplemente mirando la firma de tipo de una función polimórfica (esto se llama Teorema de Parametricidad).
ML (sin recursión infinita refy todas esas cosas raras) satisface esas condiciones.

Desde el teorema Parametricity sabemos que si tenemos una función f : 'a list -> 'b list, a continuación, para todos 'a, 'b, 'c, 'dy para todas las funciones g : 'a -> 'c, h : 'b -> 'dtenemos:

map h ∘ f = f ∘ map g

(Nota, fa la izquierda tiene tipo 'a list -> 'b listy fa la derecha es 'c list -> 'd list).

Somos libres de elegir lo gque queramos, así que deja 'a = 'cy g = id. Ahora desde map id = id(fácil de probar por inducción en la definición de map), tenemos:

map h ∘ f = f

Ahora deja 'b = 'd = booly h = not. Asumamos que para algunos zs : bool listsucede eso f zs ≠ [] : bool list. Está claro que map not ∘ f = fno se sostiene, porque

(map not ∘ f) zs ≠ f zs

Si el primer elemento de la lista de la derecha es true, entonces, a la izquierda, el primer elemento es falsey viceversa.

Esto significa que nuestra suposición es incorrecta y f zs = []. ¿Terminamos? No.

Asumimos que 'bes bool. Hemos demostrado que cuando fse invoca con type f : 'a list -> bool listpara any 'a, fsiempre debe devolver la lista vacía. ¿Puede ser que cuando llamamos fya f : 'a list -> unit listque devuelve algo diferente? Nuestra intuición nos dice que esto no tiene sentido: simplemente no podemos escribir en ML pura una función que siempre devuelve la lista vacía cuando queremos que nos dé una lista de booleanos y de lo contrario podría devolver una lista no vacía. Pero esto no es una prueba.

Lo que queremos decir es que fes uniforme : si siempre devuelve la lista vacía para bool list, entonces tiene que devolver la lista vacía para unit listy, en general, cualquier 'a list. Esto es exactamente de lo que trata el segundo punto en la lista de viñetas al comienzo de mi respuesta.

El artículo nos dice que en ML fdebe tomar valores relacionados con valores relacionados . No voy a entrar en detalles sobre las relaciones, es suficiente decir que las listas están relacionadas si y solo si tienen la misma longitud y sus elementos están relacionados por pares (es decir, [x_1, x_2, ..., x_m]y [y_1, y_2, ..., y_n]están relacionados si y solo si m = ny x_1están relacionados con y_1y x_2está relacionado con y_2y así sucesivamente). Y la parte divertida es, en nuestro caso, dado que fes polimórfico, ¡ podemos definir cualquier relación en los elementos de las listas!

Vamos a recoger cualquier 'a, 'by miran f : 'a list -> 'b list. Ahora mira f : 'a list -> bool list; Ya hemos demostrado que en este caso fsiempre devuelve la lista vacía. Ahora postulamos que todos los elementos de 'aestán relacionados entre sí (recuerde, podemos elegir cualquier relación que queramos), esto implica que cualquiera zs : 'a listestá relacionado con sí mismo. Como sabemos, ftoma valores relacionados con valores relacionados, esto significa que f zs : 'b listestá relacionado con f zs : bool list, pero la segunda lista tiene una longitud igual a cero, y dado que la primera está relacionada con ella, también está vacía.

Para completar, mencionaré que hay una sección sobre el impacto de la recursividad general (posible no terminación) en el documento original de Wadler, y también hay un documento que explora teoremas libres en presencia de seq.

kirelagin
fuente

Ahora sospecho que la prueba se puede realizar en un solo paso si en lugar de debilitar el teorema parametricity considerando las relaciones específicas inducidas por funciones ( gy hen este caso) ir directamente con las relaciones generales a medida ...

kirelagin

Nitpick, la parametricidad no comienza con el artículo de Wadler (que afirma ser un resumen de los enfoques para definir la parametricidad). La idea se remonta al artículo de Reynold "Tipos, abstracción y polimorfismo paramétrico". La idea también estuvo un poco presente en la prueba de normalización de Girard para el Sistema F, que yo sepa.

Daniel Gratzer

4

Volvamos a los objetos más simples: no puede construir un objeto de tipo adecuado 'aporque entonces significaría que este objeto xse puede usar donde sea 'aque encaje. Y eso significa en todas partes: como un entero, una matriz, incluso una función. Por ejemplo, eso significaría que puede hacer cosas como x+2, x.(1)y (x 5). Los tipos existen exactamente para evitar esto.

Esta es la misma idea que se aplica con una función de tipo 'a -> 'b, pero hay algunos casos en los que este tipo puede existir: cuando la función nunca devuelve un objeto de tipo 'b: cuando se repite o se genera una excepción.

Esto también se aplica a las funciones que devuelven una lista. Si su función es de tipo t -> 'b listy crea un objeto de tipo ty lo aplica a esta función, eso significa que si accede con éxito a un elemento de esta lista, accederá a un objeto que tenga todos los tipos. Por lo tanto, no puede acceder a ningún elemento de la lista: la lista está vacía o ... no hay lista.

Sin embargo, el tipo 'a list -> 'b listaparece en los ejercicios habituales, pero eso es solo cuando ya tiene una función de tipo 'a -> 'b:

let rec map (f : 'a -> 'b) =
  function
  | [] -> []
  | x :: xs -> f x :: map f xs

Pero probablemente conozcas este.

val map : ('a -> 'b) -> 'a list -> 'b list

jmad
fuente

1

El teórico del tipo anterior está menos que encantado con esta respuesta. Ok, un contexto de variable de tipo no vacío es una forma de tener una función que es literalmente de tipo 'a -> 'bo 'a list -> 'b list, pero esa no es una observación tan interesante. De hecho, voy a editar la pregunta para dejar en claro que esto no es de lo que se preguntaba la programación de aprendizaje para estudiantes más jóvenes.

Gilles 'SO- deja de ser malvado'

Pero el teórico de tipo más antiguo sabe que ML no tiene fallas lógicas. Si se puede producir una función f : 'a list -> 'b listy ttal que f t <> []entonces este programa escribirá-cheque, pero puede hacer camino peor que lanzar una excepción: let y = List.hd (f t) in (y y) (y + y.(0) + y.(0).(0)).

jmad

2

Teorema de parametricidad de los "Teoremas gratis!" El artículo nos dice que los términos de ML tienen una propiedad muy especial: si vemos el tipo de un término como una relación con los valores de este tipo, entonces el valor de este término estará relacionado con sí mismo. Aquí se explica cómo ver los tipos como relaciones:

Un tipo de función 'a -> 'bcorresponde a la relación definida al decir que dos funciones están relacionadas si toman valores relacionados con valores relacionados (asumiendo 'ay 'bcorresponden a algunas relaciones).
Un tipo de lista 'a listcorresponde a la relación definida al decir que dos listas están relacionadas si tienen la misma longitud y sus elementos coincidentes están relacionados (suponiendo que 'acorresponda a alguna relación).
(Ahora la parte más interesante.) De tipo A polimórficos corresponde a la relación definida por decir que dos valores polimórficas están relacionadas si podemos elegir cualquier dos tipos, cualquier relación entre los elementos de este tipo, reemplazar todas las instancias de la variable tipo con esta relación, y los valores resultantes seguirán estando relacionados.

Aquí hay un ejemplo. Supongamos que tenemos un término foo : 'a -> 'a. El teorema de la parametricidad dice que fooestá relacionado con sí mismo. Lo que esto significa es que podemos elegir dos tipos, digamos, $A_1$ y $A_2$ , elige absolutamente cualquier relación $\mathbf{A}$ entre elementos de este tipo, y si tomamos alguno $a_1 : A_1$ y $a_2 : A_2$ , de modo que estén relacionados de acuerdo con $\mathbf{A}$ , entonces $\operatorname{foo} a_1$ y $\operatorname{foo} a_2$ también estará relacionado de acuerdo a $\mathbf{A}$ :

{una}_{1} \sim_{UNA} {una}_{2} \Rightarrow foo {una}_{1} \sim_{UNA} foo {una}_{2} .

$a_1 \sim_\mathbf{A} a_2 \Rightarrow \operatorname{foo} a_1 \sim_\mathbf{A} \operatorname{foo} a_2.$

Ahora si tomamos la relación $\mathbf{A}$ no ser una relación arbitraria, sino una función $f : A_1 \to A_2$ , lo anterior se convierte en:

F ({una}_{1}) = {una}_{2} \Rightarrow F (foo {una}_{1}) = foo {una}_{2},

$f(a_1) = a_2 \Rightarrow f(\operatorname{foo} a_1) = \operatorname{foo} a_2,$

o, en otras palabras:

F (foo {una}_{1}) = foo (F ({una}_{1})),

$f(\operatorname{foo} a_1) = \operatorname{foo} (f(a_1)),$

que es exactamente el teorema libre para la idfunción: f . id = id . f.

Si realiza pasos similares para su función foo : 'a list -> 'b list, obtendrá que puede elegir dos tipos $A_1$ y $A_2$ , cualquier relación $\mathbf{A}$ entre sus elementos, cualesquiera dos tipos $B_1$ y $B_2$ , cualquier relación $\mathbf{B}$ entre sus elementos, luego tome dos listas, primero hechas de elementos de $A_1$ , segundo hecho de elementos de $A_2$ , aplique su función a ambas listas (obtener una lista de $B_1$ en el primer caso y una lista de $B_2$ en el segundo), y los resultados estarán relacionados, si las entradas estaban relacionadas.

Ahora usamos esto para probar que para cualquiera de los dos tipos Ay Bla función foodevuelve una lista vacía para cualquier entrada as : A list.

Dejar $A_1 = A_2 =$ A y deja $\mathbf{A}$ ser la relación de identidad, por lo tanto, cualquier lista de $A$ está trivialmente relacionado consigo mismo.
Dejar $B_1 =$ Ø, $B_2 =$ B y $\mathbf{B}$ cualquier relación entre ellos (solo hay uno, el vacío, pero no importa).
asestá relacionado con sí mismo (como elegimos la relación de identidad A), por lo tanto foo as : Ø listestá relacionado con foo as : B list.
Sabemos que dos listas pueden relacionarse solo si sus longitudes son iguales y también sabemos que la primera de las listas resultantes debe estar vacía, ya que no puede haber elementos del Øtipo.

Por lo tanto, para cualquiera A, By as : A listtenemos que foo as : B listtiene que ser una lista vacía.

kirelagin
fuente

Funciones de ML desde listas polimórficas a listas polimórficas

Respuestas: