Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Added hakyll, rewrote some parts.

  • Loading branch information...
commit b94a4df8643fce5a738919f6d4f0f289f95394f8 1 parent 8e2a28a
@liamoc authored
View
158 css/style.css
@@ -0,0 +1,158 @@
+
+/* FONTS FEATURED AT liamoc.net */
+/*
+*/
+pre {
+ background-color: #EBEBEB;
+ padding:5px;
+ padding-left:20px;
+}
+.right {
+ float:right;
+}
+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 {
+ margin-left:50px;
+}
+.caption {
+ font-size:10px;
+}
+td.lineNumbers pre {background-color: #EBEBEB; }
+.aside {
+ background-color: #EBEBAA;
+ padding:5px;
+ padding-left:20px;
+ padding-right:20px;
+}
+.aside pre {
+ background-color: white;
+}
+td.sourceCode { padding-left: 5px; }
+pre.sourceCode { }
+pre.sourceCode span.Normal { }
+pre.sourceCode span.Keyword { color: #AA00AA; }
+pre.sourceCode span.DataType { color: #800000; }
+pre.sourceCode span.DecVal { color: #0000FF; }
+pre.sourceCode span.BaseN { color: #0000FF; }
+pre.sourceCode span.Float { color: #800080; }
+pre.sourceCode span.Char { color: #FF00FF; }
+pre.sourceCode span.String { color: #DD0000; }
+pre.sourceCode span.Comment { color: #808080; }
+pre.sourceCode span.Others { }
+pre.sourceCode span.Alert { color: green; }
+pre.sourceCode span.Function { color: #000080; }
+pre.sourceCode span.RegionMarker { }
+pre.sourceCode span.Error { color: red; }
+
+.titleimage {
+ font-family: serif;
+ float:left;
+ margin:0px;
+ margin-left:18px;
+ font-size:42px;
+}
+
+
+
+#content {
+ background: #FFFFFF;
+ padding: 20px;
+
+}
+code {
+ font-family: monospace;/*
+ float:left;
+ margin-top:5px;
+ margin-bottom:20px;
+ width:100%;
+ padding:15px;
+ padding-left:30px;
+ border-left:10px solid #CCCCCC;*/
+
+}
+
+tt {
+ font-family: monospace;
+}
+
+pre {
+ font-family: monospace;
+}
+
+a {
+ color:#222255
+}
+a:visited {
+ color:#555577;
+}
+a:hover {
+ color:#5555AA;
+}
+.titlesub {
+ color:#444444;
+ font-size:14px;
+ margin-left:3px;
+}
+.title {
+ font-family: serif;
+ font-size: 38px;
+}
+.date {
+ font-size: 17px;
+ color:#444444;
+}
+.container {
+ margin-left:auto;
+ margin-right:auto;
+ max-width:900px;
+ min-width:640px;
+ text-align:justify;
+}
+
+.box {
+ margin-left:20px;
+ margin-right:20px;
+ margin-top:35px;
+}
+
+ul {
+ list-style-type: square;
+}
+
+body {
+ margin:60px;
+ margin-bottom:20px;
+ font-family: sans-serif;
+ background: #CCCCCC;
+}
+
+h1 {
+ font-family: serif;
+ font-weight:normal;
+ color:#222222;
+}
+h2 {
+ font-family: serif;
+ color:#444444;
+ font-weight:normal;
+}
+h3 {
+ font-family: serif;
+ font-weight:normal;
+
+}
+.header {
+ text-align:right;
+ height:78px;
+ vertical-align:bottom;
+ margin-right:15px;
+ padding-top:9px;
+}
+.footer {
+ font-size:12px;
+ color:#444444;
+ text-align:center;
+ margin-top:40px;
+}
View
4 footer.markdown
@@ -0,0 +1,4 @@
+--- footer
+Copyright © Liam O'Connor 2010. CC/BY
+
+Site Generated by [Hakyll](http://jaspervdj.be/hakyll/) and [Haskell](http://www.haskell.org).
View
19 hakyll.hs
@@ -0,0 +1,19 @@
+#!/usr/bin/runhaskell
+import Text.Hakyll
+import Text.Hakyll.Render
+import Text.Hakyll.File
+import Text.Hakyll.CreateContext
+import Text.Pandoc.Shared
+
+withHeader = (`combine` createPage "header.markdown")
+withFooter = (`combine` createPage "footer.markdown")
+
+main = hakyllWithConfiguration conf $ do
+ directory static "static"
+ directory css "css"
+ directory render "pages"
+ where render = renderChain ["templates/default.html"]
+ . withHeader
+ . withFooter
+ . createPage
+ conf = (defaultHakyllConfiguration "http://learnyouanagda.com") { pandocWriterOptions = defaultWriterOptions { writerHTMLMathMethod = GladTeX } }
View
2  header.markdown
@@ -0,0 +1,2 @@
+--- header
+
View
33 introduction.md → pages/introduction.md
@@ -1,8 +1,10 @@
-Introduction
-============
+-----
+title: Introduction
+date: 16th Febuary 2011
+-----
About this tutorial
--------------------
+===================
Welcome to *Learn You an Agda and Achieve Enlightenment!*. If you're reading this,
you're probably curious as to what Agda is, why you want to learn it, and in general what
@@ -16,6 +18,9 @@ to give it a try. Learning Agda was a very rewarding but very difficult process
is my hope that, by writing this tutorial, it will become a little bit easier for everyone
else.
+Step One: Learn Haskell
+-----------------------
+
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
@@ -36,9 +41,9 @@ to fall into place in my head. Agda is *hard*. After some time, though, Agda's i
awesomeness comes to the fore, and it all just clicks. If you encounter
obstacles in your Agda learning, don't be discouraged! Keep working, and eventually
you will be a master of Agda fu.
-
+
What is Agda, anyway?
----------------------
+=====================
Agda is a programming language, but not a programming language like Java. It's not
even very much like Haskell, although it's a lot more like Haskell than Java.
@@ -64,7 +69,7 @@ type terms.
In fact, you could think of any type system this way. In C++, people exploit the Turing-completeness
of their type system to perform compile-time analysis and computation. While such type level work
-is very powerful, I fear that such manipulations are
+is very powerful, I fear that such type machinery is
very often difficult to understand and manipulate. Even in Haskell, applications that make
extensive use of type-level computation are very often substantially harder to comprehend.
The type-level "language" is almost always substantially more complicated to work with than the value-level "language"[^1].
@@ -84,9 +89,15 @@ In fact, seeing as the language of values and the language of types are the same
that you can express about a value can be expressed statically in its type, and machine checked
by Agda. We can statically eliminate any error scenario from our program.
+Types are Proofs
+----------------
+
+<img class='img right' src='/static/owl.png' />
+
If I can come up with a function of type `Foo -> Bar` (and Agda says that it's type correct)
that means that I've, in addition to written a program, also written a proof by construction
-that, assuming some premise `Foo`, the judgement `Bar` holds. We'll touch more on proofs later.
+that, assuming some premise `Foo`, the judgement `Bar` holds (We'll touch more on proofs later -
+I don't want to get bogged down in details just yet)
Seeing as our `Foo` and `Bar` can be as expressive as we like, this lets us prove *anything we
want* about our program simply by exploiting this correspondence between proofs and programs -
@@ -94,7 +105,7 @@ called the [Curry-Howard Correspondence](http://en.wikipedia.org/wiki/Curry–Ho
discovered by two brilliant logicians in the sixties.
<div class="aside">
-#### Why Prove when you can just test?
+### Why prove when you can just test?
The validity of formal verification of software is often hotly contested by programmers who usually
have no experience in formal verification. Often testing methodologies are presented as a more viable
alternative.
@@ -151,17 +162,17 @@ Once you have Haskell and Emacs, there are three things you still need to do:
"agda" to find out). If not or otherwise, simply use the Haskell platform's `cabal-install` tool
to download, compile, and set up Agda.
- $ cabal install agda agda-executable
+ $ cabal install agda agda-executable
* Install Agda mode for emacs. Simply type in a command prompt (where Agda is in your `PATH`):
- $ agda-mode setup
+ $ agda-mode setup
* Install Haskell mode for emacs. If Haskell mode is not available in your package manager, you
can [download Haskell mode](http://www.iro.umontreal.ca/μonnier/elisp/#haskell-mode) and install
it by adding to your `.emacs` file[^0]:
- (setq load-path (cons "/path/to/my/haskell/mode" load-path))
+ (setq load-path (cons "/path/to/my/haskell/mode" load-path))
By then you should be all set. To find out if everything went as well as expected, head on over
to the next section, "Hello Peano!".
View
69 peano.md → pages/peano.md
@@ -1,8 +1,10 @@
-Hello, Peano
-============
+-----
+title: Hello, Peano
+date: 16th Feb 2011
+-----
Definitions, Definitions
-------------------------
+========================
So, unlike the previous chapter, this chapter will actually involve some coding in Agda.
@@ -21,8 +23,13 @@ data ℕ : Set where
To begin, we type `data ℕ`. The `data` keyword means we're defining a type - in this case, `ℕ`. For this example, we're specifying that this type, `ℕ`, is of type `Set` (that's what
the colon means).
-Hold on a second, types have types? If you recall the introduction, I mentioned that in Agda, types and values are treated the same way. Therefore, because values have types, types have
-to have types as well! Even `Set` (the type of our type `ℕ`) has a type: `Set₁`, which has a type `Set₂`, going on all the way up to infinity. We'll touch more on what these
+Hold on a second, types have types?
+-----------------------------------
+
+If you recall the introduction, I mentioned that in Agda, types and values are treated the same way. This means that, seeing as values are given types, types are
+given types as well. Types are merely a special group of language terms, and in Agda, all terms have types.
+
+Even `Set` (the type of our type `ℕ`) has a type: `Set₁`, which has a type `Set₂`, going on all the way up to infinity. We'll touch more on what these
`Set` types mean later, but for now you can think of `Set` as the type we give to all the data types we use in our program.
<div class="aside">
@@ -31,6 +38,9 @@ only values "smaller" than ν, (for example, `Set₁` cannot contain `Set₁` or
admissable.
</div>
+Structural Induction
+---------------------
+
Okay, so, we've defined our type, but now we need to fill the type with values. While a type with no values does have its uses, a natural numbers type with no values is
categorically wrong. So, the first natural number we'll define is zero:
@@ -49,12 +59,18 @@ Here we are simply declaring the term `zero` to be a member of our new type `ℕ
~~~
But we'd quickly find our text editor full of definitions and we'd be no closer to defining all the natural numbers than when we started. So, we should instead refer to a strict
-mathematical definition:
+mathematical definition. The notation I'm using here should be familiar to anyone who knows set theory and/or first-order logic - don't panic if you don't know these things,
+we'll be developing models for similar things in Agda later, so you will be able to pick it up as we go along.
+
+* Zero is a natural number (`0∈ℕ`).
+* For any natural number `ν`, `ν + 1` is also a natural number. For convenience, We shall refer to `ν + 1` as `suc ν`[^1]. (`∀ν∈ℕ → suc ν∈ℕ`).
+
+This is called an *inductive definition* of natural numbers. We call it *inductive* because it consists of a *base* rule, where we define a fixed starting point,
+and an *inductive* rule that, when applied to an element of the set, *induces* the next element of the set. This is a very elegant way to define infinitely large sets.
-* Zero is a natural number (`0∈ ℕ`).
-* For any natural number `ν`, `ν + 1` is also a natural number. For convenience, We shall refer to `ν + 1` as `suc ν`[^1]. (`∀ν∈ℕ → suc ν∈ ℕ`).
+We will look at inductive *proof* in the coming chapters, which shares a similar structure.
-This is called an *inductive definition* of natural numbers. For the base case, we've already defined zero to be in ℕ by saying:
+For the base case, we've already defined zero to be in ℕ by saying:
~~~{.agda}
data ℕ : Set where
@@ -65,9 +81,8 @@ For the second point (the inductive rule), it gets a little more complicated. Fi
∀ν ∈ ℕ → suc ν ∈ ℕ
-This means, given a natural number `ν`, the constructor `suc` will return another natural number. What is the *type* of `suc`? It takes one argument (`ν`), which
-we know is a natural number from the premise of the rule, and it returns a natural number, which we know from the conclusion. This means that we can define
-the constructor `suc` like so:
+This means, given a natural number `ν`, the constructor `suc` will return another natural number. So, in other words, `suc` could be considered a *function*
+that, when given a natural number, produces the next natural number. This means that we can define the constructor `suc` like so:
~~~{.agda}
data ℕ : Set where
@@ -81,7 +96,7 @@ Now we can express the number one as `suc zero`, and the number two as `suc (suc
Incidentally, this definition of natural numbers corresponds to the Haskell data type:
~~~{.haskell}
-\data Nat = Zero | Suc Nat
+data Nat = Zero | Suc Nat
~~~
If you load that into GHCi and ask it what the type of `Suc` is, it (unsurprisingly) will tell you: `Nat -> Nat`. This is a good way to get an intuition for
@@ -100,7 +115,7 @@ book won't carry over directly to extended Haskell.
</div>
One, Two.. Five!
-----------------
+================
Now we're going to define some arithmetic operations on our natural numbers. Let's try addition, first.
@@ -119,13 +134,15 @@ functions where the arguments can appear anywhere within a term. You use undersc
So, an if-then-else construct in Agda can be declared with[^3]:
~~~{.agda}
-if_then_else : ∀ { a } → Bool → a → a → a
+if_then_else_ : ∀ { a } → Bool → a → a → a
~~~
-This syntactic flexibility delivers great expressive power, but be careful about using it too much, as it can get very confusing!
+This can be used with great flexibility: You can call this function with `if a then b else c`, which desugars to `if_then_else_ a b c`. This syntactic
+flexibility delivers great expressive power, but be careful about using it too much, as it can get very confusing!
+
</div>
-Now, let's implement this function by structural recursion[^4]
+Now, let's implement this function by structural recursion[^4].
~~~{.agda}
_+_ : ℕ → ℕ → ℕ
@@ -135,7 +152,7 @@ zero + n = n
~~~
Our First Check
----------------
+===============
Normally we'd run the program at this point to verify that it works, but in Agda one does that pretty rarely. Instead, what we do is get Agda to *check* our code. This checks
that all our proof obligations have been met:
@@ -143,26 +160,28 @@ that all our proof obligations have been met:
* It checks your types. Types are how you encode proofs in Agda (although we haven't done any non-trivial proofs yet), so this is important.
* It checks that your program provably terminates. Checking that any program terminates is in general undecidable (see [The Halting Problem](http://en.wikipedia.org/wiki/Halting_problem)),
but proof obligations can only be machine-checked by Agda if your program terminates. To circumvent this dilemma, Agda runs its checker only on *structural* recursion with
-finite data structures, and warns that it can't check proof obligations if non-structural recursion is ever used. We will discuss this more in later chapters.
+finite data structures, and warns that it can't check proof obligations if non-structural recursion is ever used. We will discuss this more in later chapters, but the only examples
+presented in the early part of this book will be ones that Agda can already prove terminates.
-To run a check, type `C-c C-l` into emacs, or choose Load from the Agda menu. If your program checks correctly, there will be no hole markers (yellow highlighting) and no
+To run a check, type `C-c C-l` into emacs, or choose Load from the Agda menu. If your program checks correctly, there will be no error messages, no hole markers (yellow highlighting) and no
orange-highlighted non-terminating sections. It should also say `Agda: Checked` at the bottom of the window, and you get syntax highlighting.
+Right now, our checks aren't all that meaningful - the only thing they prove is that our addition function does indeed take any natural number and produce a natural number, as
+the type suggests. Later on, when we encode more information in our types, our checks can mean a lot more - even more than running and testing the program.
+
"I Have Merely Proven It Correct"
---------------------------------
To evaluate an expression (just to verify that it truly does work), we can type `C-c C-n` into emacs, or select "Evaluate term to normal form" from the Agda menu. Then, in the
minibuffer, we can type an expression for 3 + 2:
- (suc (suc (suc n))) + (suc (suc n))
+ (suc (suc (suc n))) + (suc (suc n))
And we get the result (5):
- (suc (suc (suc (suc (suc n)))))
-
-
+ (suc (suc (suc (suc (suc n)))))
[^1]: `suc` standing for successor.
[^2]: Unlike Haskell, type declarations are mandatory.
[^3]: Don't worry if you're scared by that `∀` sign, all will be explained in time.
-[^4]: Structural recursion is when a recursive function follows the structure of a recursive data type - it occurs very frequently in functional programs.
+[^4]: Don't be scared by the term - structural recursion is when a recursive function follows the structure of a recursive data type - it occurs very frequently in functional programs.
View
0  illustrations/completed/cover.png → static/cover.png
File renamed without changes
View
0  illustrations/completed/owl.png → static/owl.png
File renamed without changes
View
24 templates/default.html
@@ -0,0 +1,24 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html lang=en>
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" >
+<link rel="stylesheet" href="/css/style.css" />
+<title>Liam O'Connor - $title </title>
+</head>
+<body>
+<div class=container>
+<div class='titleimage'>Learn you an Agda</div>
+<div class='header'>
+$header
+</div>
+<div id="content">
+<div class='title'>$title</div>
+<div class='date'>$date</div>
+$body
+
+<div class='footer'>$footer</div>
+</div>
+</div>
+</body>
+</html>
Please sign in to comment.
Something went wrong with that request. Please try again.