@hackage idris1.2.0

Functional Programming Language with Dependent Types

  • Installation

    Custom

  • Tested Compilers

  • Dependencies (46)

  • Dependents (1)

    @hackage/acme-everything

    • Package Flags

      ffi
       (off by default)

      Build support for libffi

      gmp
       (off by default)

      Use GMP for Integers

      release
       (on by default)

      This is an official release

      freestanding
       (off by default)

      Build an Idris that doesn't use cabal

      ci
       (off by default)

      Built everything using "-Werror", meant for CI-builds only

      execonly
       (off by default)

      Build executables only, skip the libraries and RTS

Idris is a general purpose language with full dependent types. It is compiled, with eager evaluation. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. There is a tutorial at http://www.idris-lang.org/documentation. Features include:

  • Full, first class, dependent types with dependent pattern matching

  • where clauses, with rule, case expressions, pattern matching let and lambda bindings

  • Interfaces (similar to type classes), monad comprehensions

  • do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs

  • Totality checking

  • Coinductive types

  • Indentation significant syntax, extensible syntax

  • Cumulative universes

  • Simple foreign function interface (to C)

  • Hugs style interactive environment