Re: [Haskell-cafe] agda v. haskell

On Fri, 28 Sep 2007, Jeff Polakow 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