Idris

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

Source code:

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

#128on PLDB

10Years Old

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

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

Idris - Programming language

Language features