Streams

Apr. 21st, 2017 05:52 pm
thedeemon: (vonny tropics)
Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово 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)

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

— Не пугайтесь, Екатерина Петровна, и не волнуйтесь. Только нет в мире никакого равновесия. И ошибка-то всего на какие-нибудь полтора килограмма на всю вселенную, а все же удивительно, Екатерина Петровна, совершенно удивительно!
thedeemon: (office)
Забавная танцевальная битва Idris vs. Scala, где Miles Sabin пытается на Скале воспроизвести пару примеров использования зависимых типов, показанных перед этим на Идрисе:
http://www.infoq.com/presentations/scala-idris (40 минут видео)
Не очень успешно.
thedeemon: (office)
К чему был предыдущий пост. У меня тут написанный на Идрисе кодогенератор, который генерит десятки разных вариаций компенсации движения на С++, т.е. на выходе много текста. Лучше всего для этого дела подошла бы string interpolation, но в Идрисе такого нету и не предвидится. В окамле вон есть модуль Printf, где вызов вроде
Printf.sprintf "%d %s of beer" 99 "bottles"
вернет строчку
"99 bottles of beer"
и компилятор проверит, что число и типы параметров соответствуют формат-строке, это умение встроено в сам компилятор как специальный случай для этого модуля, насколько я помню. Но в Идрисе такого тоже нет, поэтому приходилось просто соединять строчки оператором ++, получалось не слишком удобно. Теперь же вот сделал себе упрощенный аналог sprintf, который просто вставляет строчки в нужные позиции. Вместо
"bigLuma.halveBlockHP(" ++ vec st ++", " ++ block ++ ");"
"PBlock<"++ w++"> "++block++" = halfLuma.makePBlock<"++w++">();"
теперь просто
ins "bigLuma.halveBlockHP($, $);" (vec st) block
ins "PBlock<$> $ = halfLuma.makePBlock<$>();" w block w
Параметры пока только строковые, но зато соответствие их числа формат-строке проверяется статически.

Реализовано так:
Read more... )
thedeemon: (office)
Описанная ниже функция add принимает натуральное число n и n интов и возвращает сумму этих интов. Т.е.
add 0 == 0
add 1 42 == 42
add 2 33 44 == 77
add 8 2 2 2 2 2 2 2 2 == 16
Вот так она описывается на Идрисе:
sumType : Nat -> Type
sumType Z = Int
sumType (S k) = Int -> sumType k

adder : (n:Nat) -> Int -> sumType n
adder Z acc = acc
adder (S k) acc = \x => adder k (x + acc)

add : (n:Nat) -> sumType n
add Z = 0
add (S k) = adder k 

Можно ли ее еще упростить и обойтись без вспомогательной функции adder? Че-то я торможу.
thedeemon: (passport)
До чего дошел прогресс:

Эдак скоро захочешь безобидную утилиту поставить, а она яндекс.бар ∞-группоиды качает!

Хозяйке на заметку: Идрис с каждой новой версией имеет все больше зависимостей, в версии 0.9.9 уже дошли до ручки LLVM (теперь там и такой есть бэкенд). Если не хочется возиться с его установкой, то волшебная фраза такая: "cabal install idris -f -LLVM".
thedeemon: (faculty of numbers)
Недавно я писал про простой шаг, добавляющий в систему типов обычного ФЯП зависимые типы: достаточно добавить один1 тип Type, элементами которого служат типы. Что занятно, из этого шага автоматически тут же следует первоклассность типов: они сразу же становятся обычными значениями, и их можно помещать в туплы, списки и т.д. и применять к ним обычные операции. Успешно компилирующийся в Идрисе пример:

swap : (a,b) -> (b,a)
swap (a,b) = (b,a)

v : fst $ swap ("hi there", head [Int, String])
v = 42

По этой причине в Идрисе нет ключевого слова newtype. Чтобы определить синоним типа, достаточно описать его как значение (или как функцию, частный случай значения):
Matrix : Type -> Type
Matrix a = List (List a)

