Contents Previous Next

# Other language constructs

```
module Lang.other where
open import Lang.dataStructures renaming (_+_ to _⨦_)
open import Lang.functions using (_+_)
```

## Modules

Modules are used to scope variable and function namespaces such as “packages” in languages like java or python. They behave as closures with the indentation as the indicator of the extent of the closure. Each Agda source file may contain one module at the top level. Modules can be imported as can be seen from the blocks of imports above.

Modules support nesting:

```
module nested where
module X where
x₁ = one
module Y where
x₂ = two
sum = X.x₁ + Y.x₂
```

Importing modules:

```
open nested.X
x₁₁ = x₁ + one
open nested.Y renaming (x₂ to x₃)
x₂ = x₃ + one
```

Modules can have parameters valid inside their closures:

```
module Sort (A : Set)(_≤_ : A → A → Bool) where
insert : A → List A → List A
insert x [] = x :: []
insert x (y :: ys) with x ≤ y
insert x (y :: ys) | true = x :: y :: ys
insert x (y :: ys) | false = y :: insert x ys
sort : List A → List A
sort [] = []
sort (x :: xs) = insert x (sort xs)
```

## Records

Tuples are called as `Record`

s in Agda. Some examples are:

A tuple of `Bool`

and `ℕ`

:

```
record R : Set where
field
r₁ : Bool
r₂ : ℕ
```

A generic tuple:

```
record Pair (A B : Set) : Set where
field
fst : A
snd : B
```

An object of `Pair`

can be constructed as:

```
p23 : Pair ℕ ℕ
p23 = record { fst = two; snd = three }
```

The `constructor`

keyword can be specified to construct records:

```
record Pair' (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
p45 : Pair' ℕ ℕ
p45 = four , five
```

The values of a record can be pattern matched upon:

```
left : Pair' ℕ ℕ → ℕ
left (x , y) = x
```

A record can be parameterized:

```
record List' (A : Set) : Set where
constructor L
field
length : ℕ
vector : Vec A length
list₂ : List' Bool
list₂ = L three vec3
```

All `Data`

definitions have an equivalent `Record`

definition, however `Record`

s are preferred whenever possible as a convention. Records have the obvious advantage of providing `getters`

and `setters`

for free.

## Postulates

`postulate`

s are another Agda language construct. These facilitate defining some type without the actual implementation.

```
postulate
A B : Set
a : A
b : B
_=AB=_ : A → B → Set
a==b : a =AB= b
```

```
data False : Set where
postulate bottom : False
```

Quirks of Syntax