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

[pbl]

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