Agda

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

#179on PLDB

17Years Old

2kRepos

Try now: TIO

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

Agda website
Agda Wikipedia page
Agda docs
There are at least 2,120 Agda repos on GitHub
Agda first developed in Chalmers University of Technology
file extensions for Agda include agda and lagda
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

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

Feature	Supported	Token	Example
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

Agda - Programming language

Language features