m : Matrix Int
m = [[1,2], [3,4]]
thedeemon: (office)
В классической логике есть закон исключения третьего, гласящий, что для любого утверждения А справедливо A | -A, т.е. либо оно верно, либо ложно. Однако это очень смелое утверждение, его можно трактовать так, что любое утверждение разрешимо (decidable), что тоже довольно нагло, и вообще герр Гёдель хмурится. Интуиционисткая логика высказываний и с ней конструктивная математика и прочая теория типов ведут себя скромнее, и такого смелого утверждения не делают. Но зато в них доказуемо вот такое:
--(A | -A)
Давайте его докажем, используя тот же Идрис, хотя ровно так же док-во записывается на Хаскеле. Отрицание определено как импликация в абсурд, т.е. отрицание утверждения А это функция, которая из доказательства А производит абсурд (_|_). Тогда наше утверждение записывается так:

((А | (A -> _|_) -> _|_) -> _|_

В теории типов в синтаксисе Идриса оно становится типом функции:

M : ((Either A (A -> _|_)) -> _|_) -> _|_

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

f : (Either A (A -> _|_)) -> _|_

Нам нужно, используя ее одну, произвести _|_. На вход она принимает либо А, либо -А. Взять значение типа А нам неоткуда, значит нужна функция типа A -> _|_. Как ее построить? Сделать лямбду, которая принимает значение А, и скармливает его f, а она уже произведет _|_. Имея такую функцию типа A -> _|_, ее можно опять же скормить f, и тогда получить _|_ "из ничего". Выглядит это так:
  M f = f (Right g) where
    g a = f (Left a)

Вот так, используя только переданную на вход f, скармливая ей использующую ее же функцию, можно произвести _|_ и так получить конструктивное доказательство --(A | -A). Что это значит? Что хоть мы в интуиционизме и конструктивизме и не утверждаем, что для всякого утверждения А верно (A | -A), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.
thedeemon: (office)
В теории типов, конечно. Сегодня в нашем тавтологическом кружке для самых маленьких азы зависимых типов мимоходом. Аксиома выбора может быть сформулирована по-разному, например так: для любого семейства непустых множеств A существует функция выбора f, определённая на A. Берем мы кучу непустых множеств, вводим индексацию, т.е. каждое множество из этой кучи соотносим с элементом из некоторого множества А, например, числом; получили семейство множеств. Для конечного набора множеств используем конечное множество индексов А, для счетного множества множеств - счетное множество индексов, например A=Nat, можем даже взять континуум разных множеств и адресовать их вещественными числами, так у нас в семействе даже будет множество с индексом Пи. Сами множества в семействе могут быть очень разной природы. Перейдя от множеств к типам, мы получаем семейство типов, индексированное типом А, т.е. для каждого х из А у нас будет тип Bx, для разных х тип может быть разным, и собрание всех этих Bx будет нашим семейством типов, зависимым типом. Исходное семейство множеств мы можем представить бинарным отношением R(x,y), где x из А, а y из Bx. Факт того, что это семейтсво непустых множеств, можно выразить требованием для R быть left-total: для каждого х из А обязан существовать хотя бы один y из Bx, для которых выполнено отношение R(x,y). Тогда из наличия такого вот отношения R следует существование функции f из А в Bx, которая для каждого х из А выбирает некоторый элемент y из множества Bx, для которого выполнено R(x,y). Это и есть аксиома выбора, и сейчас мы ее докажем конструктивно как теорему. Математически утверждение выглядит так:

(∀x:A . ∃y:Bx . R(x,y)) => (∃f : A -> Bx . ∀x:A . R(x, f x))

Запишем это утверждение и его доказательство на ЯП с зависимыми типами Idris. Read more... )
thedeemon: (office)
Захотелось мне недавно реализовать циклический сдвиг непустого вектора (списка с длиной в типе) на Идрисе. Пишу:
rotLeft : Vect a (S n) -> Vect a (S n)
rotLeft v = tail v ++ [head v]

