1+ < h2 > Agda Full Example</ h2 >
2+ < p > ** Copyright - this piece of code is a modified version of [https://plfa.github.io/Naturals/] by Philip Wadler, Wen Kokke, Jeremy G Siek and contributors.</ p >
3+ < pre > < code > -- 1.1 Naturals
4+
5+ module plfa.part1.Naturals where
6+
7+ -- The standard way to enter Unicode math symbols in Agda
8+ -- is to use the IME provided by agda-mode.
9+ -- for example ℕ can be entered by typing \bN.
10+
11+ -- The inductive definition of natural numbers.
12+ -- In Agda, data declarations correspond to axioms.
13+ -- Also types correspond to sets.
14+ -- CHAR: \bN → ℕ
15+ data ℕ : Set where
16+ -- This corresponds to the `zero` rule in Dedekin-Peano's axioms.
17+ -- Note that the syntax resembles Haskell GADTs.
18+ -- Also note that the `has-type` operator is `:` (as in Idris), not `::` (as in Haskell).
19+ zero : ℕ
20+ -- This corresponds to the `succesor` rule in Dedekin-Peano's axioms.
21+ -- In such a constructive system in Agda, induction rules etc comes by nature.
22+ -- The function arrow can be either `-> ` or `→`.
23+ -- CHAR: \to or \-> or \r- → →
24+ suc : ℕ → ℕ
25+
26+ -- EXERCISE `seven`
27+ seven : ℕ
28+ seven = suc (suc (suc (suc (suc (suc (suc zero))))))
29+
30+ -- This line is a compiler pragma.
31+ -- It makes `ℕ` correspond to Haskell's type `Integer`
32+ -- and allows us to use number literals (0, 1, 2, ...) to express `ℕ`.
33+ {-# BUILTIN NATURAL ℕ #-}
34+
35+ -- Agda has a module system corresponding to the project file structure.
36+ -- e.g. `My.Namespace` is in
37+ -- `project path/My/Namespace.agda`.
38+
39+ -- The `import` statement does NOT expose the names to the top namespace.
40+ -- You'll have to use `My.Namespace.thing` instead of directly `thing`.
41+ import Relation.Binary.PropositionalEquality as Eq
42+ -- The `open` statement unpacks all the names in a imported namespace and exposes them to the top namespace.
43+ -- Alternatively the `open import` statement imports a namespace and opens it at the same time.
44+ -- The `using (a; ..)` clause can limit a range of names to expose, instead of all of them.
45+ -- Alternatively, the `hiding (a; ..)` clause can limit a range of names NOT to expose.
46+ -- Also the `renaming (a to b; ..)` clause can rename names.
47+ -- CHAR: \== → ≡
48+ -- \gt → ⟨
49+ -- \lt → ⟩
50+ -- \qed → ∎
51+ open Eq using (_≡_; refl)
52+ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
53+
54+ -- Addition of `ℕ`.
55+ -- Note that Agda functions are *like* Haskell functions.
56+ -- In Agda, operators can be mixfix (incl. infix, prefix, suffix, self-bracketing and many others).
57+ -- All the `holes` are represented by `_`s. Unlike Haskell, operator names don't need to be put in parentheses.
58+ -- Operators can also be called in the manner of normal functions.
59+ -- e.g. a + b = _+_ a b.
60+ -- Sections are also available, though somehow weird.
61+ -- e.g. a +_ = _+_ a.
62+ _+_ : ℕ → ℕ → ℕ
63+ -- Lhs can also be infix!
64+ -- This is the standard definition in both Peano and Agda stdlib.
65+ -- We do pattern match on the first parameter, it's both convention and for convenience.
66+ -- Agda does a termination check on recursive function.
67+ -- Here the first parameter decreases over evaluation thus it is *well-founded*.
68+ zero + n = n
69+ (suc m) + n = suc (m + n)
70+
71+ -- Here we take a glance at the *dependent type*.
72+ -- In dependent type, we can put values into type level, and vice versa.
73+ -- This is especially useful when we're expecting to make the types more precise.
74+ -- Here `_≡_` is a type that says that two values are *the same*, that is, samely constructed.
75+ _ : 2 + 3 ≡ 5
76+ -- We can do it by ≡-Reasoning, that is writing a (unreasonably long) chain of equations.
77+ _ =
78+ begin
79+ 2 + 3
80+ ≡⟨⟩ -- This operator means the lhs and rhs can be reduced to the same form so that they are equal.
81+ suc (1 + 3)
82+ ≡⟨⟩
83+ suc (suc (0 + 3)) -- Just simulating the function evaluation
84+ ≡⟨⟩
85+ suc (suc 3)
86+ ≡⟨⟩
87+ 5
88+ ∎ -- The *tombstone*, QED.
89+
90+ -- Well actually we can also get this done by simply writing `refl`.
91+ -- `refl` is a proof that says "If two values evaluates to the same form, then they are equal".
92+ -- Since Agda can automatically evaluate the terms for us, this makes sense.
93+ _ : 2 + 3 ≡ 5
94+ _ = refl
95+
96+ -- Multiplication of `ℕ`, defined with addition.
97+ _*_ : ℕ → ℕ → ℕ
98+ -- Here we can notice that in Agda we prefer to indent by *visual blocks* instead by a fixed number of spaces.
99+ zero * n = zero
100+ -- Here the addition is at the front, to be consistent with addition.
101+ (suc m) * n = n + (m * n)
102+
103+ -- EXERCISE `_^_`, Exponentation of `ℕ`.
104+ _^_ : ℕ → ℕ → ℕ
105+ -- We can only pattern match the 2nd argument.
106+ m ^ zero = suc zero
107+ m ^ (suc n) = m * (m ^ n)
108+
109+ -- *Monus* (a wordplay on minus), the non-negative subtraction of `ℕ`.
110+ -- if less than 0 then we get 0.
111+ -- CHAR: \.- → ∸
112+ _∸_ : ℕ → ℕ → ℕ
113+ m ∸ zero = m
114+ zero ∸ suc n = zero
115+ suc m ∸ suc n = m ∸ n
116+
117+ -- Now we define the precedence of the operators, as in Haskell.
118+ infixl 6 _+_ _∸_
119+ infixl 7 _*_
120+
121+ -- These are some more pragmas. Should be self-explaining.
122+ {-# BUILTIN NATPLUS _+_ #-}
123+ {-# BUILTIN NATTIMES _*_ #-}
124+ {-# BUILTIN NATMINUS _∸_ #-}
125+
126+ -- EXERCISE `Bin`. We define a binary representation of natural numbers.
127+ -- Leading `O`s are acceptable.
128+ data Bin : Set where
129+ ⟨⟩ : Bin
130+ _O : Bin → Bin
131+ _I : Bin → Bin
132+
133+ -- Like `suc` for `Bin`.
134+ inc : Bin → Bin
135+ inc ⟨⟩ = ⟨⟩ I
136+ inc (b O) = b I
137+ inc (b I) = (inc b) O
138+
139+ -- `ℕ` to `Bin`. This is a Θ(n) solution and awaits a better Θ(log n) reimpelementation.
140+ to : ℕ → Bin
141+ to zero = ⟨⟩ O
142+ to (suc n) = inc (to n)
143+
144+ -- `Bin` to `ℕ`.
145+ from : Bin → ℕ
146+ from ⟨⟩ = 0
147+ from (b O) = 2 * (from b)
148+ from (b I) = 1 + 2 * (from b)
149+
150+ -- Simple tests from 0 to 4.
151+ _ : from (to 0) ≡ 0
152+ _ = refl
153+
154+ _ : from (to 1) ≡ 1
155+ _ = refl
156+
157+ _ : from (to 2) ≡ 2
158+ _ = refl
159+
160+ _ : from (to 3) ≡ 3
161+ _ = refl
162+
163+ _ : from (to 4) ≡ 4
164+ _ = refl
165+
166+ -- EXERCISE END `Bin`
167+
168+ -- STDLIB: import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)
169+ </ code > </ pre >
0 commit comments