Idris - Programming language

Idris is an open source programming language created in 2014 by Edwin Brady.

#84on PLDB

10Years Old

2kRepos

Download source code:

git clone https://github.com/idris-lang/Idris-dev

Homepage · REPL · Try It Online · Source Code · Blog · Wikipedia · Twitter · FAQ · Docs

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...

Tags: programming language
Idris is developed on GitHub and has 3,418 stars
There are at least 1,895 Idris repos on GitHub
Early development of Idris happened in University of St Andrews
Idris is written in Idris, Bourne shell, Haskell, reStructuredText, SVG, C, Make, Markdown, YAML, JavaScript, Perl, XML, CSS, Nix, Python, CMake, Scheme, Bash, Java
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
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
3 PLDB concepts link to Idris: cloc, Idris, Pygments

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

Language features

Feature	Supported	Example	Token
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