agda/doc/HCAR/May-2008.tex

\documentclass{article}

\usepackage{hcar}

\begin{document}

\begin{hcarentry}{Agda}
\label{agda}
\report{Nils Anders Danielsson}
\status{Actively developed by a number of people}
\makeheader

Do you crave for highly expressive types, but do not want to resort to
type-class hackery? Then Agda might provide a view of what the future
has in store for you.

Agda is a dependently typed functional programming language (developed
using Haskell). The language has inductive families, i.e.\ GADTs
which can be indexed by \emph{values} and not just types. Other
goodies include parameterised modules, mixfix operators, and an
\emph{interactive} Emacs interface (the type checker can assist you in
the development of your code).

A lot of work remains in order for Agda to become a full-fledged
programming language (effects, good libraries, mature compilers,
documentation, etc.), but already in its current state it can provide
lots of fun as a platform for experiments in dependently typed
programming.

New since last time:
\begin{itemize}
\item A simple foreign function interface, which allows use of Haskell
  functions in Agda code.
\item The libraries are steadily increasing in size.
\end{itemize}

\FurtherReading
  The Agda Wiki: \url{http://www.cs.chalmers.se/~ulfn/Agda/}
\end{hcarentry}

\end{document}