Idris

Description #

Idris is a general-purpose functional programming language with dependent types, allowing types to be predicated on values. It supports interactive theorem proving, precise type-driven development, and has Haskell-like syntax with additional compile-time safety.

History #

Idris was created by Edwin Brady and first released in 2007. Its design draws inspiration from Haskell and Coq, with the goal of bringing dependent types to general-purpose programming. Idris 2, written in Idris itself, was released in 2021.

Hello World Code #

module Main

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

How to Run #

Option 1: Online

• Try Idris (Replit) (for Idris 1 only)

Option 2: Local

1. Install Idris (v1 or v2):

brew install idris  # macOS
sudo apt install idris  # Linux

Save code as Main.idr and run:

idris Main.idr -o main
./main

Key Concepts

1. Dependent types
2. Pure functional programming
3. Interactive theorem proving
4. Type-driven development
5. Totality checking
6. Lazy evaluation
7. Pattern matching
8. First-class types
9. IO monad
10. Meta-programming and reflection

Try It Online #

• Replit – Idris (Note: Idris 2 may not be available online yet)

Fun Facts #

• Idris allows you to encode program correctness directly in types.
• Idris 2 is self-hosted—written in Idris itself.
• It’s commonly compared with Agda and Coq in type theory circles.

Resources #

Type-driven Development with Idris (Book)

Idris Official Site

Idris GitHub Repository

Idris 2 (new version)