Function on types and advanced pattern matching

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

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

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.