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.
• Each file should have module name same as file like in haskell.
• Type names should start with upper-case letter.
• Dotted expression
• No step-by-step evaluation as in Coq.
• The public in open import Universes public allows other module importing this module to access what's imported here
  • Kind of like Export Require Import in Coq

• Records need to be opened before they can be used
• Open publicly so that other module importing this module can also use it.
• Anonymous lambda syntax: λ x -> body

• Mixfix notations
  • Needs space between symbols. There's no way getting around that apparently..
  • https://stackoverflow.com/questions/42725948/get-around-whitespace-requirement-for-mixfix-operators-in-agda
  • 3 * 4 is fine, but 3*4 isn't.
• '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.
• Set in Agda is like Type in Coq
  • This is commonly used as an alias: Type = Set
  • https://proofassistants.stackexchange.com/questions/4189/why-does-agda-use-set-instead-of-type
• Identifiers:
  • These characters cannot be part of an identifier: .;{}()@"
  • https://agda.readthedocs.io/en/latest/language/lexical-structure.html#keywords-and-special-symbols
  • Also, _|_ can't be used because it is used for with
• agda seems to have tools to convert agda to haskell, but not much used and hence not too mature.
  • https://agda.readthedocs.io/en/v2.5.2/tools/compilers.html
• --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
• Anonymous functions: \ x -> x

Imports needed

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

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)

Kinds

• Setω: Like type of types
• (n : Level) → Set n is a type, but it doesn't have a type without Setω.
• https://agda.readthedocs.io/en/v2.6.0/language/universe-levels.html#expressions-of-kind-set

Cubical

