← Back to branch summary

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

« back to all changes in this revision

Viewing changes to doc/HCAR/November-2012.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/November-2012.tex
1
 
\documentclass{article}
2
 
 
3
 
\usepackage{hcar}
4
 
 
5
 
\begin{document}
6
 
 
7
 
% Agda-NA.tex
8
 
\begin{hcarentry}[section,updated]{Agda}
9
 
\label{agda}
10
 
\report{Nils Anders Danielsson}%11/12
11
 
\status{actively developed}
12
 
\participants{Ulf Norell, Andreas Abel, and many others}
13
 
\makeheader
14
 
 
15
 
Agda is a dependently typed functional programming language (developed
16
 
using Haskell). A central feature of Agda is inductive families,
17
 
i.e.\ GADTs which can be indexed by \emph{values} and not just types.
18
 
The language also supports coinductive types, parameterized modules,
19
 
and mixfix operators, and comes with an \emph{interactive}
20
 
interface---the type checker can assist you in the development of your
21
 
code.
22
 
 
23
 
A lot of work remains in order for Agda to become a full-fledged
24
 
programming language (good libraries, mature compilers, documentation,
25
 
etc.), but already in its current state it can provide lots of fun as
26
 
a platform for experiments in dependently typed programming.
27
 
 
28
 
The next version of Agda is still under development. Some of the
29
 
changes were mentioned in the last HCAR entry. More recently Stevan
30
 
Andjelkovic has contributed a LaTeX backend, with the aim to support
31
 
both precise, Agda-style highlighting, and lhs2TeX-style alignment of
32
 
code.
33
 
 
34
 
\FurtherReading
35
 
  The Agda Wiki: \url{http://wiki.portal.chalmers.se/agda/}
36
 
\end{hcarentry}
37
 
 
38
 
\end{document}