Agda - Programming language

Agda is an open source programming language created in 2007 by Ulf Norell and Catarina Coquand.

#250on PLDB

17Years Old

2kRepos

Homepage · REPL · Try It Online · Wikipedia · Docs

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. Read more on Wikipedia...

Tags: programming language
There are at least 2,120 Agda repos on GitHub
Early development of Agda happened in Chalmers University of Technology
The Google BigQuery Public Dataset GitHub snapshot shows 143 users using Agda in 207 repos on GitHub
Explore Agda snippets on Rosetta Code
Agda on HOPL
Pygments supports syntax highlighting for Agda
GitHub supports syntax highlighting for Agda
See also: (7 related languages) Coq, Epigram, Haskell, Idris, Emacs, Unicode, JavaScript
4 PLDB concepts link to Agda: cloc, datafun, Obsidian, Pygments

Example from hello-world:

module agda where
open import IO

main = run (putStrLn "Hello World")

Example from Linguist:

module NatCat where

open import Relation.Binary.PropositionalEquality

-- If you can show that a relation only ever has one inhabitant
-- you get the category laws for free
module
  EasyCategory
  (obj : Set)
  (_⟶_ : obj → obj → Set)
  (_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z)
  (id : ∀ x → x ⟶ x)
  (single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s)
  where

  idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r
  idʳ x y r = single-inhabitant x y (r ∘ id y) r

  idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r
  idˡ x y r = single-inhabitant x y (id x ∘ r) r

  ∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t)
  ∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t))

open import Data.Nat

same : (x y : ℕ) (r s : x ≤ y) → r ≡ s
same .0 y z≤n z≤n = refl
same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s)

≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
≤-trans .0 y z z≤n s = z≤n
≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s)

≤-refl : ∀ x → x ≤ x
≤-refl zero = z≤n
≤-refl (suc x) = s≤s (≤-refl x)

module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same

Example from Wikipedia:

data _≤_ : ℕ → ℕ → Set where
   z≤n : {n : ℕ} → zero ≤ n
   s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

Language features

Feature	Supported	Example	Token
MultiLine Comments	✓
Integers	✓	-- \d+
Floats	✓	-- \d+[eE][+-]?\d+
Hexadecimals	✓	-- 0[xX][\da-fA-F]+
Strings	✓	"Hello world"	"
Print() Debugging	✓		putStrLn
Comments	✓	-- A comment
Line Comments	✓	-- A comment	--
Typed Holes	✓
Semantic Indentation	X