• Needs {-# OPTIONS --cubical #-}
• --without-k disables Streicher's axiom (aka Axiom K), "which we don't want for univalent mathematics"
  • Makes it constructive-only ??
• A library that needs to be installed separately
  • https://github.com/agda/cubical
• Installation needed export LC_ALL=C.UTF-8 (locale found with locale -a) beforehand.
  • C in C.UTF-8 stands for computer

DBT: Why the 'cubical' in cubical type theory?

postulate
  PathP : ∀ {ℓ} (A : I -> Set ℓ) -> A i0 -> A i1 -> Set ℓ

Standard library

-- ~/.agda/libraries
--
-- (old one. nix channel 24.05)
-- /nix/store/dhyjk470gy6l53zrcf72jg5n390h028z-standard-library-2.0/standard-library.agda-lib
--
-- (nix channel 24.11)
/nix/store/1wfcxqkrqsy17ads3j1c3x42cgz6b04m-standard-library-2.1.1/standard-library.agda-lib

open import Data.Bool
open import Data.Nat

b : Bool
b = Data.Nat._<ᵇ_ 1 2

'Extraction'

https://agda.readthedocs.io/en/latest/language/foreign-function-interface.html

• 'Extraction' to haskell and javascript possible by default.
• Compile with agda --compile input.agda
  • Output Haskell source will be in a separate directory, but built executable will be at same level as input agda file.
• Compile to javascript with: agda --js input.agda
• Looks like work is also being done to have a rust backend…
  • https://github.com/omelkonian/agda2rust

—

• For functions: {-# COMPILE GHC <Name> as <HaskellName> #-}
• Useful for agda postulates: {-# COMPILE GHC <Name> = type <HaskellType> #-}
  • ie, for opaque types
• For types: {-# COMPILE GHC <Name> = data <HaskellData> (<HsCon1> | .. | <HsConN>) #-}
  • Provide a mapping from agda type to haskell type along with that of their constructors.
  • Eg: {-# COMPILE GHC Unit = data () (()) #-}
• For simple textual replacement: {-# COMPILE GHC <Name> = <HaskellCode> #-}
  • Eg: {-# COMPILE GHC putStr = type Data.Text.IO.putStr #-}
• Expose agda definition to haskell code
  • {-# COMPILE GHC agdaName as agdaNameInHaskell #-}
• For javascript extraction, we use JS instead of GHC.
• Inline haskell: {-# FOREIGN GHC import Text.Parsec #-}
  • https://agda.readthedocs.io/en/latest/language/foreign-function-interface.html#the-foreign-pragma

A complete example (modified from the one at an older version of docs):

module HelloWorld where

{-# FOREIGN GHC import Data.Text.IO #-}

data Unit : Set where
  unit : Unit

{-# COMPILE GHC Unit = data () (()) #-}

postulate
  String : Set

{-# BUILTIN STRING String #-}

postulate
  IO : Set → Set

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}

postulate
  putStr : String → IO Unit

{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}

main : IO Unit
main = putStr "Hello, World!"

—

Compiled Haskell will be in a directory named MAlonzo/:

• MAlonzo is apparently another name for GHC back-end of agda
  • Stands for Modified Alonzo
• https://wiki.portal.chalmers.se/agda/Docs/MAlonzo
• https://www.reddit.com/r/agda/comments/46dwg7/malonzo/
• I guess this is the original Alonzo: https://www.mimuw.edu.pl/~ben/Papers/TYPES07-alonzo.pdf
  • 'Haskell programs are close to Curry style lambda-calculus. On the other hand, Agda programs are closer to Church style'

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 like 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

https://wiki.portal.chalmers.se/agda/Main/AgdaVsCoq

False type:

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

Following comparison is probably a bit too approximative…

Coq-like notations

Other than mixfix operators, syntax declarations can help.

—

• Syntax declarations must be linear. ie, each argument can be used exactly once.

syntax wrong x = x + x

-- Eg.agda:16,22: Malformed syntax declaration: syntax must use holes exactly once
-- x<ERROR>

syntax wrong x = id
-- Eg.agda:16,18: Malformed syntax declaration: syntax must use holes exactly once
-- id<ERROR>

• Syntax declarations cannot have holes.

syntax #_ f = Atom f

-- Eg.agda:17,20: Syntax declarations are allowed only for simple names (without holes)
-- f<ERROR>

—

For example, a unary operator in agda-unimathˡ:

infix 25 ¬_

¬_ : {l : Level} → UU l → UU l
¬ A = A → empty

See:

• An example: https://unimath.github.io/agda-unimath/MIXFIX-OPERATORS.html

Precedence

Lower precedence value => higher precedence (like in Coq)

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

Associativity of mixfix operators can be definied with one of the above three.

Erasure

https://agda.readthedocs.io/en/v2.6.3/language/runtime-irrelevance.html

• Needs --erasure option

• Syntax: @0

Haskell-like type alias

Just make it like a normal definition.

open import Data.Nat using (ℕ)
open import Data.Vec

BMatrix2D : ℕ -> ℕ -> Set
BMatrix2D r c = Vec (Vec Bool c) r

'Type class instance'

Type classes are just records.

• https://agda.readthedocs.io/en/latest/language/instance-arguments.html#declaring-instances

open import Data.List using (List; []; _++_)

record Monoid (A : Set) : Set where
  field
    mempty : A 
    _<>_ : A -> A -> A

-- Make mempty and _<>_ available
open Monoid {{...}} public

instance
  ListMonoid : {A : Set} -> Monoid (List A)
  ListMonoid =
    record {
      mempty = [];
      _<>_ = _++_
    }

• private instance: limit the scope of instance to current module

Rewriting

• Similar to automatic rewrites of Coq
  • Adds some definitions as rules that are automatically?? used for rewrites.
• Needs {-# OPTIONS --rewriting #-}
• Done via REWRITE pragma.
  • Eg: {-# REWRITE +zero +suc #-}

See:

• https://agda.readthedocs.io/en/latest/language/rewriting.html
• https://jesper.sikanda.be/posts/hack-your-type-theory.html

Emacs

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

• C-c C-c: Case split

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

  • C-u C-u C-c C-,: Show goal info after normalization
  • C-u C-u C-u C-c C-,: Show goal info in weak-head normal form

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

• C-c C-l: Type check buffer

  • Write an ? and do C-c C-l to insert a hole

• C-c C-r: Refine

  • Can be used to introduce a lambda abstraction if it's obvious from the type.

• 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

—

• {!!} can be used to place a hole manually
• Demand to fill a hole with an expression using C-c C-SPC

—

• 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

• Show environment (while cursor is on a hole): C-c C-e
• C-c C-,: Show goal and context
• C-c C-t: Show goal

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

Misc

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

Doubts

• Finite types
• String, Char
• Coinduction
• Are there notation scopes in agda?
• How to perform compilation/extraction of unary Nat to Haskell Int?
• recursive notations like in coq
• override implicit argument in agda
  • https://agda.readthedocs.io/en/latest/language/implicit-arguments.html
• scoped inline type annotation in agda

Resources

• CS410: Advanced Functional Programming at University of Strathclyde
  • (2015 edition)
  • (2022 edition)
• https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html
• Functional programming course at TU Delft
  • https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf