[Agda] Instance Arguments

出來跑，遲早都要還的... XD

最近在試著使用 agda 裡面的 record，尤其是用來模擬 haskell 中的 type class。不過，用起來一直怪怪的，到處都綁手綁腳的。剛好前兩天看到 josh 的文章，裡面提到今年的 ICFP 有人在弄 type classes in agda。哪裡還有客氣的，趕快去找來看 XD。

大概看過去，看起來相當不錯的感覺，不過就是他沒有寫清楚實作上的細節。稍微查了一下發現 agda 號稱 2.2.12 就會有開始提供這個東西：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
也有講到如何用 instance argument 來做 type class：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments

不過不過，現在 stable agda 才 2.2.10；development version 也才不過 2.2.11！看來只好慢慢等了。

另外，agda 的 instance arguments 畢竟還是和 haskell 裡面的 type class 不一樣。type class 基本上會自動遞迴地去試圖找出一個 instance，但是 instance argument 設計上限制我們必須要真的給它一個 instance。老實說，這邊目前還不是了解，看看以後能不能多懂一點。附上參考資料：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Non-recursiveResolutionForInstanceArguments