Streams

Apr. 21st, 2017 05:52 pm
thedeemon: (vonny tropics)
[personal profile] 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)

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

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

Date: 2017-04-21 07:27 pm (UTC)
From: [personal profile] sassa_nf
а list comprehension есть? а tails линейный?

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

Date: 2017-04-24 09:44 am (UTC)
5ht: (Default)
From: [personal profile] 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.
Edited Date: 2017-04-24 09:45 am (UTC)

Date: 2017-04-22 09:32 am (UTC)
pbl: (Default)
From: [personal profile] pbl
Феноменально. Но почему Inf не мемоизируется? Если уж на то пошло, почему Lazy не мемоизируется, и какой он после этого Lazy?

Date: 2017-04-22 06:06 pm (UTC)
pbl: (Default)
From: [personal profile] pbl
Как-то это уж чересчур для 1.0.

Date: 2017-04-22 06:09 pm (UTC)
pbl: (Default)
From: [personal profile] pbl
А вы не хотите про это написать кляузу куда-нибудь в /r/Idris или порепортить на гитхабе? Или это задокументированное поведение? Сейчас ничего не нашел на эту тему, но смутно припоминаю, что Lazy по крайней мере обещали нормальное поведение с вычисляемостью ноль или один раз. Inf на тот момент еще не существовало.

Date: 2017-04-22 09:11 pm (UTC)
pbl: (Default)
From: [personal profile] pbl
Если у них такое спросить, а оно, типа, так задумано - они по-доброму посылают... я проверял. :-/

Date: 2017-04-24 07:09 pm (UTC)
bamalip: (Default)
From: [personal profile] bamalip
В репле вьічисления в Идрисе идут не так, как в компилированном коде. Єто надо учитьівать, в том числе при оценке асимптотической сложности.

Profile

thedeemon: (Default)
Dmitry Popov

May 2017

S M T W T F S
 1234 56
789 10 11 1213
14151617181920
21222324252627
28293031   

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 23rd, 2017 02:54 pm
Powered by Dreamwidth Studios