diff --git a/index.md b/index.md index 40e349ba..051d155a 100644 --- a/index.md +++ b/index.md @@ -21,7 +21,7 @@ http://homepages.inf.ed.ac.uk/wadler/ - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }}) --> - - [Naturals: Natural numbers]({{ "/Naturals" | relative_rul }}) + - [Naturals: Natural numbers]({{ "/Naturals" | relative_url }}) - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }}) - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }}) - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }}) diff --git a/out/Basics.md b/out/Basics.md index 15285abe..8d5a4cc6 100644 --- a/out/Basics.md +++ b/out/Basics.md @@ -1,3 +1,4 @@ + --- title : "Basics: Functional Programming in Agda" layout : page @@ -5,433 +6,1612 @@ permalink : /Basics --- 
{% raw %}
-open import Relation.Binary.PropositionalEquality Data.Empty       using (_≡_⊥; refl⊥-elim)
-{% endraw %}
- -The functional programming style brings programming closer to -simple, everyday mathematics: If a procedure or method has no side -effects, then (ignoring efficiency) all we need to understand -about it is how it maps inputs to outputs -- that is, we can think -of it as just a concrete method for computing a mathematical -function. This is one sense of the word "functional" in -"functional programming." The direct connection between programs -and simple mathematical objects supports both formal correctness -proofs and sound informal reasoning about program behavior. - -The other sense in which functional programming is "functional" is -that it emphasizes the use of functions (or methods) as -_first-class_ values -- i.e., values that can be passed as -arguments to other functions, returned as results, included in -data structures, etc. The recognition that functions can be -treated as data in this way enables a host of useful and powerful -idioms. - -Other common features of functional languages include _algebraic -data types_ and _pattern matching_, which make it easy to -construct and manipulate rich data structures, and sophisticated -_polymorphic type systems_ supporting abstraction and code reuse. -Agda shares all of these features. - -This chapter introduces the most essential elements of Agda. - -## Enumerated Types - -One unusual aspect of Agda is that its set of built-in -features is _extremely_ small. For example, instead of providing -the usual palette of atomic data types (booleans, integers, -strings, etc.), Agda offers a powerful mechanism for defining new -data types from scratch, from which all these familiar types arise -as instances. - -Naturally, the Agda distribution comes with an extensive standard -library providing definitions of booleans, numbers, and many -common data structures like lists and hash tables. But there is -nothing magic or primitive about these library definitions. To -illustrate this, we will explicitly recapitulate all the -definitions we need in this course, rather than just getting them -implicitly from the library. - -To see how this definition mechanism works, let's start with a -very simple example. - -### Days of the Week - -The following declaration tells Agda that we are defining -a new set of data values -- a _type_. - -
{% raw %}
-data Day : Set where
-  monday    : Day
-  tuesday   : Day
-  wednesday : Day
-  thursday  : Day
-  friday    : Day
-  saturday  : Day
-  sunday    : Day
-{% endraw %}
- -The type is called `day`, and its members are `monday`, -`tuesday`, etc. The second and following lines of the definition -can be read "`monday` is a `day`, `tuesday` is a `day`, etc." - -Having defined `day`, we can write functions that operate on -days. - -
{% raw %}
-nextWeekday : Day -> Day
 nextWeekdayopen monday    =import tuesday
-nextWeekdayRelation.Nullary tuesday   =using wednesday
-nextWeekday wednesday = thursday
-nextWeekday thursday  = friday
-nextWeekday friday    = monday
-nextWeekday saturday  = monday
-nextWeekday sunday    = monday
-{% endraw %}
- -One thing to note is that the argument and return types of -this function are explicitly declared. Like most functional -programming languages, Agda can often figure out these types for -itself when they are not given explicitly -- i.e., it performs -_type inference_ -- but we'll include them to make reading -easier. - -Having defined a function, we should check that it works on -some examples. There are actually three different ways to do this -in Agda. - -First, we can use the Emacs command `C-c C-n` to evaluate a -compound expression involving `nextWeekday`. For instance, `nextWeekday -friday` should evaluate to `monday`. If you have a computer handy, this -would be an excellent moment to fire up Agda and try this for yourself. -Load this file, `Basics.lagda`, load it using `C-c C-l`, submit the -above example to Agda, and observe the result. - -Second, we can record what we _expect_ the result to be in the -form of an Agda type: - -
{% raw %}
-test-nextWeekday : nextWeekday (nextWeekday¬_; saturdayDec; yes; no)
+open ≡import tuesdayRelation.Binary.PropositionalEquality
+                             using (_≡_; refl; _≢_; trans; sym)
 {% endraw %}
