Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Idris (programming language)
Summary
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 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 Java virtual machine (JVM), Common Intermediate Language (CIL), and LLVM.
Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.
Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants.
The syntax of Idris shows many similarities with that of Haskell. A hello world program in Idris might look like this:
module Main
main : IO ()
main = putStrLn "Hello, World!"
The only differences between this program and its Haskell equivalent are the single (instead of double) colon in the type signature of the main function, and the omission of the word "where" in the module declaration.
Idris supports inductively-defined data types and parametric polymorphism. Such types can be defined both in traditional Haskell 98-like syntax:
data Tree a = Node (Tree a) (Tree a) | Leaf a
or in the more general generalized algebraic data type (GADT)-like syntax:
data Tree : Type -> Type where
Node : Tree a -> Tree a -> Tree a
Leaf : a -> Tree a
With dependent types, it is possible for values to appear in the types; in effect, any value-level computation can be performed during type checking.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.