idris: Dependently Typed Functional Programming Language

[ bsd3, compilers-interpreters, dependent-types, library, program ] [ Propose Tags ]

Idris is an experimental language with full dependent types. 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.cs.st-andrews.ac.uk/~eb/Idris/tutorial.html.

The aims of the project are:

  • To provide a platform for realistic programming with dependent types. By realistic, we mean the ability to interact with the outside world and use primitive types and operations. This includes networking, file handling, concurrency, etc.

  • To show that full dependent types do not mean we have to abandon the functional style we have come to know and love with languages like Haskell and OCaml. We aim to show that lightweight dependently typed programming means allowing the programmer full access to values in types, and letting the type checker do the hard work so you don't have to!

The Darcs repository can be found at http://www-fp.cs.st-andrews.ac.uk/~eb/darcs/Idris.

Modules

[Last Documentation]

  • Idris
    • Idris.AbsSyntax
    • Idris.Compiler
    • Idris.ConTrans
    • Idris.Context
    • Idris.Fontlock
    • Idris.LambdaLift
    • Idris.Latex
    • Idris.Lexer
    • Idris.Lib
    • Idris.MakeTerm
    • Idris.PMComp
    • Idris.Parser
    • Idris.PartialEval
    • Idris.Prover
    • Idris.RunIO
    • Idris.SCTrans
    • Idris.Serialise
    • Idris.SimpleCase

Downloads

Versions [RSS] 0.1.3, 0.1.3.1, 0.1.4, 0.1.5, 0.1.7, 0.1.7.1, 0.9.0, 0.9.1, 0.9.2, 0.9.2.1, 0.9.3, 0.9.3.1, 0.9.4, 0.9.4.1, 0.9.5, 0.9.5.1, 0.9.6, 0.9.6.1, 0.9.7, 0.9.8, 0.9.9, 0.9.9.1, 0.9.9.2, 0.9.9.3, 0.9.10, 0.9.10.1, 0.9.11, 0.9.11.1, 0.9.11.2, 0.9.12, 0.9.13, 0.9.13.1, 0.9.14, 0.9.14.1, 0.9.14.2, 0.9.14.3, 0.9.15, 0.9.15.1, 0.9.16, 0.9.17, 0.9.17.1, 0.9.18, 0.9.18.1, 0.9.19, 0.9.19.1, 0.9.20, 0.9.20.1, 0.9.20.2, 0.10, 0.10.1, 0.10.2, 0.10.3, 0.11, 0.11.1, 0.11.2, 0.12, 0.12.1, 0.12.2, 0.12.3, 0.99, 0.99.1, 0.99.2, 1.0, 1.1.0, 1.1.1, 1.2.0, 1.3.0, 1.3.1, 1.3.2, 1.3.3, 1.3.4
Change log CHANGELOG
Dependencies array, base (>=4 && <5), binary, Cabal, containers, directory, epic (>=0.1.7), haskell98, ivor (>=0.1.14), mtl, old-locale, old-time, parsec, readline [details]
License BSD-3-Clause
Author Edwin Brady
Maintainer Edwin Brady <eb@cs.st-andrews.ac.uk>
Category Compilers/Interpreters, Dependent Types
Home page http://www.cs.st-andrews.ac.uk/~eb/Idris/
Uploaded by EdwinBrady at 2011-06-14T20:46:15Z
Distributions Arch:1.3.4, Fedora:1.3.4
Reverse Dependencies 1 direct, 0 indirect [details]
Executables idris
Downloads 68217 total (129 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-27 [all 7 reports]