суботу, 24 серпня 2013 р.

Dependent types at work

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

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

четвер, 15 серпня 2013 р.

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