Skip to content

Basic Types

This module establishes the foundational type-theoretic constructs used throughout different entries in this website.

{-# OPTIONS --without-K --type-in-type --exact-split #-}
module Foundation.BasicTypes where

open import Agda.Primitive using (Level; lsuc)

Product Types

The product type represents pairs of values, fundamental for modeling object state that consists of multiple components.

Product type for pairing values:

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

infixr 4 _×_
infixr 4 _,_

Projection functions:

fst : {A B : Set} → A × B → A
fst (a , b) = a

snd : {A B : Set} → A × B → B
snd (a , b) = b

Dependent pair type (Σ type):

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,Σ_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

Alternative notation for Σ interpreted as existential quantification:

∃ : {ℓ : Level} {A : Set ℓ} → (A → Set ℓ) → Set ℓ
∃ {ℓ} {A} P = Σ A P

∃-syntax : {ℓ : Level} (A : Set ℓ) → (A → Set ℓ) → Set ℓ
∃-syntax A P = Σ A P

syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B

Coproduct Types

Coproduct or Sum types model choice and alternatives, essential for representing different message types and object states in the AVM.

Coproduct type for alternatives:

data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

infixr 3 _+_

Case analysis for sum types:

case_of_ : {A B C : Set} → A + B → (A → C) → (B → C) → C
case (inl a) of f = λ g → f a
case (inr b) of f = λ g → g b

Unit and Empty Types

The unit type represents trivial computations, while the empty type represents impossible situations.

Unit type - exactly one value:

record ⊤ : Set where
  constructor tt
{-# BUILTIN UNIT ⊤ #-}

Empty type - no values:

data ⊥ : Set where

Elimination principle for the empty type:

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

Negation:

¬ : Set → Set
¬ A = A → ⊥

Boolean Type

Boolean type or the two-element type is a fundamental type in type theory. It is used to represent truth values.

Two-element type:

data Bool : Set where
  true  : Bool
  false : Bool
{-# BUILTIN BOOL Bool #-}

Operations on the two-element type:

not : Bool → Bool
not true = false
not false = true

_∧_ : Bool → Bool → Bool
true  ∧ true  = true
true  ∧ false = false
false ∧ true  = false
false ∧ false = false

_∨_ : Bool → Bool → Bool
false ∨ false = false
false ∨ true  = true
true  ∨ false = true
true  ∨ true  = true

infixr 6 _∧_
infixr 5 _∨_

If-then-else syntax for boolean conditionals:

if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

Equality and Decidability

Propositional equality is fundamental for reasoning about object identity and state equivalence.

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

infix 10 _≡_

Symmetry:

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

Transitivity:

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

Congruence:

cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

Negated Equality - Used extensively in well-formedness conditions to express "is defined":

_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬ (x ≡ y)

infix 4 _≢_

Decidability type for propositions that can be algorithmically decided:

data Dec (A : Set) : Set where
  yes : A → Dec A
  no  : (¬ A) → Dec A

Equational Reasoning

Equational reasoning combinators provide a readable syntax for chaining equality proofs:

infix  1 begin_
infixr 2 _≡⟨⟩_ _≡⟨_⟩_
infix  3 _∎

begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin p = p

_≡⟨⟩_ : {A : Set} (x : A) {y : A} → x ≡ y → x ≡ y
x ≡⟨⟩ p = p

_≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = trans p q

_∎ : {A : Set} (x : A) → x ≡ x
x ∎ = refl

Option Types

Option types or Maybe types handle partial operations and potential failures, crucial for modeling object operations that may not always succeed. Also, useful for modeling partial functions.

Maybe type for partial operations:

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A
{-# BUILTIN MAYBE Maybe #-}

The value just is better than nothing:

just≢nothing : ∀ {A} {x : A} → just x ≡ nothing → ⊥
just≢nothing ()

just-injective : ∀ {A} {x y : A} → just x ≡ just y → x ≡ y
just-injective refl = refl

Bind operation for Maybe:

_>>=ᴹ_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
nothing >>=ᴹ f = nothing
(just x) >>=ᴹ f = f x

Map operation:

map-maybe : {A B : Set} → (A → B) → Maybe A → Maybe B
map-maybe f nothing = nothing
map-maybe f (just x) = just (f x)

Natural Numbers

Natural numbers are essential for modeling object identifiers, message sequences, and temporal ordering.

Natural numbers:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

Basic arithmetic:

_+ℕ_ : ℕ → ℕ → ℕ
zero +ℕ n = n
(suc m) +ℕ n = suc (m +ℕ n)

_*ℕ_ : ℕ → ℕ → ℕ
zero *ℕ n = zero
(suc m) *ℕ n = n +ℕ (m *ℕ n)

infixl 6 _+ℕ_
infixl 7 _*ℕ_

Natural number comparison:

_≥_ : ℕ → ℕ → Set
zero ≥ zero = ⊤
zero ≥ suc m = ⊥
suc n ≥ zero = ⊤
suc n ≥ suc m = n ≥ m

_≤_ : ℕ → ℕ → Set
n ≤ m = m ≥ n

infix 4 _≥_
infix 4 _≤_

Boolean comparison for natural numbers:

_≤?_ : ℕ → ℕ → Bool
zero ≤? _ = true
(suc m) ≤? zero = false
(suc m) ≤? (suc n) = m ≤? n

_<?_ : ℕ → ℕ → Bool
_ <? zero = false
zero <? (suc _) = true
(suc m) <? (suc n) = m <? n

infix 4 _≤?_
infix 4 _<?_

Decidable equality for natural numbers:

_≟ℕ_ : (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 m≢n = no λ { refl → m≢n refl }

infix 4 _≟ℕ_

Lists

Lists model sequences of messages, object histories, and collections of identifiers.

Lists:

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A
{-# BUILTIN LIST List #-}

infixr 5 _∷_

List operations:

length : {A : Set} → List A → ℕ
length [] = zero
length (x ∷ xs) = suc (length xs)

_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

infixr 5 _++_

List concatenation is associative:

++-assoc : ∀ {A} (xs ys zs : List A) → ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs))
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (λ l → x ∷ l) (++-assoc xs ys zs)

Right identity for concatenation:

++-right-id : ∀ {A} (xs : List A) → (xs ++ []) ≡ xs
++-right-id [] = refl
++-right-id (x ∷ xs) = cong (λ l → x ∷ l) (++-right-id xs)

Map function:

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

Fold right:

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr f z [] = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

Finite Sets

Finite sets model collections of object identifiers and principal names.

Finite sets using lists (naive implementation):

FinSet : Set → Set
FinSet A = List A

Membership predicate:

data _∈_ {A : Set} (x : A) : List A → Set where
  here  : {xs : List A} → x ∈ (x ∷ xs)
  there : {y : A} {xs : List A} → x ∈ xs → x ∈ (y ∷ xs)

infix 4 _∈_

Strings and Identifiers

Abstract string type (postulated for simplicity):

postulate String : Set
{-# BUILTIN STRING String #-}

postulate
   _≟-string_ : (s₁ s₂ : String) → Maybe (s₁ ≡ s₂)
   nat-to-string : ℕ → String
   string-to-nat : String → ℕ
   _++ˢ_ : String → String → String

infixr 5 _++ˢ_

Object identifiers for interaction trees and AVM:

postulate ObjectId : Set

Predicates and Set Relations

Predicates model properties of elements. A predicate on type A is a function A → Set.

Pred : {ℓ : Level} → Set ℓ → Set (lsuc ℓ)
Pred {ℓ} A = A → Set ℓ

Membership for predicates (not lists):

_∈Pred_ : {ℓ : Level} {A : Set ℓ} → A → Pred A → Set ℓ
x ∈Pred P = P x

infix 4 _∈Pred_

Subset relation between predicates:

_⊆_ : {ℓ : Level} {A : Set ℓ} → Pred {ℓ} A → Pred {ℓ} A → Set (lsuc ℓ)
P ⊆ Q = ∀ {x} → P x → Q x

infix 4 _⊆_

Logical Connectives

Logical equivalence (bi-implication):

record _↔_ (A B : Set) : Set where
  constructor mk↔
  field
    to   : A → B
    from : B → A

open _↔_ public

infix 3 _↔_

Misc

Function composition:

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(g ∘ h) x = g (h x)

Monad Interface

For supporting Agda's do-notation, we define a simple monad record:

record RawMonad (M : Set → Set) : Set₁ where
  field
    return : {A : Set} → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B

  _>>_ : {A B : Set} → M A → M B → M B
  m₁ >> m₂ = m₁ >>= λ _ → m₂
Module References

Referenced By

This module is referenced by:

?>