Idris
Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including JVM, CIL, and LLVM.Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.
Relations
A programming language is a formal language comprising a set of instructions that produce various kin...
Edit details Edit relations Attach new author Attach new topic Attach new resource
Resources
treated in Type-driven development with Idris
Type-Driven Development with Idris, written by the creator of Idris, teaches you how to improve the p...
has official A Crash Course in Idris 2
This is a crash course in Idris 2 (sort of a tutorial, but rather less gentle I’m afraid!). It provid...
treated in Idris 2: Quantitative Type Theory in Action
Dependent types allow us to express precisely what a function is intended to do. Recent work on Quant...