Действительно ли Идрис строго оценивается?

Исходя из Haskell, я читал историю Идриса о лени (нестрогости). Я просмотрела последние примечания к выпуску и нашла код, похожий на следующий

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
myIf True t e = t
myIf False t e = e

Я написал простую факториальную функцию, чтобы проверить ее.

myFact : Int -> Int
myFact n = myIf (n == 1) 1 (n * myFact (n-1))

Я запустил, и это сработало!

> myFact 5
120 : Int

Я решил сломать его, изменив сигнатуру типа myIf на

myIf : (b : Bool) -> a -> a -> a

Я перезагрузил idris repl и снова запустил myFact 5, ожидая бесконечной рекурсии. К моему удивлению, он все еще работал так же!

Может ли idris понять, когда следует избегать строгости? Почему это не повторилось навсегда?

Я использую Idris 0.9.15, и ни в одном из примечаний к выпуску между этим и связанными примечаниями не упоминаются какие-либо изменения.


lazy-evaluation idris
person mjgpy3    schedule 02.10.2015    source источник
comment
Мой REPL делает то же самое. Однако я получаю бесконечный цикл, если я вызываю myFact с :x в REPL или компилирую в исполняемый файл.   -  person C. Quilley    schedule 02.10.2015
comment
Возможный дубликат нетерпеливой оценки Idris   -  person Cactus    schedule 06.10.2015

Ответы (1)


arrow_upward
18
arrow_downward

Объяснение здесь: http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-ожидать-что-происходит

Семантика оценки во время компиляции и во время выполнения различается (неизбежно, поскольку во время компиляции средству проверки типов необходимо оценивать выражения при наличии неизвестных значений), и REPL использует понятие времени компиляции как для удобства, так и потому, что это полезно для посмотрите, как уменьшаются выражения в средстве проверки типов.

Однако здесь есть еще кое-что. Идрис заметил, что myIf — очень маленькая функция, и решил встроить ее. Таким образом, при компиляции myFact на самом деле имеет определение, которое выглядит примерно так:

myFact x = case x == 1 of
                True => 1
                False => x * myFact (x - 1)

Таким образом, обычно вы можете писать управляющие структуры, такие как myIf, не беспокоясь о том, чтобы сделать что-то Lazy, потому что Idris все равно скомпилирует их в желаемую управляющую структуру. То же самое касается, например. && и || и короткое замыкание.

person Edwin Brady    schedule 03.10.2015
comment
Является ли эта встроенная оптимизация правильной, когда она меняет семантику? - person luochen1990; 24.04.2017
comment
Это не меняет семантику. Вы получаете один и тот же ответ для всех входных данных, как бы вы это ни делали. - person Edwin Brady; 24.04.2017
comment
Но это меняет всю совокупность, что трудно понять, особенно когда пользователь переключается на какой-то похожий стиль кодирования (например, некоторые изменения, которые делают код уже недостаточно маленьким для встраивания), ожидая, что поведение программ не изменится, но программы могут опять не работает.. - person luochen1990; 24.04.2017
comment
Это не меняет тотальности... РЕДАКТИРОВАТЬ: Ах, конечно, вы имеете в виду, что это меняет окончание этого конкретного выражения, поэтому я должен немного уточнить: Идрис будет думать, что бы он ни делал для оптимизации, что myFact не является тотальным . И, в любом случае, поскольку он не тотальный, он не будет его оценивать при проверке типов. Есть разумный аргумент в пользу того, что это встраивание должно выполняться только тогда, когда определение является полным. - person Edwin Brady; 25.04.2017