Idris (programming language)

aesthetics  →
being  →
complexity  →
database  →
enterprise  →
ethics  →
fiction  →
history  →
internet  →
knowledge  →
language  →
licensing  →
linux  →
logic  →
method  →
news  →
perception  →
philosophy  →
policy  →
purpose  →
religion  →
science  →
sociology  →
software  →
truth  →
unix  →
wiki  →
essay  →
feed  →
help  →
system  →
wiki  →
critical  →
discussion  →
forked  →
imported  →
original  →
Idris (programming language)
[ temporary import ]
please note:
- the content below is remote from Wikipedia
- it has been imported raw for GetWiki

Agda (programming language)>Agda, Clean (programming language),"UNIQUENESS TYPES"ACCESSDATE=2018-11-20, Coq,IDRIS, A LANGUAGE WITH DEPENDENT TYPES>URL=HTTP://WWW.IDRIS-LANG.ORG/Epigram (programming language)>Epigram, Haskell (programming language), ML (programming language)>ML, Rust| influenced =| operating_system = Cross-platform| license = BSD-3| file ext = .idr,}}}}Idris is a general-purpose purely functional programming language with dependent types, strict or optional lazy evaluation and features such as a totality checker.Even before its possible usage for interactive theorem-proving, the focus of Idris is on general-purpose programming, like the purely functional Haskell, and with sufficient performance. The type system of Idris is similar to the one used by Agda and theorem-proving in it is similar to Coq, including tactics. In comparison, Idris has a priority on easy management of side-effects and support for implementing embedded domain specific languages.{{As of|2017|05}}, 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 also a number of third-party code generators for other platforms, including Java, JVM, CIL, OCaml, and a partial LLVM backend.WEB,weblink Code Generation Targets — Idris 1.1.1 documentation,, The name Idris goes back to the character of the singing dragon in the 1970s UK children's television program Ivor the Engine.WEB, Frequently Asked Questions,weblink 2015-07-19,


Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants.

Functional programming

The syntax of Idris shows many similarities with that of Haskell. A hello world program in Idris might look like this:module Mainmain : IO ()main = putStrLn "Hello, World!"The only differences between this program and its Haskell equivalent are the single colon (instead of two) in the signature of the main function and the omission of the word "where" in the module declaration.

Inductive and parametric data types

Like most modern functional programming languages, Idris supports a notion of inductively-defined data type and parametric polymorphism. Such types can be defined both in traditional "Haskell98" syntax:data Tree a = Node (Tree a) (Tree a) | Leaf aor in the more general GADT syntax:data Tree : Type -> Type where
Node : Tree a -> Tree a -> Tree a
Leaf : a -> Tree a

Dependent types

With dependent types, it is possible for values to appear in the types; in effect, any value-level computation can be performed during typechecking. The following defines a type of lists of statically known length, traditionally called 'vectors':data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a
This type can be used as follows:totalappend : Vect n a -> Vect m a -> Vect (n + m) aappend Nil ys = ysappend (x :: xs) ys = x :: append xs ysThe functions append a vector of m elements of type a to a vector of n elements of type a. Since the precise types of the input vectors depend on a value, it is possible to be certain at compile-time that the resulting vector will have exactly (n + m) elements of type a.The word "total" invokes the totality checker which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven to not enter an infinite loop.Another common example is pairwise addition of two vectors that are parameterized over their length:totalpairAdd : Num a => Vect n a -> Vect n a -> Vect n apairAdd Nil Nil = NilpairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ysNum a signifies that the type a belongs to the type class Num. Note that this function still typechecks successfully as total, even though there is no case matching Nil in one vector and a number in the other. Since both vectors are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.

Proof assistant features

Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile-time. This makes Idris into a proof assistant.There are two standard ways of interacting with proof assistants: by writing a series of tactic invocations (Coq style), or by interactively elaborating a proof term (Epigram/Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.

Code generation

Because Idris contains a proof assistant, Idris programs can be written to pass proofs around. If treated naïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms,WEB,weblink Erasure By Usage Analysis — Idris 1.1.1 documentation,, with promising{{Vague|date=May 2018}} results.WEB,weblink Benchmark results,, By default, Idris generates native code by going through C. Other backends are available for generating JavaScript and Java.

See also



External links

{{Programming languages}}

- content above as imported from Wikipedia
- "Idris (programming language)" does not exist on GetWiki (yet)
- time: 1:27pm EST - Sun, Feb 17 2019
[ this remote article is provided by Wikipedia ]
LATEST EDITS [ see all ]
M.R.M. Parrott