Dependent types. Don't need proofs

У многих зависимые типы ассоциируются с теоремами и доказательствами. Это и не странно, поскольку, наверное, первое, на что обращает внимание пытливый ум, это изоморфизм Карри-Ховарда. Но доказывать теоремы и проверять доказательства — это далеко не все, что можно делать с помощью зависимых типов.

А что, если бы не было изоморфизма Карри-Ховарда? Никаких теорем, никаких доказательств, никаких HoTT и так далее. Но что бы тогда осталось? Вы не поверите! Осталась бы суть... а именно зависимые типы.

Безопасный void* на Agda

В стандартной библиотеке Хаскеля есть тип Dynamic, который состоит из значения, тип которого как-бы утрачен, и тега, который представляется типом TypeRep. TypeRep — это по сути дерево из строк, среди которых есть имя пакета с версией, имя модуля, имя самого типа, и так для всех составляющих. Его можно использовать как уникальный идентификатор типа. Так он и используется в Dynamic, если TypeRep'ы одинаковы, unsafeCoerce'им.

Это конечно все очень удобно, но больно напоминает void*. По сути оно таким и является, даже похоже менее безопасным чем C++ RTTI (поскольку TypeRep можно задать самому, а к C++ typeid прямого доступа нет). Ну и как водится решил я написать такой TypeRep, который позволил бы безопасно делать то же. На Хаскеле сразу не получилось, по этому решил написать прототип на Агде. Круто:) на Агде пишем прототипы для Хаскеля. Заодно пришлось написать платформу для эмуляции Хаскельных type class'ов на Агде.

Из значений в типы...

Хаскель поддерживает зависимые типы — это уже давно не для кого не секрет. Конечно в нем это не очень родная возможность, но все же успешные опыты существуют. Но долго мне было непонятно как такое (см. ниже код на Агде) сделать на Хаскеле. Проблема в том, что значения n и m — это (внимание) значения, а они присутствуют в типе. В Агде так можно, но в Хаскеле типы и значения строго разделены.

main : IO Unit
main =
  getContents >>= λ stdin →
  let (n , m) = readℕ×ℕ stdin
      proof : n ≤ m ⊎ n > m
      proof = n ≤? m
  in
  putStrLn $ show proof

Dependent types at work

Зависимые типы имеют реальное практическое применение. И бояться их не надо, они могут встречаться в самых неожиданных местах. Посмотрите внимательно в вашем коде, я думаю скорее всего найдете пару-тройку применений зависимых типов. И это — не обязательно сложные математические доказательства.

Более мощная система типов повышает выразительную мощь языка, что позволяет лаконичнее описывать решение практической задачи.

Agda, Не останавливайтесь!

(Следующий этап — микроконтроллер)

Hello,

I'm trying to get Agda working on my Samsung chromebook.
I got to the point where I have ghci trunk working,
but I am stuck at getting Agda trunk to work with ghc
I compiled (and the dependent packages). This is needed
for the interactive Emacs mode. Therefore I'd like to know
if it's possible to run agda interpreter on ARM at all,
has anybody tried this? I notice that Agda trunk does not
compile with ghc trunk is there any plan to fix it?

Thanks,
Wojciech
_______________________________________________
Agda mailing list
Agda@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

NoCopyPaste Paranoid

Напишу ка я идеальный NoCopyPaste Quicksort на Haskell.

Elm <~ FRP ~ Magic

Добрался до Web:) А именно до Elm, который построен на идиоме функционального реактивного программирования. Это такой подход в котором с одной стороны функциональная чистота и декларативность, а с другой удобность построения интерактивного графического интерфейса. Вещи, которые могут изменятся, представляются в виде сигналов. А вся программа представляется в виде pure functional зависимостей между сигналами.

Erlang: Dynamic vs Static

Имел как-то я неосторожность обмолвится, что Erlang — не совсем динамически типизирован, даже немножко статически.

Но давайте смотреть.

Матан для лямбда-исчисления

Интересная и очень полезная вещь мне открылась в Haskell.

Разбираясь с Cont монадой, я не мог понять, почему первое приближение оператора bind в виде простой аппликации плохое, то есть:

m >>= f = m f

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

m >>= f = \k -> m (\a -> f a k)

Мне хотелось быстро сравнить два подхода и понять предельно чисто, где кроется суть. Но как? И тут пришло просветление. Нужно как в матане перебрать все варианты аргументов и посмотреть какие будут результаты.

Легко и непринужденно пишем Regex

Итак мы уже поняли зачем Эрик использует список и ничто нам не мешает двигаться дальше. Как вы уже знаете парсер имеет тип Parser a, где a – это тип значения, которое может вернуть парсер, если ему скормить строку, а что если a – это Parser 'a, то есть все целиком имеет тип Parser (Parser a)?

Why laziness matters

По мотивам лекции. Там Эрик пишет функциональный парсер, а для типа возвращаемого значения использует список. Я решил углубиться в реализацию, поэкспериментировать, начал писать, но не имея понятия зачем там список, решил использовать Maybe.

Как я на Erlang'е OOP делал

Написал в учебных целях утилиту для разбора build-output'а (Visual Studio/Incredibuild). Код тут.

Uniqueness types in Agda

Сразу линк. Данная реализация уникальных типов на Agda базируется на явном управлении контекстом. Каждый оператор рассматривается как преобразователь контекста (Transformer в коде). Преобразователь характеризуется сигнатурой (Types) входа (то, что он употребляет, consumes, и удаляет с контекста) и сигнатурой выхода (то, что добавляет в контекст).