Questions Concepts
GitHub icon

Idris

Idris - Programming language

< >

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

Source code:
git clone https://github.com/idris-lang/Idris-dev
#129on PLDB 9Years 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...


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

View source

- Build the next great programming language · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Queries · Stats · Sponsor · Traffic · Traffic Today · Day 305 · feedback@pldb.com · Logout