Agda

General

• Absurd pattern: () (kinda like False in Coq)

  • https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#absurd-patterns

• tt: not exactly unit type as in Coq. It's like the I constructor (of True type) in Coq.

• postulate: like Axiom in Coq

• Each file should have module name.

• Type names should start with upper-case letter.

• Dotted expression

• No step-by-step evaluation as in Coq.

• Mixfix notations

• 'Function' associates to right

  • A -> B -> C is A -> (B -> C)

• Looks like space is needed before : in type annotations

  • zero: ℕ and zero :ℕ give parse error, zero : ℕ doesn't.

• --without-K and --safe seems like not-so-good-to-use flags.

  • --safe option 'to avoid possible misuses of certain features which could lead to logical inconsistencies' ʳ

• --cubical: implements a computational interpretation of HoTT.

  • Supports univalence.

• UIP: Uniqueness of identity proofs

• Axiom K: Equivalent to UIP ??

• Setoid: Set equipped with an equivalence relation

• Extensional vs intentional type theory

• postulate: like Axiom in Coq

  • Signature without definition
  • https://agda.readthedocs.io/en/v2.6.20240714/language/postulates.html

Imports needed

• List: open import Data.List using ([]; [_]; _++_; List; sum)
• Nat: open import Data.Nat using (ℕ; _+_)

Mutually recursive types

• Use mutual keyword

Example from here:

mutual
  data ty-ctx : Set where
    ε    : ty-ctx
    _,-_ : (Δ : ty-ctx) → defn Δ → ty-ctx

  data defn : ty-ctx → Set where
    synonym : ∀ {Δ} → ty Δ → defn Δ
    newtype : ∀ {Δ} → ty Δ → defn Δ

  data ty : ty-ctx → Set where
    wk    : ∀ {Δ τ} → ty Δ → ty (Δ ,- τ)
    defd  : ∀ {Δ τ} → ty (Δ ,- τ)
    bit   : ∀ {Δ}   → ty Δ
    _⇒_  : ∀ {Δ}   → ty Δ → ty Δ → ty Δ

Record type

https://agda.readthedocs.io/en/latest/language/record-types.html

• Access field of a record by with .fieldname

record RecName : Set where
  field
    a : ℕ
    b : 𝔹

—

'Open' a record to bring their field names into default scope.

• Because by default, a module of the same name is also defined.

open RecName

Example from docs:

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

geta : Pair A B

Levels

• Type: Level
  • lzero: Level: lowest level
  • lsuc: Level -> Level: Next level
  • _⊔_: Level -> Level -> Level: Least upper bound of 2 levels
• Set: Like Type in Coq
  • Set: Set0
  • Set₁: Set ∈ Set₁ ??
  • Set₂: Set₁ ∈ Set₂ ??
• 0ℓ: Level zero
  • https://agda.github.io/agda-stdlib/master/Level.html#521

Example from docs:

data _×_ {n m : Level} (A : Set n) (B : Set m) : Set (n ⊔ m) where
   _,_ : A → B → A × B

Example import:

• open import Level using (0ℓ) renaming (suc to lsuc)

Standard library

Standard library need to be installed separately.

• https://agda.readthedocs.io/en/latest/tools/package-system.html
• https://github.com/NixOS/nixpkgs/blob/master/doc/languages-frameworks/agda.section.md

—

• ~/.agda/defaults: list of agda libraries loaded by default
  • All these library names must be mentioned in ~/.agda/libraries
• ~/.agda/libraries: list of paths complete paths to agda-lib files of packages (including the agda-lib file name with extension)
• Default AGDA_DIR in unix: ~/.agda

Pragmas

Special comments.

Example:

{-# BUILTIN NATURAL ℕ #-}

agda

associates numbers with elements of the ℕ type. So 2 would implicitly mean suc (suc zero).

See: https://plfa.github.io/Naturals/#a-pragma

—

• {-# BUILTIN NATURAL ℕ #-}
  • Informs agda that ℕ corresponds to natural numbers
  • Allows to use numbers instead of constructors (eg: 0 instead of zero)
  • Internally allows use of haskell Int (log₂ space) instead of unary nat.
• {-# OPTIONS --exact-split #-}
  • Don't allow case overlaps

Space matters: a : Set vs a: Set

The space matters. Looks if we do a: Set, a: will be considered a name.

For example, this works:

data Type : Set where
  Nat : Type

But this doesn't:

data Type: Set where
  Nat : Type
{-
Missing type signature for data definition Type:
when scope checking the declaration
  data Type: Set where
    Nat : Type
 -}

Coq vs agda

False type:

• Agda: data 𝟘 : Type where
• Coq: Inductive False : Prop :=.

Following comparison is probably a bit too approximative…

Precedence

Lower precedence value => higher precedence

• infixl: left associativity
• infixr: right associativity
• infix: no associativity (parenthesis always needed)

Emacs

• C-c C-w: Show definition of a name

• C-c C-c: Case split

• C-c C-,: Show current goal info

• C-c C-Space: Finish hole after filling it

• C-c C-l: Type check buffer

• Right click on a typechecked part to go to its definiton

• Find type of an expression: C-c C-d

• Evaluate (find normal form) of an expression: C-c C-n

—

• Move to next goal: C-c C-f
• Move to previous goal: C-c C-b
• Evaluate a term in current scope: C-c C-n
• Infer type of an expression that you give: C-c C-d
• Quit agda: C-c C-x C-q

• Hide/unhide hidden args: C-c C-x C-i
• Kill agda: C-c C-x C-q
• Kill and restart agda: C-c C-x C-r

https://agda.readthedocs.io/en/latest/tools/emacs-mode.html#keybindings

Todo

• Find type of name under cursor
• Find definition of name under cursor

Unicode

• : ℕ
• \) then use C-n to choose from options: ⟩

—

• M-x agda-input-show-translations: Show latex codes for unicode symbols
• Show how to input a unicode character already in a buffer: M-x quail-show-key

Misc

• Papers using agda: https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.PapersUsingAgda