Top Related Projects
Agda is a dependently typed programming language / interactive theorem prover.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Lean 4 programming language and theorem prover
The core OCaml system: compilers, runtime system, base libraries
A strongly-typed language that compiles to JavaScript
Quick Overview
Idris2 is a purely functional programming language with dependent types. It is a successor to Idris, designed to be more performant and to address some of the shortcomings of its predecessor. Idris2 aims to support theorem proving and general-purpose programming with a focus on correctness and expressiveness.
Pros
- Strong static typing with dependent types, allowing for more precise and expressive code
- Powerful type inference, reducing the need for explicit type annotations
- Totality checking, ensuring functions always terminate
- Efficient compilation through Chez Scheme backend
Cons
- Steep learning curve, especially for programmers not familiar with dependent types
- Smaller ecosystem and community compared to more mainstream languages
- Limited tooling and IDE support
- Performance may not be on par with lower-level languages for certain tasks
Code Examples
- Hello World example:
main : IO ()
main = putStrLn "Hello, World!"
- Defining a vector with a fixed length:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
-- Example usage
myVect : Vect 3 Int
myVect = 1 :: 2 :: 3 :: Nil
- Proving a simple theorem:
plusZeroRight : (n : Nat) -> n + 0 = n
plusZeroRight Z = Refl
plusZeroRight (S k) = cong S (plusZeroRight k)
Getting Started
-
Install Idris2:
- On macOS:
brew install idris2
- On Ubuntu:
sudo apt-get install idris2
- Or build from source: Clone the repository and follow the build instructions in the README.
- On macOS:
-
Create a new Idris file (e.g.,
hello.idr
):
main : IO ()
main = putStrLn "Hello, Idris2!"
- Compile and run:
idris2 hello.idr -o hello
./build/exec/hello
This will output: "Hello, Idris2!"
Competitor Comparisons
Agda is a dependently typed programming language / interactive theorem prover.
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.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Pros of Rocq
- Specialized for formal verification and proof checking
- Integrates with the Coq proof assistant ecosystem
- Focuses on mathematical rigor and correctness proofs
Cons of Rocq
- Narrower scope and application domain than Idris2
- Steeper learning curve for non-mathematicians
- Less extensive general-purpose programming features
Code Comparison
Rocq (proof-oriented):
Theorem add_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m. induction n as [| n' IHn'].
- simpl. rewrite -> add_0_r. reflexivity.
- simpl. rewrite -> IHn'. rewrite -> add_succ_r. reflexivity.
Qed.
Idris2 (general-purpose with dependent types):
addComm : (n, m : Nat) -> n + m = m + n
addComm Z m = rewrite plusZeroRightNeutral m in Refl
addComm (S k) m = rewrite addComm k m in
rewrite plusSuccRightSucc m k in Refl
While both examples demonstrate theorem proving capabilities, Rocq's syntax is more focused on formal proofs, whereas Idris2 integrates proofs with general-purpose programming constructs. Idris2 offers a broader range of features for software development, while Rocq specializes in mathematical verification.
Lean 4 programming language and theorem prover
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.
The core OCaml system: compilers, runtime system, base libraries
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.
A strongly-typed language that compiles to JavaScript
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.
Convert
designs to code with AI
Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.
Try Visual CopilotREADME
Idris 2
Idris 2 is a purely functional programming language with first class types.
For installation instructions, see INSTALL.md.
The wiki lists a number of useful resources, in particular
- What's changed since Idris 1
- Resources for learning Idris, including official talks that showcase its capabilities
- Editor support
Things still missing
- Cumulativity (currently
Type : Type
. Bear that in mind when you think you've proved something) rewrite
doesn't yet work on dependent types
Contributions wanted
If you want to learn more about Idris, contributing to the compiler could be one way to do so. The contribution guidelines outline the process. Having read that, choose a good first issue or have a look at the contributions wanted for something more involved. This map should help you find your way around the source code. See the wiki page for more details.
Top Related Projects
Agda is a dependently typed programming language / interactive theorem prover.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Lean 4 programming language and theorem prover
The core OCaml system: compilers, runtime system, base libraries
A strongly-typed language that compiles to JavaScript
Convert
designs to code with AI
Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.
Try Visual Copilot