Dmitry Popov

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово 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)

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

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

К чему был предыдущий пост. У меня тут написанный на Идрисе кодогенератор, который генерит десятки разных вариаций компенсации движения на С++, т.е. на выходе много текста. Лучше всего для этого дела подошла бы 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... )

До чего дошел прогресс:

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

Хозяйке на заметку: Идрис с каждой новой версией имеет все больше зависимостей, в версии 0.9.9 уже дошли до ручки LLVM (теперь там и такой есть бэкенд). Если не хочется возиться с его установкой, то волшебная фраза такая: "cabal install idris -f -LLVM".

В классической логике есть закон исключения третьего, гласящий, что для любого утверждения А справедливо 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), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.

Захотелось мне недавно реализовать циклический сдвиг непустого вектора (списка с длиной в типе) на Идрисе. Пишу:

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... )

В Идрисе один из базовых типов - String, внутри представленный как null-terminated C string. Знаете, как узнать длину такой строки? Сконвертить в список Char'ов, а потом посчитать его длину. А все потому, что хоть в рантайме идриса и есть нормальная функция вычисления длины (по-хорошему ее вообще стоило бы хранить, а не вычислять), в стандартную библиотеку ее забыли экспортнуть. У них там в академии своя атмосфера.

Недавно видел жалобу на то, что с монадами код разрастается, и простые выражения порой требуют несколько строчек для записи (речь про 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 |]