Idris is a purely functional programming language featuring dependent types, optional lazy evaluation, and a broad set of language and platform features, designed by Edwin Brady. Being dependently typed allows types to be predicated on values, meaning some aspects of a program's correctness can be proved at compile time. Idris is compiled and targets C via a custom, lightweight virtual machine, though other backends are supported.
Facts
First Released ParadigmPurely functional with dependent types 2 Classification
Typing Discipline Connections
Influenced By
"The syntax of Idris shows many similarities with that of Haskell." en.wikipedia.org/wiki/Idris_(programming_language)
Sources
1. Wikidata: Idris
- Wikidata Q15408477, class allow-list match (w-wdresolver-0926)
- Wikidata Q15408477 P571 (inception)
- Wikidata Q15408477 P7078 (typing discipline)
View the Source2. Idris (Wikipedia)
Infobox, First appeared
First appeared 2007
Lead paragraph
Idris is a purely-functional programming language with dependent types, quantity annotations, optional lazy evaluation, and features such as a totality checker.
View the SourceDependent type (Wikipedia)
In Group: Dependently Typed Proof Assistant Languages, article names Idris among functional languages using dependent types to help reduce bugsView the Source Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.