Зависимые типы имеют реальное практическое применение. И бояться их не надо, они могут встречаться в самых неожиданных местах. Посмотрите внимательно в вашем коде, я думаю скорее всего найдете пару-тройку применений зависимых типов. И это — не обязательно сложные математические доказательства.
Более мощная система типов повышает выразительную мощь языка, что позволяет лаконичнее описывать решение практической задачи.
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
