Pros of Agda

• More mature and established, with a larger community and ecosystem
• Stronger focus on mathematical proofs and theorem proving
• More flexible syntax and notation, allowing for unicode characters

Cons of Agda

• Steeper learning curve, especially for programmers without a strong mathematical background
• Less emphasis on practical programming and general-purpose development
• Slower compilation times compared to Idris 2

Code Comparison

Agda:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

Idris 2:

data Nat : Type where
  Z : Nat
  S : Nat -> Nat

(+) : Nat -> Nat -> Nat
Z + n = n
(S m) + n = S (m + n)

Both Agda and Idris 2 are dependently typed programming languages, but they have different focuses and design philosophies. Agda is more oriented towards mathematical proofs and theorem proving, while Idris 2 aims to be a general-purpose programming language with dependent types. The code comparison shows similar syntax for defining natural numbers and addition, but Agda allows for more flexible notation with unicode characters. Idris 2 generally has a more familiar syntax for programmers coming from other functional languages.

Pros of Coq

• More mature and widely used in academia and industry
• Stronger focus on formal verification and theorem proving
• Larger ecosystem of libraries and tools

Cons of Coq

• Steeper learning curve due to its more complex type system
• Less emphasis on general-purpose programming compared to Idris2
• Syntax can be more verbose and less intuitive for beginners

Code Comparison

Coq example:

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m. induction n as [| n' IHn'].
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite -> IHn'. rewrite -> plus_n_Sm. reflexivity.
Qed.

Idris2 example:

plusCommutative : (n, m : Nat) -> n + m = m + n
plusCommutative Z m = sym (plusZeroRightNeutral m)
plusCommutative (S k) m =
  rewrite plusCommutative k m in
  rewrite plusSuccRightSucc m k in
  Refl

Both examples demonstrate proof of commutativity for addition, but Coq's syntax is more verbose and uses tactics, while Idris2's syntax is more concise and resembles functional programming.

Pros of Lean4

• More advanced metaprogramming capabilities
• Stronger focus on mathematical foundations and formal proofs
• Better performance for large-scale projects

Cons of Lean4

• Steeper learning curve for beginners
• Less extensive standard library compared to Idris2
• Fewer resources and tutorials available for newcomers

Code Comparison

Idris2:

data Vec : Nat -> Type -> Type where
  Nil  : Vec Z a
  (::) : a -> Vec n a -> Vec (S n) a

append : Vec n a -> Vec m a -> Vec (n + m) a
append Nil ys = ys
append (x :: xs) ys = x :: append xs ys

Lean4:

inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)

def append : {n m : Nat} → Vec α n → Vec α m → Vec α (n + m)
  | [], ys => ys
  | (x :: xs), ys => x :: append xs ys

Both examples demonstrate vector concatenation, showcasing similar syntax and dependent types. Lean4's code is slightly more concise, while Idris2's is more explicit in type declarations.

Pros of OCaml

• More mature ecosystem with a larger community and extensive libraries
• Better performance and more efficient memory usage
• Wider industry adoption and proven track record in production environments

Cons of OCaml

• Less expressive type system compared to Idris2's dependent types
• Limited support for theorem proving and formal verification
• Steeper learning curve for beginners due to its unique syntax and concepts

Code Comparison

OCaml:

let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

let result = factorial 5

Idris2:

factorial : Nat -> Nat
factorial 0 = 1
factorial n = n * factorial (n - 1)

result : Nat
result = factorial 5

The code comparison showcases the differences in syntax and type annotations between OCaml and Idris2. OCaml uses a more traditional imperative-style syntax, while Idris2 employs a more declarative approach with pattern matching and explicit type signatures. Idris2's dependent type system allows for more precise type checking and theorem proving capabilities, which are not available in OCaml's simpler type system.

Pros of PureScript

• More mature ecosystem with better JavaScript integration
• Larger community and more extensive library support
• Better tooling and IDE support for web development

Cons of PureScript

• Less powerful type system compared to Idris2's dependent types
• Limited support for theorem proving and formal verification
• Lacks Idris2's elaborator reflection capabilities

Code Comparison

PureScript

module Main where

import Effect.Console (log)

main :: Effect Unit
main = log "Hello, PureScript!"

Idris2

module Main

main : IO ()
main = putStrLn "Hello, Idris2!"

Both examples demonstrate a simple "Hello, World!" program. PureScript uses the Effect monad for side effects, while Idris2 uses the IO monad. PureScript's syntax is more similar to Haskell, whereas Idris2 has some unique features due to its dependent type system.

PureScript is generally more focused on practical web development, with better JavaScript interoperability. Idris2, on the other hand, is more oriented towards research, theorem proving, and exploring advanced type system features. The choice between the two depends on the specific project requirements and the developer's preferences for type system power versus ecosystem maturity.