Topic | v1 | created by jjones |

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.


is Programming language

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

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