[Haskell-cafe] agda v. haskell
Nils Anders Danielsson
nad at cs.chalmers.se
Sat Sep 29 08:41:46 EDT 2007
On Fri, 28 Sep 2007, Jeff Polakow <jeff.polakow at db.com> wrote:
> Agda is essentially an implementation of a type checker for
> Martin-Lof type theory (i.e. dependent types).
> It is designed to be used as a proof assistant.
Well, the language aims to become a practical programming language.
Ulf's recently defended PhD thesis has the title "Towards a practical
programming language based on dependent type theory"
(http://www.cs.chalmers.se/~ulfn/papers/thesis.html). Lots of work
remains to be done before this goal is reached, though.
In the meantime, Agda is an excellent vehicle for experiments in
dependently typed programming with inductive families (≈ GADTs). For
more information, see the Agda wiki
More information about the Haskell-Cafe