Streams

[thedeemon]

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

data Stream : Type -> Type where
(::) : (value : elem) -> Inf (Stream elem) -> Stream elem

Благодаря автоматическому расставлению делеев и форсов, код с такими коданными выглядит так же просто и чисто, как в хаскеле:

countFrom : Integer -> Stream Integer
countFrom x = x :: countFrom (x+1)

first : Nat -> Stream a -> List a
first Z xs = []
first (S k) (x :: xs) = x :: first k xs

prepend : List a -> Stream a -> Stream a
prepend [] ys = ys
prepend (x :: xs) ys = x :: prepend xs ys

Обратите внимание, что в функциях выше :: используется в паттерн-матчинге и в конструировании сразу и для списков и для стримов, компилятор сам по типу понимает где что, и для стримов вставляет delay/force.
Подобно Основное Теореме Арифметики и Основной Теореме Алгебры, есть Основная Теорема Функционального Программирования (это, по Карри-Говарду, конечно же тоже функция), ее можно записать так:

fibs : Stream Integer
fibs = 1 :: 1 :: zipWith (+) fibs (drop 1 fibs)

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

— Не пугайтесь, Екатерина Петровна, и не волнуйтесь. Только нет в мире никакого равновесия. И ошибка-то всего на какие-нибудь полтора килограмма на всю вселенную, а все же удивительно, Екатерина Петровна, совершенно удивительно!

Comments

[sassa_nf]

а list comprehension есть? а tails линейный?

fibs = 1 :: 1 :: [ x + y | x :: y :: _ <- tails fibs ]

[thedeemon]

comprehension есть, но синтаксис там сложный паттерн-матчинг не позволяет, можно так:

fibs = 1 :: 1 :: [ sumFirstTwo s | s <- tails fibs ]

где
sumFirstTwo : Num a => Stream a -> a
sumFirstTwo (x::y::_) = x + y

Но реализован comprehension для стримов как-то ужасно, работает плохо (репл быстро съедает всю память). Можно так написать:

fibs = 1 :: 1 :: map sumFirstTwo (tails fibs)

Тогда работает ок, но время все равно не линейное. При этом готовой реализации tails для стримов не было, я ее так написал:

tails : Stream a -> Stream (Stream a)
tails src@(x :: xs) = src :: tails xs

Если присмотреться, видно, что мемоизации не происходит и одни и те же элементы будут много раз вычисляться.

[5ht]

Смысл же в том, что интро-конструкторы и элиминатор в data и codata свапнутые.
Поэтому cons листовый добавляет элементы, а для стрима — распаковывает (действительно лениво).
У нас в OM Lazy тоже присутствует для имплемнтации макроса If например
Lazy := λ (a: *) → λ (x: a) → λ (y: #Unit/@) → x
If := λ (A : *) → λ (X : #Bool) → λ (Y : #Lazy A) → λ (Z : #Lazy A) → X (#Lazy A) Y Z #Unit/Make
Странно, что они выбрали это для бесконечных деревьев, вместо нормальной коиндукции и cofix.

[pbl]

Феноменально. Но почему Inf не мемоизируется? Если уж на то пошло, почему Lazy не мемоизируется, и какой он после этого Lazy?

[thedeemon]

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

[pbl]

Как-то это уж чересчур для 1.0.

[pbl]

А вы не хотите про это написать кляузу куда-нибудь в /r/Idris или порепортить на гитхабе? Или это задокументированное поведение? Сейчас ничего не нашел на эту тему, но смутно припоминаю, что Lazy по крайней мере обещали нормальное поведение с вычисляемостью ноль или один раз. Inf на тот момент еще не существовало.

[thedeemon]

Ну я пока не изучил вопрос и его историю в достаточной степени.

[pbl]

Если у них такое спросить, а оно, типа, так задумано - они по-доброму посылают... я проверял. :-/

[bamalip]

В репле вьічисления в Идрисе идут не так, как в компилированном коде. Єто надо учитьівать, в том числе при оценке асимптотической сложности.