Idris

Idris is a purely-functional programming language with dependent types, quantity annotations, optional lazy evaluation, and features such as a totality checker. Idris is designed to be a general-purpose programming language similar to Haskell, but may also be used as a proof assistant. Wikipedia

Created Year: 2007
Implemented in: Haskell
File extensions: idr, lidr

Wikidata: Q15408477

Influenced by: Agda • Clean • Epigram • Haskell • Rocq prover

Programming paradigms: functional programming • purely functional programming • total functional programming

Language types: dependently typed programming language • purely functional programming language

➡️ Influence Network Poster

➡️ Hack the Planet

Idris Influence Network

Pan and zoom the graph with your mouse or alternatively your fingers on touch devices.

Hello World in Idris

module Main

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

Source: github.com/leachim6/hello-world

Search on GitHub

ℹ️ Click on a column heading to sort the results.
Name	Description	Last pushed to	Open issues	Forks	Stars	Size

Latest data update: 2025-10-20