Idris

Idris is a programming language created in 2014 by Edwin Brady.

#133on PLDB	9Years Old	6.2kUsers
1Books	8Papers	2kRepos

Try now: Riju · TIO

Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker. Even before its possible usage for interactive theorem-proving, the focus of Idris is on general-purpose programming, like the purely functional Haskell, and with sufficient performance. The type system of Idris is similar to the one used by Agda and theorem-proving in it is similar to Coq, including tactics. Read more on Wikipedia...

Idris website
Idris Wikipedia page
Idris is developed on GitHub and has 3,342 stars
Idris docs
There are at least 1,895 Idris repos on GitHub
Idris first developed in University of St Andrews
file extensions for Idris include idr and lidr
Idris is written in Haskell
Idris on Twitter
The Google BigQuery Public Dataset GitHub snapshot shows 219 users using Idris in 301 repos on GitHub
There are 11 Project Euler users using Idris
Explore Idris snippets on Rosetta Code
Idris appears in the TIOBE Index
Pygments supports syntax highlighting for Idris
GitHub supports syntax highlighting for Idris
Official Blog page for Idris
Frequently Asked Questions for Idris
Indeed.com has 1 matches for "idris developer".
idris-lang.org was registered in 2010
See also: (14 related languages)Agda, Coq, Epigram, Haskell, ML, Rust, Perl, C, JavaScript, Java, JVM, CIL, OCaml, LLVM IR
HTML of this page generated by LanguagePage.ts

Example from Riju:

module Main

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

Example from hello-world:

module Main

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

Example from the Hello World Collection:

Hello world in Idris

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

Example from Linguist:

module Prelude.Char

import Builtins

isUpper : Char -> Bool
isUpper x = x >= 'A' && x <= 'Z'

isLower : Char -> Bool
isLower x = x >= 'a' && x <= 'z'

isAlpha : Char -> Bool
isAlpha x = isUpper x || isLower x

isDigit : Char -> Bool
isDigit x = (x >= '0' && x <= '9')

isAlphaNum : Char -> Bool
isAlphaNum x = isDigit x || isAlpha x

isSpace : Char -> Bool
isSpace x = x == ' '  || x == '\t' || x == '\r' ||
            x == '\n' || x == '\f' || x == '\v' ||
            x == '\xa0'

isNL : Char -> Bool
isNL x = x == '\r' || x == '\n'

toUpper : Char -> Char
toUpper x = if (isLower x)
               then (prim__intToChar (prim__charToInt x - 32))
               else x

toLower : Char -> Char
toLower x = if (isUpper x)
               then (prim__intToChar (prim__charToInt x + 32))
               else x

isHexDigit : Char -> Bool
isHexDigit x = elem (toUpper x) hexChars where
  hexChars : List Char
  hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
              'A', 'B', 'C', 'D', 'E', 'F']

Example from Wikipedia:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Feature	Supported	Token	Example
Integers	✓		-- \d+
Floats	✓		-- \d+[eE][+-]?\d+
Hexadecimals	✓		-- 0[xX][\da-fA-F]+
Strings	✓	"	"Hello world"
Print() Debugging	✓	putStrLn
Comments	✓		-- A comment
Line Comments	✓	--	-- A comment
Dependent types	✓
Semantic Indentation	X

title	authors	year	citations	influentialCitations
IDRIS ---: systems programming meets full dependent types	Edwin C. Brady	2011	85	6
Elaborator reflection: extending Idris in Idris	D. Christiansen and Edwin C. Brady	2016	31	4
Idris 2: Quantitative Type Theory in Practice	Edwin C. Brady	2021	15	0
A Dependently Typed Library for Static Information-Flow Control in Idris	Simon Gregersen and Søren Eller Thomsen and Aslan Askarov	2019	4	1
Edit-Time Tactics in Idris	Joomy Korkut	2018	3	0
The Idris Programming Language - Implementing Embedded Domain Specific Languages with Dependent Types	Edwin C. Brady	2013	3	0
Idris 2: Quantitative Type Theory in Practice (Artifact)	Edwin C. Brady	2021	1	0
Building a Blockchain Simulation using the Idris Programming Language	Qiutai Pan and X. Koutsoukos	2019	1	0

Idris - Programming language

Language features

Books about Idris from ISBNdb

Publications about Idris from Semantic Scholar