Idris is an actively used programming language created in 2014. 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 ranks in the top 5% of languages
- the Idris website
- the Idris wikipedia page
- Idris on github
- Idris first appeared in 2014
- Idris was created by Edwin Brady
- file extensions for Idris include idr and lidr
- tryitonline has an online Idris repl
- Have a question about Idris not answered here? Email me and let me know how I can help.
Example code from the Hello World Collection:
Hello world in Idris > main : IO () > main = putStrLn "Hello, World!"
Example code 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 code 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
Last updated August 9th, 2020