А компилятор мне отвечает, что он хоть и умный, но ленивый, и ему не очевидно, что n+1 это n+1, ну в смысле что результат применения функции сложения натурального числа n с константой 1 это следующее за n число.
"Can't unify Vect a (m + n) with Vect a (S n)
Specifically: Can't unify plus m with S"
Для случаев, когда код правильный, но компилятор не убежден в корректности типов, в Идрисе есть специальные доказательства и интерактивный режим их построения посредством тактик. Пишем так:
rotLeft v ?= tail v ++ [head v]

Знак вопроса перед равенством означает, что корректность типов будет доказана отдельной леммой. Запускаем REPL. Он такой код принимает, а по команде :m показывает, что есть одна незакрытая лемма:
Global metavariables:  [Main.rotLeft_lemma_1]

Спрашиваем ее тип:
> :t rotLeft_lemma_1
rotLeft_lemma_1 : (a : Type) -> (n : Nat) -> (Vect a (S n)) -> (Vect a (n + (S O))) 
-> Vect a (S n)

Тип ее говорит, что это функция, принимающая на вход аргументы исходной функции и ее результат в том виде, который смог вывести компилятор (Vect a (n + (S O)), где S O - это натуральная единица в унарной записи), а на выходе должна выдать значение того типа, что мы указали выходным типом исходной функции (Vect a (S n)). Перехожу в интерактивный режим доказательств: :p rotLeft_lemma_1, после чего как та мартышка с печатной машинкой пробую разные тактики (это был мой первый опыт, я тогда об этих тактиках почти ничего не знал). Вижу, что последовательность из двух тактик intros и trivial лемму закрывает: Read more... )
thedeemon: (office)
Понадобились мне тут в хозяйстве деревья, я взял пилу, топор и пошел в гугл, нашел там AA-деревья, про которые говорится, что они по эффективности как красно-черные, но в реализации проще. Это бинарное дерево, у каждой вершины (узла) есть "уровень", ее высота. Узлы с данными есть двух видов: первый вид имеет форму /\, оба поддерева ниже текущей вершины, обозначим его буквой А. Узлы второго имеют форму Г, в них правое поддерево той же высоты, что и текущая вершина, а левое поддерево ниже; обозначим второй вид буквой H. Инвариант для АА-деревьев звучит так:
1. The level of every leaf node is one.
2. The level of every left child is exactly one less than that of its parent.
3. The level of every right child is equal to or one less than that of its parent.
4. The level of every right grandchild is strictly less than that of its grandparent.
5. Every node of level greater than one has two children.

Тут leaf node - это вершина, у которой нет поддеревьев. Четвертое условие гарантирует, что в дереве не будет цепочек из горизонтальных ребер, поэтому, двигаясь от корня к любой вершине, мы будем спускаться на уровень вниз не реже, чем в половине шагов, а значит самый длинный путь в дереве не более чем в два раза длиннее самого короткого, что дает логарифмическое соотношение высоты и общего числа вершин.

Любой нормальный язык позволяет эти инварианты выразить в типах. Вот так, например, это выглядит в Идрисе:
data Tree : Type -> Nat -> Bool -> Type where
  Null  : Tree a 0 False
  ANode : Tree a n b1 -> a -> Tree a n b2 -> Tree a (n+1) False
  HNode : Tree a n b -> a -> Tree a (n+1) False -> Tree a (n+1) True

Read more... )

strlen

Jan. 24th, 2013 09:23 pm
thedeemon: (office)
В Идрисе один из базовых типов - String, внутри представленный как null-terminated C string. Знаете, как узнать длину такой строки? Сконвертить в список Char'ов, а потом посчитать его длину. А все потому, что хоть в рантайме идриса и есть нормальная функция вычисления длины (по-хорошему ее вообще стоило бы хранить, а не вычислять), в стандартную библиотеку ее забыли экспортнуть. У них там в академии своя атмосфера.
thedeemon: (office)
Все мы помним про карринг, позволяющий функцию, принимающую пару аргументов, заменить на функцию от одного аргумента, возвращающую функцию от второго, которая уже возвращает нужный результат. Типы ((a,b) -> c) и (a -> b -> c) эквивалентны, т.к. мы можем описать две функции от одного к другому и обратно, композиция которых равна id, т.е. построить изоморфизмы. Запишем их на хаскелеподобном языке Идрис:
id1 : ((a,b) -> c) -> (a -> b -> c)
id1 f = \a => \b => f (a,b)

