[Haskell-cafe] agda v. haskell

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
(http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php).

-- 
/NAD