4da 21.02.2012 10:47 darkstar

Настолько ли неудобно писать на agda, как говорят?
Поскольку это ЯП (в том числе), для написания каких приложений он хорошо подходит?

programming, agda, ?
#oiesze
re 5 comments !recommend ~bookmark Ssubscribe
1. jtootf 21.02.2012 13:44

http://udpn.livejournal.com/65962.html

#oiesze/1
rereply
2. 4da → jtootf /1 21.02.2012 13:57 k-pax

udpn рассказывает, что формализует для себя некоторые вещи. ок. парсер на agda написать можно ?

#oiesze/2
rereply
3. jtootf → 4da /2 21.02.2012 14:00 galois

udpn пишет на Agda то, для чего Agda подходит. nivanych, емнип, переписывал с Haskell на Agda вебню, потому как ему системы типов не хватало. да, парсер на Agda написать можно

#oiesze/3
rereply
4. 4da → jtootf /3 21.02.2012 14:03 k-pax

то есть, на ней можно писать все, что можно писать на хаскеле (mod библиотеки)
что лучше подходит для расширения сознания? agda? coq? epigram? idris?

#oiesze/4
rereply
5. jtootf → 4da /4 21.02.2012 14:06 galois

LSD. Agda — это Мартин-Лёф, Epigram — UTT, Coq — что-то мощнее, не интересовался. про Idris впервые слышу. Isabelle/HOL — это, собственно, HOL

#oiesze/5
rereply
Do you really want to delete ?