26
我在學習agda。但是，我遇到了問題。我在agda wiki上發現的所有教程對我來說都太複雜，涵蓋了編程的各個方面。在平行閱讀關於agda的3個教程之後，我能夠編寫簡單的證明，但我仍然沒有足夠的知識將其用於真正的字算法正確性。如何學習agda
你能推薦我關於這個主題的任何教程嗎？類似於學習你自己的Haskell，但對於Agda。
Q
如何學習agda
A
回答
18
大約一年前，當我開始學習Agda時，我想我嘗試了所有可用的教程，並且每次都教給我一些新的東西。
你或許應該給予勒柯克一試，因爲它有一個更大的用戶羣，並有適用於它提供了兩個漂亮的書：
- Coq'Art - 有點過時，但初學者友好
- Certified Programming with Dependent Types
好的是，Agda和Coq基於的理論有點類似，所以很多例子都可以從一個翻譯到另一個。 Programming in Martin-Löf's Type Theory是一個非常好的可讀的介紹依賴型理論，它可以爲你清除一些事情。
這將有助於瞭解「真實世界算法」的含義。 papers which mention Agda中描述了許多示例開發。
16
Conor McBride去年使用Agda進行了依賴型編程的a great series of lectures。如果你想從關於這個主題的簡潔教程中解脫出來，這是一個很好的去處。我相信也有相應的練習。
相關問題（稍後問）：http://stackoverflow.com/questions/13497865/where-to-start-with-dependent-type-programming/14292455#14292455 – 2013-01-12 15:25:03
不Agda但伊德里斯，但仍然相當相關： https://vimeo.com/117221082 – 2015-03-07 14:30:51