programar - haskell inteligencia artificial

¿Cómo superamos la brecha de tiempo de compilación y de tiempo de ejecución cuando programamos en un lenguaje tipificado de manera dependiente?

Question

Me dicen que en el sistema de tipos dependiente, "tipos" y "valores" se mezclan, y podemos tratar a ambos como "términos" en su lugar.

Pero hay algo que no puedo entender: en un lenguaje de programación fuertemente tipado sin Tipo Dependiente (como Haskell), los Tipos se deciden (deducen o verifican) en tiempo de compilación , pero los valores se deciden (se calculan o ingresan) en tiempo de ejecución .

Creo que debe haber una brecha entre estas dos etapas. Solo piense que si un valor se lee interactivamente desde STDIN, ¿cómo podemos hacer referencia a este valor en un tipo que debe decidirse AOT?

por ejemplo, hay un número natural n y una lista del número natural xs (que contiene n elementos) que necesito leer de STDIN, ¿cómo puedo colocarlos en una estructura de datos Vect n Nat ?

Answer 1

Me parece que hay dos preguntas aquí:

1. Dado que algunos valores son desconocidos durante el tiempo de compilación (p. Ej., Valores leídos desde STDIN), ¿cómo podemos usarlos en tipos? (Tenga en cuenta que chi ya ha dado una excelente respuesta a esto ).

2. Algunas operaciones (por ejemplo, getLine ) parecen no tener ningún sentido en el momento de la compilación; ¿Cómo podríamos hablar de ellos en tipos?

La respuesta a (1), como ha dicho chi, es un razonamiento simbólico o abstracto. Puede leer un número n , y luego realizar un procedimiento que genere un Vect n Nat mediante la lectura de la línea de comandos n veces, utilizando propiedades aritméticas como el hecho de que 1+(n-1) = n para valores naturales distintos de cero. números.

La respuesta a (2) es un poco más sutil. De manera ingenua, es posible que desee decir "esta función devuelve un vector de longitud n , donde n se lee desde la línea de comando". Hay dos tipos que podrías intentar dar (disculpas si me sale mal la notación de Haskell)

unsafePerformIO (do n <- getLine; return (IO (Vect (read n :: Int) Nat)))

o (en notación pseudo-Coq, ya que no estoy seguro de qué es la notación de Haskell para tipos existenciales)

IO (exists n, Vect n Nat)

Estos dos tipos pueden tener sentido y decir cosas diferentes. El primer tipo, para mí, dice "en tiempo de compilación, lee n desde la línea de comandos y devuelve una función que, en tiempo de ejecución, da un vector de longitud n al realizar IO". El segundo tipo dice "en tiempo de ejecución, realice IO para obtener un número natural n y un vector de longitud n ".

La forma en que me gusta ver esto es que todos los efectos secundarios (aparte de, quizás, la no terminación) son transformadores de mónada, y solo hay una mónada: la mónada del "mundo real". Los transformadores de mónada funcionan tan bien a nivel de tipo como a nivel de término; lo único que es especial es run :: M a -> a que ejecuta la mónada (o pila de transformadores de mónada) en el "mundo real". Hay dos puntos en el tiempo en los que puede invocar la run : uno es en tiempo de compilación, donde se invoca cualquier instancia de run que se muestra en el nivel de tipo. Otra es en tiempo de ejecución, donde invoca cualquier instancia de run que se muestre en el nivel de valor. Tenga en cuenta que run solo tiene sentido si especifica un orden de evaluación; Si su idioma no especifica si es llamada por valor o llamada por nombre (o llamada por valor o llamada por necesidad o llamada por otra cosa), puede obtener incoherencias cuando Intenta calcular un tipo.

Answer 2

Supongamos que ingresamos n :: Int en el tiempo de ejecución de STDIN. Luego leemos n cadenas, y las almacenamos en vn :: Vect n String (pretendo por el momento que se pueda hacer esto). Del mismo modo, podemos leer m :: Int y vm :: Vect m String . Finalmente, concatenamos los dos vectores: vn ++ vm (simplificando un poco aquí). Este puede ser verificado y tendrá el tipo Vect (n+m) String .

Ahora es cierto que el comprobador de tipos se ejecuta en tiempo de compilación, antes de que se conozcan los valores n,m , y también antes de que se conozcan vn,vm . Pero esto no importa: aún podemos razonar simbólicamente en las incógnitas n,m argumentamos que vn ++ vm tiene ese tipo, que involucra n+m , incluso si aún no sabemos qué es realmente n+m .

No es tan diferente de hacer matemáticas, donde manipulamos expresiones simbólicas que involucran variables desconocidas de acuerdo con algunas reglas, incluso si no conocemos los valores de las variables. No necesitamos saber qué número es n para ver que n+n = 2*n .

Del mismo modo, el comprobador de tipo puede escribir cheque

-- pseudocode
readNStrings :: (n :: Int) -> IO (Vect n String)
readNStrings O     = return Vect.empty
readNStrings (S p) = do
   s <- getLine
   vp <- readNStrings p
   return (Vect.cons s vp)

(Bueno, en realidad podría necesitarse un poco más de ayuda del programador para verificar esto, ya que implica la coincidencia y la recursión dependientes. Pero esto lo descuidaré).

Es importante destacar que el verificador de tipos puede verificarlo sin saber qué es n .

Tenga en cuenta que el mismo problema realmente surge con las funciones polimórficas.

fst :: forall a b. (a, b) -> a
fst (x, y) = x

test1 = fst @ Int @ Float (2, 3.5)
test2 = fst @ String @ Bool ("hi!", True)
...

Uno podría preguntarse "¿cómo puede verificar primero el tipógrafo sin saber qué tipos a y b serán en tiempo de ejecución?". De nuevo, razonando simbólicamente.

Con los argumentos de tipo, esto es posiblemente más obvio, ya que normalmente ejecutamos los programas después del borrado de tipo, a diferencia de los parámetros de valor como nuestro n :: Int anterior, que no se pueden borrar. Sin embargo, existe cierta similitud entre la cuantificación universal sobre tipos o sobre Int .