id2 : (a -> b -> c) -> ((a,b) -> c)
id2 f = \pair => f (fst pair) (snd pair)

В хаскеле они есть в стандартной библиотеке под именами curry и uncurry. Теперь вспомним соответствие Карри-Говарда, связывающее типы с утверждениями, а значения с доказательствами. Произведение типов (тупл, product type) там превращается в конъюнкцию, функциональный тип - в следствие. Фактически, выше мы доказали утверждение
((A & B) => C) == (A => (B => C))

Теперь перенесемся в мир зависимых типов, взяв тот же язык Идрис. Одним из базовых элементов, появляющихся с зависимыми типами, является зависимая пара - обобщение произведения типов, также известное как зависимая сумма (dependent sum):Read more... )
thedeemon: (office)
Недавно видел жалобу на то, что с монадами код разрастается, и простые выражения порой требуют несколько строчек для записи (речь про do-нотацию была). Сейчас осваиваю потихоньку язык Idris - это такой правильный хаскель с полноценными зависимыми типами (о которых чуть позже) и кучей встроенных плюшек для создания eDSL'ей (об этом вероятно еще позже). Так вот, в идрисе для монад сахара еще подсыпали, хочу поделиться. Пусть у нас есть функция readInt типа String -> IO Int, запрашивающая и получающая число откуда-то из внешнего мира, и мы хотим прочитать два числа и вывести их сумму. В языках вроде Clean или ML, где для монад вообще никаких спецсредств нету, это выглядит весьма печально. В хаскеле и идрисе есть привычная всем do-нотация:
main = do
  a <- readInt "a"
  b <- readInt "b"
  print (a+b)

Вот и получилось много строк на ровном месте. Первый кусочек сахара: monad comprehensions. Они когда-то были в хаскеле, потом потерялись, есть ли сейчас - не знаю. Идея в том, чтобы list comprehensions обобщить с монады List на произвольные монады:
main = [a + b | a <- readInt "a", b <- readInt "b"] >>= print

Не особо короче, чем вариант do с фигурными скобками и точками с запятой, но сама идея занятная.

Еще один вариант, доступный и в хаскеле: спрятать весь plumbing в операторы. Это как раз происходит, если вспомнить, что монада это функтор, а в наших языках еще и аппликативный:
class Functor f => Applicative (f : Type -> Type) where 
    pure  : a -> f a
    (<$>) : f (a -> b) -> f a -> f b
и
main = (pure (+) <$> readInt "a" <$> readInt "b") >>= print

(это на идрисе, в хаскеле некоторые значки будут другими, но в целом то же самое)

Второй кусочек сахара: idiom brackets. Специальный синтаксис для аппликативных функторов, где функции автоматически отображаются функтором с помощью pure, а их применения заменяются на применения образов через <$>:
main = [|readInt "a" + readInt "b"|] >>= print

(рассахаривается в предыдущий вариант)
В хаскеле похожая штука есть, но выглядит довольно страшно.

Еще пример для закрепления. Вот такую функцию
m_mul : Maybe Int -> Maybe Int -> Maybe Int
m_mul (Just x) (Just y) = Just (x * y)
m_mul _ _ = Nothing

можно записать как
m_mul x y = [| x * y |]

Profile

thedeemon: (Default)
Dmitry Popov

September 2017

S M T W T F S
     12
3456789
10111213141516
17181920212223
24252627282930

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 26th, 2017 07:24 am
Powered by Dreamwidth Studios