Streams

[thedeemon]

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово Inf, и поле оказывается "ленивым": когда данные конструируются,

Comments

[thedeemon]

Если я все правильно путаю, дело в том, что когда отложенное вычисление производится, его результат не записывается на место thunk'a, как в хаскеле. Значение типа Stream Integer это пара из числа и функции, вычисляющей "хвост". Если мы эту пару передаем в два разных места (тут это zipWith и drop), и в одном месте вызывается ф-я вычисления хвоста, то в другом месте исходное значение не изменится, там по-прежнему хвост не вычислен, чтобы получить второе число последовательности нужно еще раз вызывать вычисление хвоста.

[_xacid_]

семантика call-by-name как в книжках

[ext_1178598]

> Выглядит не хуже чем в хаскеле. Но есть важный момент, который все портит: тут нет мемоизации

Это же вопрос исключительно реализации Delay (возвращает ли она простую санку или мемоизирующую обертку, желательно с поддержкой на уровне рантайма).

[thedeemon]

Да! Причем даже в окамле санки с мемоизацией:
# let x = lazy (print_string "Х"; 2) in Lazy.force x + Lazy.force x;;
Х- : int = 4

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

[maxim]

Теорема галимая, вот получше

CoFixpoint fib (a b: nat) : Stream nat := Cons a (fib b (a + b)).

#trollface

[thedeemon]

Она же на Идрисе:

f : Nat -> Nat -> Stream Nat
f a b = a :: f b (a + b)

[clayrat]

для совсем уже ленивых есть

codata Stream : Type -> Type where
(::) : (e : a) -> Stream a -> Stream a

которое рассахаривается в то, что в посте

(еще есть Lazy, которое совсем как Inf, но считается структурно "сходящимся")