2016-06-30 5 views
2

Чтение и игра с некоторыми примерами из официального учебника Идриса оставила меня немного смущенной относительно ленивой оценки.confused об ленивой оценке в Idris

Как указано в руководстве Идрис использует нетерпеливый оценку, и они идут на, чтобы дать пример, когда это не было бы уместно

ifThenElse : Bool -> a -> a -> a 
ifThenElse True t e = t 
ifThenElse False t e = e 

И затем перейти, чтобы показать пример, используя ленивые вычисления

ifThenElse : Bool -> Lazy a -> Lazy a -> a 
ifThenElse True t e = t 
ifThenElse False t e = e 

Мне нравится пробовать что-то при чтении, поэтому я создал неэффективную функцию Фибоначчи, чтобы протестировать не-ленивый и ленивый ifThenElse.

fibo : Nat -> Nat 
fibo Z = Z 
fibo (S Z) = S Z 
fibo (S(S Z)) = S(S Z) 
fibo (S(S(S n))) = fibo (S(S n)) + fibo (S n) 

-- the non lazy 
ifThenElse1 : Bool -> (t: a) -> (f: a) -> a 
ifThenElse1 False t f = f 
ifThenElse1 True t f = t 

-- should be slow when applied to True 
iftest1 : Bool -> Nat 
iftest1 b = ifThenElse1 b (fibo 5) (fibo 25) 

-- the lazy 
ifThenElse2 : Bool -> (t: Lazy a) -> (f: Lazy a) -> a 
ifThenElse2 False t f = f 
ifThenElse2 True t f = t 

-- should be fast when applied to True 
iftest2 : Bool -> Nat 
iftest2 b = ifThenElse2 b (fibo 5) (fibo 25) 

Учитывая, что Идрис следует выполнять нетерпеливый оценку, я бы ожидать, что исполнение iftest1 быть замедлен (fibo 25) даже при нанесении на True. Тем не менее, как iftest1, так и iftest2 выполняются очень быстро при применении к True. Так, может быть, мое понимание ленивости/рвения в корне ошибочно?

Что является хорошим примером, чтобы наблюдать разницу между ленинностью и рвением в Идрисе?

ответ

2

Вы, вероятно, пробовали iftest1 и iftest2 от Idris REPL. The REPL uses different evaluation order than compiled code

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

REPL, для удобства, использует оценку времени компиляции.

+0

Итак, я должен уметь видеть разницу для скомпилированного кода? Я просто попытался создать основную функцию, которая принимает некоторый пользовательский ввод, который затем используется для создания логического для функции 'iftest1'. Я скомпилировал файл в исполняемый файл, запустил его и дал ему некоторый ввод. Однако кажется, что 'iftest1' все еще ведет себя так, как будто он ленив. Я также попытался сделать функцию Фибоначчи не полной, но она ничего не изменила. Что было бы лучшим примером, чтобы наблюдать ленивость и рвение? (если вообще возможно создать такой пример) – Michelrandahl

+2

Попробуйте сделать 'b: Bool' зависимым от некоторого ввода, поэтому' iftest1 b' не может быть уменьшен во время компиляции. – xash