Top 1K Features Creators Events Podcasts Books Extensions Interviews Blog Explorer CSV

Idris

< >

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


Example from Riju:
module Main main : IO () main = putStrLn "Hello, world!"
Example from hello-world:
module Main main : IO () main = putStrLn "Hello World"
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
View source
- Build the next great programming language · Add · About · Search · Keywords · Livestreams · Labs · Resources · Acknowledgements · Part of the World Wide Scroll