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 зависимостей между сигналами.