 | This articlerelies excessively onreferences toprimary sources. Please improve this article by addingsecondary or tertiary sources. Find sources: "Idris" programming language – news ·newspapers ·books ·scholar ·JSTOR(August 2019) (Learn how and when to remove this message) |
| Idris | |
|---|---|
| Paradigm | Functional |
| Designed by | Edwin Brady |
| First appeared | 2007; 18 years ago (2007)[1] |
| Stable release | |
| Typing discipline | Dependent |
| OS | Cross-platform |
| License | BSD |
| Filename extensions | .idr, .lidr |
| Website | idris-lang |
| Influenced by | |
| Agda,Clean,[3]Rocq (previously known as Coq),[4]Epigram,F#,Haskell,[4]ML,[4]Rust[3] | |
Idris is apurely-functionalprogramming language withdependent types,quantity annotations, optionallazy evaluation, and features such as atotality checker. Idris is designed to be ageneral-purpose programming language similar toHaskell, but may also be used as aproof assistant.
The Idristype system is similar toAgda's. Compared to Agda, Idris prioritizes management ofside effects and support forembedded domain-specific languages. Idris is compiled by modular backends, which provide code generation and aruntime system.[5] The Idris compiler includes backends forChez Scheme,Racket,JavaScript (both browser- andNode.js-based), andC. Additional third-party backends are available for other platforms.[6]
Idris is named after a singing dragon from the 1970s UK children's television programmeIvor the Engine.[7]
Idris combines a number of features from relatively mainstream functional programming languages with features borrowed fromproof assistants.
The syntax of Idris shows many similarities with that of Haskell. Ahello world program in Idris might look like this:
moduleMainmain:IO()main=putStrLn"Hello, World!"
The only differences between this program and itsHaskell equivalent are the single (instead of double) colon in thetype signature of the main function, and the omission of the word "where" in themodule declaration.[8]
Idris supportsinductively-defined data types andparametric polymorphism. Such types can be defined both in traditionalHaskell 98-like syntax:
dataTreea=Node(Treea)(Treea)|Leafa
or in the more generalgeneralized algebraic data type (GADT)-like syntax:
dataTree:Type->TypewhereNode:Treea->Treea->TreeaLeaf:a->Treea
Withdependent types, it is possible for values to appear in the types; in effect, any value-level computation can be performed duringtype checking. The following defines a type of lists whose lengths are known before the program runs, traditionally calledvectors:
dataVect:Nat->Type->TypewhereNil:Vect0a(::):(x:a)->(xs:Vectna)->Vect(n+1)a
This type can be used as follows:
totalappend:Vectna->Vectma->Vect(n+m)aappendNilys=ysappend(x::xs)ys=x::appendxsys
The functionappend appends a vector ofm elements of typea to a vector ofn elements of typea. Since the precise types of the input vectors depend on a value, it is possible to be certain atcompile time that the resulting vector will have exactly (n +m) elements of typea.The word "total" invokes thetotality checker which will report an error if the functiondoesn't cover all possible cases or cannot be (automatically) proven not to enter aninfinite loop.
Another common example is pairwise addition of two vectors that are parameterized over their length:
totalpairAdd:Numa=>Vectna->Vectna->VectnapairAddNilNil=NilpairAdd(x::xs)(y::ys)=x+y::pairAddxsys
Num a signifies that the type a belongs to thetype classNum. Note that this function still typechecks successfully as total, even though there is no case matchingNil in one vector and a number in the other. Because the type system can prove that the vectors have the same length, we can be sure at compile time that case will not occur and there is no need to include that case in the function’s definition.
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 (Rocq 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 Rocq.[vague]
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.[9][10]
By default, Idris generates native code throughC. The other officially supported backend generatesJavaScript.
Idris 2 is a newself-hosted version of the language which deeply integrates alinear type system, based onquantitative type theory. It currently compiles toScheme andC.[11]
Haskell programming | |||||
|---|---|---|---|---|---|
| Software |  | ||||
| Book | |||||
| Community |
| ||||
