PLDB
Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon

Idris

Idris

Idris is a pl created in 2014 by Edwin Brady.

#126on PLDB 8Years Old 6.2kUsers
1Books 8Papers 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"
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 ϴ

Books about Idris from ISBNdb

title authors year publisher
Type-Driven Development with Idris Edwin Brady 20170313 Simon & Schuster

Publications about Idris from Semantic Scholar

title authors year citations influentialCitations
IDRIS ---: systems programming meets full dependent types Edwin C. Brady 2011 85 6
Elaborator reflection: extending Idris in Idris D. Christiansen and Edwin C. Brady 2016 31 4
Idris 2: Quantitative Type Theory in Practice Edwin C. Brady 2021 15 0
A Dependently Typed Library for Static Information-Flow Control in Idris Simon Gregersen and Søren Eller Thomsen and Aslan Askarov 2019 4 1
Edit-Time Tactics in Idris Joomy Korkut 2018 3 0
The Idris Programming Language - Implementing Embedded Domain Specific Languages with Dependent Types Edwin C. Brady 2013 3 0
Idris 2: Quantitative Type Theory in Practice (Artifact) Edwin C. Brady 2021 1 0
Building a Blockchain Simulation using the Idris Programming Language Qiutai Pan and X. Koutsoukos 2019 1 0
fish.html · idris.html · applescript.html

View source

PLDB - Build the next great programming language · v2022 · Day 33 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com