-This declaration does two things: it makes an assertion (that the second -weekday after `saturday` is `tuesday`), and it gives the assertion a name -that can be used to refer to it later. - -Having made the assertion, we must also verify it. We do this by giving -a term of the above type: +# Natural numbers 
{% raw %}
-test-nextWeekdaydata ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+{-# BUILTIN NATURAL ℕ #-}
+{% endraw %}
+ +
{% raw %}
+congruent : ∀ {m n} → m ≡ n → suc m ≡ suc n
+congruent refl = refl
+
+injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
+injective refl = refl
+
+distinct : ∀ {m} → zero ≢ suc m
+distinct ()
+{% endraw %}
+ +
{% raw %}
+_≟_ : ∀ (m n : ℕ) → Dec (m ≡ n)
+zero ≟ zero =  yes refl
+zero ≟ suc n =  no (λ()) 
+suc m ≟ zero =  no (λ())
+suc m ≟ suc n with m ≟ n
+... | yes refl =  yes refl
+... | no p =  no (λ r → p (injective r))
+{% endraw %}
+ +# Addition and its properties + +
{% raw %}
+_+_ : ℕ → ℕ → ℕ
+zero + n = n
+suc m + n = suc (m + n)
+{% endraw %}
+ +
{% raw %}
++-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p)
++-assoc zero n p = refl
++-assoc (suc m) n p rewrite +-assoc m n p = refl
+
++-zero : ∀ m → m + zero ≡ m
++-zero zero = refl
++-zero (suc m) rewrite +-zero m = refl
+
++-suc : ∀ m n → m + (suc n) ≡ suc (m + n)
++-suc zero n = refl
++-suc (suc m) n rewrite +-suc m n = refl
+
++-comm : ∀ m n → m + n ≡ n + m
++-comm m zero =  +-zero m
++-comm m (suc n) rewrite +-suc m n | +-comm m n = refl
 {% endraw %}
-There is no essential difference between the definition for -`test-nextWeekday` here and the definition for `nextWeekday` above, -except for the new symbol for equality `≡` and the constructor `refl`. -The details of these are not important for now (we'll come back to them in -a bit), but essentially `refl` can be read as "The assertion we've made -can be proved by observing that both sides of the equality evaluate to the -same thing, after some simplification." +# Equality and decidable equality for naturals -Third, we can ask Agda to _compile_ some program involving our definition, -This facility is very interesting, since it gives us a way to construct -_fully certified_ programs. We'll come back to this topic in later chapters. + + + +# Showing `double` injective + +
{% raw %}
+double : ℕ → ℕ
+double zero  =  zero
+double (suc n)  =  suc (suc (double n))
+{% endraw %}
+ +
{% raw %}
+double-injective : ∀ m n → double m ≡ double n → m ≡ n
+double-injective zero zero refl = refl
+double-injective zero (suc n) ()
+double-injective (suc m) zero ()
+double-injective (suc m) (suc n) r =
+   congruent (double-injective m n (injective (injective r)))
+{% endraw %}
+ +In Coq, the inductive proof for `double-injective` +is sensitive to how one inducts on `m` and `n`. In Agda, that aspect +is straightforward. However, Agda requires helper functions for +injection and congruence which are not required in Coq. + +I can remove the use of `congruent` by rewriting with its argument. +Is there an easy way to remove the two uses of `injective`? diff --git a/out/Stlc.md b/out/Stlc.md index d6ce9cb3..462370e9 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -38,8 +38,7 @@ lists, records, subtyping, and mutable state. ## Imports -
-
+
{% raw %}
 open)
-
-

+{% endraw %}
## Syntax @@ -301,8 +299,7 @@ Here is the syntax of types in BNF. And here it is formalised in Agda. -
-
+
{% raw %}
 infixrType
-
-

+{% endraw %}
Terms have six constructs. Three are for the core lambda calculus: @@ -409,8 +405,7 @@ Here is the syntax of terms in BNF. And here it is formalised in Agda. -
-
+
{% raw %}
 infixlTerm
-
-

+{% endraw %}
#### Special characters @@ -669,8 +663,7 @@ Here are a couple of example terms, `not` of type `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` which takes a function and a boolean and applies the function to the boolean twice. -
-
+
{% raw %}
 f)
-
-

+{% endraw %}
#### Bound and free variables @@ -991,8 +983,7 @@ to be weaker than application. For instance, - abbreviates `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` - and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``. -
-
+
{% raw %}
 ex₁refl
-
-

+{% endraw %}
#### Quiz @@ -1405,8 +1395,7 @@ as values. The predicate `Value M` holds if term `M` is a value. -
-
+
{% raw %}
 datafalse
-
-

+{% endraw %}
We let `V` and `W` range over values. @@ -1601,8 +1589,7 @@ name. Here is the formal definition in Agda. -
-
+
{% raw %}
 _[_:=_])
-
-

+{% endraw %}
The two key cases are variables and abstraction. @@ -2272,8 +2258,7 @@ Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE). Here is confirmation that the examples above are correct. -
-
+
{% raw %}
 ex₁₁refl
-
-

+{% endraw %}
#### Quiz @@ -3005,8 +2989,7 @@ and indeed such rules are traditionally called beta rules. Here are the above rules formalised in Agda. -
-
+
{% raw %}
 infixN
-
-

+{% endraw %}
#### Special characters @@ -3637,8 +3619,7 @@ are written as follows. Here it is formalised in Agda. -
-
+
{% raw %}
 infixN
-
-

+{% endraw %}
We can read this as follows. @@ -3839,8 +3819,7 @@ The names of the two clauses in the definition of reflexive and transitive closure have been chosen to allow us to lay out example reductions in an appealing way. -
-
+
{% raw %}
 reduction₁∎
-
-

+{% endraw %}