pattern - Dada una firma de tipo Haskell, ¿es posible generar el código automáticamente?

listas infinitas haskell

Question

Lo que dice en el título. Si escribo una firma de tipo, ¿es posible generar algorítmicamente una expresión que tenga esa firma de tipo?

Parece plausible que sea posible hacer esto. Ya sabemos que si el tipo es un caso especial de firma de tipo de función de biblioteca, Hoogle puede encontrar esa función de forma algorítmica. Por otro lado, muchos problemas simples relacionados con las expresiones generales son en realidad irresolubles (p. Ej., Es imposible saber si dos funciones hacen lo mismo), por lo que no es inverosímil que este sea uno de ellos.

Probablemente sea una mala forma hacer varias preguntas al mismo tiempo, pero me gustaría saber:

• Se puede hacer?

• ¿Si es así, cómo?

• Si no, ¿hay alguna situación restringida donde sea posible?

• Es muy posible que dos expresiones distintas tengan la misma firma de tipo. ¿Puedes calcularlos a todos ? O incluso algunos de ellos?

• ¿Alguien tiene código de trabajo que hace esto de verdad?

Answer 1

Esto es imposible en general (y para lenguajes como Haskell que ni siquiera tiene la fuerte propiedad de normalización), y solo es posible en algunos (muy) casos especiales (y para lenguajes más restringidos), como cuando un tipo de dominio tiene el único constructor (por ejemplo, una función f :: forall a. a -> () se puede determinar de forma única). Para reducir un conjunto de posibles definiciones para una firma determinada a un conjunto único con una sola definición, es necesario dar más restricciones (en forma de propiedades adicionales, por ejemplo, todavía es difícil imaginar cómo puede ser útil sin dar un ejemplo de uso).

Desde el punto de vista categórico (n-), los tipos corresponden a objetos, los términos corresponden a flechas (los constructores también corresponden a flechas), y las definiciones de funciones corresponden a 2 flechas. La pregunta es análoga a la pregunta de si se puede construir una categoría 2 con las propiedades requeridas especificando solo un conjunto de objetos. Es imposible ya que necesita una construcción explícita para flechas y 2 flechas (es decir, escribir términos y definiciones), o sistema deductivo que permite deducir la estructura necesaria usando un cierto conjunto de propiedades (que aún deben definirse explícitamente).

También hay una pregunta interesante: dado un ADT (es decir, subcategoría de Hask) es posible derivar automáticamente instancias para Typeable, Data (sí, utilizando SYB ), Traversable, Plegable, Functor, Pointed, Applicative, Monad, etc. ) En este caso, tenemos las firmas necesarias, así como propiedades adicionales (por ejemplo, las leyes de mónadas, aunque estas propiedades no se pueden expresar en Haskell, pero se pueden expresar en un idioma con tipos dependientes). Hay algunas construcciones interesantes:

http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell

que muestra lo que se puede hacer para la lista ADT.

Answer 2

La pregunta es realmente bastante profunda y no estoy seguro de la respuesta, si está preguntando sobre la gloria de los tipos de Haskell, incluidas las familias de tipos, GADT, etc.

Lo que estás preguntando es si un programa puede probar automáticamente que un tipo arbitrario está habitado (contiene un valor) al exhibir tal valor. Un principio llamado la Correspondencia Curry-Howard dice que los tipos pueden interpretarse como proposiciones matemáticas, y el tipo está habitado si la proposición es demostrable de manera constructiva. Entonces pregunta si hay un programa que puede probar que cierta clase de proposiciones son teoremas. En un lenguaje como Agda, el sistema de tipos es lo suficientemente poderoso como para expresar proposiciones matemáticas arbitrarias , y probar los arbitrarios es indecidible por el teorema de incompletitud de Gödel. Por otro lado, si bajas a (digamos) Hindley-Milner puro, obtienes un sistema decidible mucho más débil y (creo). Con Haskell 98, no estoy seguro, porque se supone que las clases de tipo pueden ser equivalentes a las de GADT.

Con GADT, no sé si es decidible o no, aunque quizás algunas personas más conocedoras aquí lo sabrían de inmediato. Por ejemplo, podría ser posible codificar el problema de detención para una máquina de Turing dada como una GADT, por lo que hay un valor de ese tipo si la máquina se detiene. En ese caso, la habitabilidad es claramente indecidible. Pero tal vez tal codificación no sea posible, incluso con familias de tipos. Actualmente no soy lo suficientemente fluido en este tema para que sea obvio para mí, aunque como dije, tal vez alguien más aquí sepa la respuesta.

(Actualización :) Oh, se me ocurre una interpretación mucho más simple de su pregunta: es posible que se pregunte si cada tipo de Haskell está habitado. Obviamente, la respuesta es no. Considera el tipo polimórfico

a -> b

No hay función con esa firma (sin contar algo como inseguroCercamiento, lo que hace que el sistema de tipo sea inconsistente).

Answer 3

Oleg at okmij.org tiene una implementación de esto. Aquí hay una breve introducción here pero la fuente literaria de Haskell contiene los detalles y la descripción del proceso. (No estoy seguro de cómo esto le corresponde a Djinn en el poder, pero es otro ejemplo).

Hay casos donde no hay una función única:

fst'', snd'' :: (a, a) -> a
fst'' (a,_) = a
snd'' (_,b) = b

No solo esto; hay casos en los que hay un número infinito de funciones:

list0, list1, list2 :: [a] -> a
list0 l = l !! 0
list1 l = l !! 1
list2 l = l !! 2
-- etc.

-- Or 
mkList0, mkList1, mkList2 :: a -> [a]
mkList0 _ = []
mkList1 a = [a]
mkList2 a = [a,a]
-- etc.

(Si solo desea funciones totales, considere [a] como restringido a listas infinitas para list0 , list1 , etc., es decir data List a = Cons a (List a) )

De hecho, si tiene tipos recursivos, cualquier tipo que los involucre corresponde a un número infinito de funciones. Sin embargo, al menos en el caso anterior, hay una cantidad contable de funciones, por lo que es posible crear una lista (infinita) que contenga todas ellas. Pero, creo que el tipo [a] -> [a] corresponde a un número incontable de funciones infinitas (nuevamente restringe [a] a listas infinitas) ¡así que ni siquiera puedes enumerarlas todas!

(Resumen: hay tipos que corresponden a un número finito, contablemente infinito e incontable infinito de funciones.)

Answer 4

Djinn hace esto para un subconjunto restringido de tipos Haskell, que corresponde a una lógica de primer orden. Sin embargo, no puede administrar tipos o tipos recursivos que requieran recurrencia para implementar; entonces, por ejemplo, no puede escribir un término de tipo (a -> a) -> a (el tipo de fix ), que corresponde a la proposición "si a implica a , luego a ", que es claramente falso; puedes usarlo para probar cualquier cosa. De hecho, esta es la razón por la cual la fix da lugar a ⊥.

Si permite el fix , entonces escribir un programa para dar un término de cualquier tipo es trivial; el programa simplemente imprimiría la fix id para cada tipo.

Djinn es principalmente un juguete, pero puede hacer cosas divertidas, como derivar las instancias de Monad correctas para Reader y Cont dados los tipos de return y (>>=) . Puede probarlo instalando el paquete djinn , o usando lambdabot , que lo integra como el comando @djinn .