Idris 2

Description #

Idris 2 is a modern functional programming language with full dependent types, designed for writing robust, type-safe programs that integrate with low-level code.

History #

Idris was first released by Edwin Brady in 2013 as a general-purpose language with dependent types. Idris 2, its successor, offers improved performance and interoperability, built on a new compiler backend.

Hello World Code #

module Main

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

How to Run #

Option 1: Online
Try Idris 2 Online

Option 2: Local

• Install via package manager or build from source:

brew install idris2

Compile and run:

idris2 --build hello.ipkg
./build/exec/hello

Key Concepts #

• Full dependent types
• Strong static typing with type inference
• Pure functional with side-effect management
• Interactive REPL and compiler
• Interoperability with C and other languages
• Pattern matching and totality checking
• Syntax similar to Haskell
• Type-driven development
• Algebraic data types
• Used in research and advanced type-safe programming

Try It Online #

https://idris2-playground.web.app

Fun Facts #

• Idris 2 allows encoding program correctness within the type system itself.
• The language supports type-driven development, where types guide program construction.
• Idris 2 can generate optimized C code, making it practical for systems programming.

Resources #

Official Site
Docs
GitHub
Community