← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to doc/HCAR/December-2007.tex

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HCAR/December-2007.tex
1
 
\documentclass{article}
2
 
 
3
 
\usepackage{hcar}
4
 
 
5
 
\begin{document}
6
 
 
7
 
\begin{hcarentry}{Agda}
8
 
\report{Nils Anders Danielsson}
9
 
\status{Actively developed by a number of people}
10
 
\makeheader
11
 
 
12
 
Do you crave for highly expressive types, but do not want to resort to
13
 
type-class hackery? Then Agda might provide a view of what the future
14
 
has in store for you.
15
 
 
16
 
Agda is a dependently typed functional programming language (developed
17
 
using Haskell). The language has inductive families, i.e.\@ GADTs
18
 
which can be indexed by \emph{values} and not just types. Other
19
 
goodies include parameterised modules, mixfix operators, and an
20
 
\emph{interactive} Emacs interface (the type checker can assist you in
21
 
the development of your code).
22
 
 
23
 
A lot of work remains in order for Agda to become a full-fledged
24
 
programming language (effects, good libraries, mature compilers,
25
 
documentation, \ldots), but already in its current state it can
26
 
provide lots of fun as a platform for experiments in dependently typed
27
 
programming.
28
 
 
29
 
\FurtherReading
30
 
  The Agda Wiki: \url{http://www.cs.chalmers.se/~ulfn/Agda/}
31
 
\end{hcarentry}
32
 
 
33
 
\end{document}