Other language constructs

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 Records 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 Records are preferred whenever possible as a convention. Records have the obvious advantage of providing getters and setters for free.

Postulates

postulates 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