Идрис с нетерпением - программирование

В Haskell я мог бы реализовать if следующим образом:

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

Это ведет себя так, как я ожидаю:

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

В Racket я мог реализовать испорченный if следующий:

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

Это ведет себя так, как я ожидаю:

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

В Idris я мог бы реализовать if следующим образом:

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

Такое поведение меня удивляет:

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

Я ожидал, что Irdis будет вести себя как Racket, где оба аргумента оценены. Но это не так!

Как Идрис решает, когда оценивать вещи?

Ответ 1

Мы говорим, что у Идриса строгая оценка, но это для семантики времени выполнения.

Будучи полностью зависимым от типизированного языка, Идрис имеет две фазы, где он оценивает вещи, время компиляции и время выполнения. Во время компиляции он будет оценивать только то, что, как известно, является тотальным (то есть завершение и покрытие всех возможных входов), чтобы держать проверку типов разрешимой. Оценщик времени компиляции является частью ядра Idris и реализован в Haskell с использованием представления значений значений типа HOAS (более высокий порядок абстрактного синтаксиса). Поскольку все, как известно, имеет нормальную форму здесь, стратегия оценки фактически не имеет значения, потому что в любом случае он получит тот же ответ, и на практике он будет делать то, что хочет выполнить система времени выполнения Haskell.

В REPL для удобства используется понятие оценки времени компиляции. Таким образом, ваш "spin 1000" никогда не получает оценку. Если вы создадите исполняемый файл с тем же кодом, я ожидаю увидеть совсем другое поведение.

Кроме того, что проще реализовать (потому что у нас есть оценщик), это может быть очень полезно, чтобы показать, как термины оцениваются в контроле типа. Таким образом, вы можете увидеть разницу между:

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

Это было бы сложнее (хотя и не невозможно), если бы мы использовали оценку времени выполнения на REPL, которая не уменьшается при lambdas.