| dbo:abstract
|
- Idris és un llenguatge de programació funcional amb tipus dependents de valors, desenvolupat a la Universitat escocesa de Saint Andrews sota la direcció d'. per a aplicacions de propòsit general amb la possibilitat de verificació estàtica incorporada. El sistema de tipus és similar al del llenguatge , amb una sintaxi molt semblant al Haskell però amb semàntica estricta (avaluació primerenca), designant l'avaluació tardana als tipus (tipus Lazy a). Els tipus hi són objectes de primer ordre, permetent barrejar objectes i tipus als paràmetres i resultats. Aquest llenguatge permet incorporar tipus com a proposicions i funcions com a proves, per certificar les propietats de la funcionalitat aportada, seguint la teoria de la Correspondència Curry-Howard entre programes i proves, incorporant propietats dels sistemes d'ajuda a la comprovació (Proof assistants) també anomenats com ara , o bé . (ca)
- 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 it 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 (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 JVM, CIL, and LLVM. Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine. (en)
- Idris — чистый функциональный язык программирования общего назначения с Haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства автоматического доказательства, сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как . Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. Реализован на Haskell, доступен в виде -пакета. Исходный код на Idris компилируется в набор промежуточных представлений, а из них — в си-код, при исполнении которого используется копирующий сборщик мусора с применением . Также официально реализована возможность компиляции в код на JavaScript (в том числе для Node.js). Существуют сторонние реализации кодогенераторов для Java, JVM, CIL, Erlang, PHP и (с ограничением) LLVM. Язык назван в честь поющего дракона Идриса из британской детской телепередачи 1970 года . Язык сочетает особенности основных популярных языков функционального программирования с возможностями, заимствованными из систем автоматического доказательства, фактически размывая границу между этими двумя классами языков. Вторая версия языка (выпущенная в 2020 году, основанная на «количественной теории типов») существенно отличается от первой: добавлена полноценная поддержка , код компилируется по умолчанию в Scheme, компилятор языка написан на самом языке. (ru)
- Idris是一个通用的依赖类型纯函数式编程语言，其类型系统与Agda以及相似。 Idris语言具备堪与Coq媲美的交互式定理证明能力，自带tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能，对副作用的控制，以及对于实现嵌入式领域特定语言（Embedded Domain Specific Language，EDSL）的支持。 Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码，并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。 Idris的名字来自于20世纪70年代的英国儿童动画片《》里，一条会唱歌的龙。 (zh)
|
| rdfs:comment
|
- Idris是一个通用的依赖类型纯函数式编程语言，其类型系统与Agda以及相似。 Idris语言具备堪与Coq媲美的交互式定理证明能力，自带tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能，对副作用的控制，以及对于实现嵌入式领域特定语言（Embedded Domain Specific Language，EDSL）的支持。 Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码，并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。 Idris的名字来自于20世纪70年代的英国儿童动画片《》里，一条会唱歌的龙。 (zh)
- Idris és un llenguatge de programació funcional amb tipus dependents de valors, desenvolupat a la Universitat escocesa de Saint Andrews sota la direcció d'. per a aplicacions de propòsit general amb la possibilitat de verificació estàtica incorporada. El sistema de tipus és similar al del llenguatge , amb una sintaxi molt semblant al Haskell però amb semàntica estricta (avaluació primerenca), designant l'avaluació tardana als tipus (tipus Lazy a). Els tipus hi són objectes de primer ordre, permetent barrejar objectes i tipus als paràmetres i resultats. (ca)
- 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 it is designed to be a general-purpose programming language similar to Haskell. Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine. (en)
- Idris — чистый функциональный язык программирования общего назначения с Haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства автоматического доказательства, сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как . Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. Язык назван в честь поющего дракона Идриса из британской детской телепередачи 1970 года . (ru)
|
