Agda

Instalacja

Na systemach uniksowych zdecydowanie polecana jest instalacja przez Cabal: cabal update && cabal install Agda. Należy zwrócić uwagę, że do korzystania w pełni z możliwości system potrzebny jest Emacs -- po zainstalowaniu Agdy Emacsa konfigurujemy przez polecenie agda-mode setup. Dokładniejsze informacje. Dla systemów windowsowych dostępny jest instalator, który sam ściąga i instaluje cały komplet: Haskell Platform, Agdę, Emacsa i zestaw czcionek. Informacje dla Windows.

Do rozwiązania naszych zadań nie będzie to potrzebne, ale warto w wolnym czasie zainstalować bibliotekę standardową Agdy. Jest tam sporo bardzo ciekawego kodu!

Samouczki i dokumentacja

Lista samouczków jest dość obszerna, jednak nie wszystkie są całkiem aktualne. Pierwsza pozycja na liście (Ulf Norell and James Chapman. Dependently Typed Programming in Agda) jest na pewno dobra. Kolejna pozycja (Dependent Types at Work) także zawiera sporo ciekawych przykładów. Jest dostępnych także kilka wykładów video, wykład Daniela Peeblesa powinien być dość przystępny i mieć czytelne slajdy.

W dokumentacji na Agda Wiki mamy dostęp do podręcznika. Bardzo przydatne są strony o wprowadzaniu symboli unikodowych oraz o sterowaniu trybem emacsowym.

Artykuły

Lista artykułów korzystających z Agdy jest bardzo długa, na początek proponujemy zobaczyć bardzo ciekawe możliwości samych typów zależnych:

1. Why dependent types matter, 2006, Thorsten Altenkirch, Conor McBride, James McKinna
2. The power of Pi, ICFP 2008, Nicolas Oury and Wouter Swierstra

Osoby, które będą chciały dowiedzieć się jak to działa "pod spodem" powinny rzucić okiem na pracę doktorską Ulfa Norella, który jest głównym implementatorem bieżącego wcielenia Agdy.