Browse files

Added some introduction illustrations

  • Loading branch information...
1 parent 5c6a0e0 commit dc133418e4892f42ad3cbe21f22d396cadd4dc94 @liamoc committed Mar 4, 2011
Showing with 22 additions and 2 deletions.
  1. +14 −0 css/style.css
  2. +8 −2 pages/
  3. BIN static/koala.png
  4. BIN static/types.png
14 css/style.css
@@ -24,13 +24,27 @@ pre {
.right {
+ margin-left:20px;
+} {
+ position:relative;
+ left:auto;
+ right:auto;
+.left {
+ float:left;
+ margin-right:20px;
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode, table.sourceCode pre
{ margin: 0; padding: 0; border: 0; vertical-align: baseline; border: none; }
td.lineNumbers { text-align: right; background-color: #EBEBEB; color: black; padding-right: 5px; padding-left: 5px;font-family:Monaco,monospace; font-size:11px; }
.figure {
+.img {
+ margin-bottom:15px;
.caption {
10 pages/
@@ -23,15 +23,19 @@ else.
Step One: Learn Haskell
+<img class='img left' src='/static/koala.png' />
This tutorial is not aimed at anyone completely new to programming. Agda is similar on
a basic level to typed functional languages such as Haskell and ML, and so knowing a
language in the ML family will certainly make learning Agda a great deal easier. If you
don't know a statically typed functional language, I recommend that you learn Haskell,
as Agda has a close relationship with the Haskell ecosystem. If you're looking for a good
Haskell tutorial, look no further than this book's companion, [Learn You a Haskell](
+You should only have to read the first few chapters of this book in order to get a feel
+for Agda.
-Really, I mean it. If you don't know Haskell (or ML), learn it before trying to tackle
+If you don't know how purely functional programming works, learn a little of it before
+trying to tackle Agda.
Understanding of imperative and object oriented programming (C, Java, Ruby..) isn't
necessary. In fact, trying to apply skills learnt from these languages might even be
@@ -60,6 +64,8 @@ an expression's type might just be a concrete type, like `Bool` or `Int`. Java (
generics), C++ (through templates) and Haskell all support polymorphic types as well,
such as `List a` or `Map k v`.
+<img class='img right' src='/static/types.png' />
But, if `List a` is a type, then what exactly *is* just `List` (without the parameter)?
Haskell calls it a "type constructor", but really it's a *function* at the type level. `List` takes in a type, say `Int`,
and returns a new type, `List Int`. Haskell (with appropriate extensions) even supports arbitrary functions on the
BIN static/koala.png
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
BIN static/types.png
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.

0 comments on commit dc13341

Please sign in to comment.