haskell - Idris entusiasta evaluación

lazy-evaluation evaluation

Question

En Haskell , podría implementar if así:

if'' True  x y = x
if'' False x y = y
spin 0 = ()
spin n = spin (n - 1)

Esto se comporta como espero :

haskell> if'' True  (spin 1000000) ()  -- takes a moment
haskell> if'' False (spin 1000000) ()  -- immediate

En Racket , podría implementar un fallo if así:

(define (if2 cond x y) (if cond x y))
(define (spin n) (if (= n 0) (void) (spin (- n 1))))

Esto se comporta como espero :

racket> (if2 #t (spin 100000000) (void))  -- takes a moment
racket> (if2 #f (spin 100000000) (void))  -- takes a moment

En Idris , podría implementar if así:

if'' : Bool -> a -> a -> a
if'' True  x y = x
if'' False x y = y
spin : Nat -> ()
spin Z = ()
spin (S n) = spin n

Este comportamiento me sorprende :

idris> if'' True  (spin 1000) ()  -- takes a moment
idris> if'' False (spin 1000) ()  -- immediate

Esperaba que Irdis se comportara como Racket, donde se evalúan ambos argumentos. ¡Pero ese no es el caso!

¿Cómo decide Idris cuándo evaluar las cosas?

Answer 1

Decimos que Idris tiene una evaluación estricta, pero esto es por su semántica en tiempo de ejecución.

Al ser un lenguaje totalmente dependiente, Idris tiene dos fases en las que evalúa las cosas, el tiempo de compilación y el tiempo de ejecución. En tiempo de compilación, solo evaluará las cosas que sabe que son totales (es decir, que terminan y cubren todas las entradas posibles) a fin de que la comprobación de tipos sea decidible. El evaluador en tiempo de compilación es parte del kernel Idris, y se implementa en Haskell utilizando una representación de valores de estilo HOAS (sintaxis abstracta de orden superior). Como se sabe que todo tiene una forma normal aquí, la estrategia de evaluación en realidad no importa porque de cualquier manera obtendrá la misma respuesta, y en la práctica hará lo que el sistema de tiempo de ejecución Haskell decida hacer.

El REPL, por conveniencia, utiliza la noción de evaluación en tiempo de compilación. Entonces, tu ''spin 1000'' nunca se está evaluando. Si haces un ejecutable con el mismo código, esperaría ver un comportamiento muy diferente.

Además de ser más fácil de implementar (porque tenemos el evaluador disponible), esto puede ser muy útil para mostrar cómo se evalúan los términos en el verificador de tipos. Entonces puedes ver la diferencia entre:

Idris> /n, m => (S n) + m
/n => /m => S (plus n m) : Nat -> Nat -> Nat

Idris> /n, m => n + (S m)
/n => /m => plus n (S m) : Nat -> Nat -> Nat

Esto sería más difícil (aunque no imposible) si usáramos la evaluación en tiempo de ejecución en REPL, que no se reduce en lambdas.