Чтение и игра с некоторыми примерами из официального учебника Идриса оставила меня немного смущенной относительно ленивой оценки.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. Так, может быть, мое понимание ленивости/рвения в корне ошибочно?
Что является хорошим примером, чтобы наблюдать разницу между ленинностью и рвением в Идрисе?
Итак, я должен уметь видеть разницу для скомпилированного кода? Я просто попытался создать основную функцию, которая принимает некоторый пользовательский ввод, который затем используется для создания логического для функции 'iftest1'. Я скомпилировал файл в исполняемый файл, запустил его и дал ему некоторый ввод. Однако кажется, что 'iftest1' все еще ведет себя так, как будто он ленив. Я также попытался сделать функцию Фибоначчи не полной, но она ничего не изменила. Что было бы лучшим примером, чтобы наблюдать ленивость и рвение? (если вообще возможно создать такой пример) – Michelrandahl
Попробуйте сделать 'b: Bool' зависимым от некоторого ввода, поэтому' iftest1 b' не может быть уменьшен во время компиляции. – xash