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?

Conventions

Agda	Cubical
Set	Type
Setω	Typeω
lzero	ℓ-zero
lsuc	ℓ-suc
⊔	ℓ-max

From Cubical/Core/Primitives.agda.

Interval type (`I`)

I : IUniv, where IUniv is a special sort (used to be Setω in earlier versions of cubical ??)
- We cannot pattern match on I values
- Kind of like how we can't pattern match on functions
- A special type. Only type for which transport operation isn't there ??
i : I is indicative of i ∈ [0.0, 1.0]
- Where 0.0 (i0) and 1.0 (i1) are the end points of the interval
neg i: symmetry
- 'reflection'?? of i in [0.0, 1.0]
- Like taking 1.0 - x for a given x.
- This is cubical agda specific ?? Not really necessary ??

Definition	Notation
`min ia ib`	`ia ∧ ib`
`max ia ib`	`ia ∨ ib`
`neg i`	`~i`

Path type

Path over a type A is represented with a function of type I -> A
Path A a b: Type of paths between a and b
- where A : Type, a b : A

Equality x ≡ y 'consists of a path p : I -> A such that p i0 == x and p i1 == y.

where == is definitional equality

PathP is the primitive notion, not Path (_≡_)

Defined as a postulate.

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

Resources

https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/ (Doesn't use cubical, but builds something similar from scratch)
https://nextjournal.com/agdacubicold/intro

Standard library

Installation

WARNING!: Each agda version will work with only a specific version of standard-library.

Example: agda 2.7.0 works with standard-library 2.1.1

Standard library need to be installed separately.

—

~/.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

-- ~/.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

Bool

_<ᵇ_: a boolean function
_<_: in 'prop-world'

open import Data.Bool
open import Data.Nat

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

Misc

Empty type: https://agda.github.io/agda-stdlib/v2.1/Data.Empty.html

'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	Agda
False	⊥	Empty type
unit	⊤	Unit type
tt	tt	Value of unit type
Type	Set
Axiom	postulate

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:

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

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

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

General

Imports needed

Mutually recursive types

Record type

Levels

Cubical

Conventions

Interval type (I)

Path type

Resources

Standard library

Installation

Bool

Misc

'Extraction'

Pragmas

Space matters: a : Set vs a: Set

Coq vs agda

Coq-like notations

Precedence

Erasure

Haskell-like type alias

'Type class instance'

Rewriting

Emacs

Todo

Unicode

Misc

Doubts

Resources

Interval type (`I`)

Space matters: `a : Set` vs `a: Set`