Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Idris (programming language)
Résumé
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.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.