Idris is a general-purpose purely functional programming language with dependent types. The type system is similar to the one used by Agda. The language supports interactive theorem-proving comparable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages. The name Idris goes back to the character of the singing dragon in the 1970s UK kids' program Ivor the Engine.

Property Value
dbo:abstract
  • Idris 是一个通用的依赖类型纯函数式编程语言,其类型系统与 Agda 以及 Epigram 相似。 Idris 语言具备堪与 Coq 媲美的交互式定理证明能力,自带 tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。 Idris 通过一个依赖类型的核心语言 TT 生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java 和 LLVM 的编译器后端。 Idris 的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗》里,一条会唱歌的龙。 (zh)
  • Idris это чисто-функциональный язык программирования общего назначения с haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства интерактивного доказательства теорем сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как язык программирования общего назначения. Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. По состоянию на 2014 год, Idris компилируется в C-код и использует копирующий сборщик мусора с использованием Алгоритма Чейни. Так-же реализованы backendы на JavaScript, Java и, частично, LLVM. Имя Idris является отсылкой к поющему дракону, персонажу британской детской телепередачи 1970 гг. Ivor the Engine. (ru)
  • Idris is a general-purpose purely functional programming language with dependent types. The type system is similar to the one used by Agda. The language supports interactive theorem-proving comparable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages. As of October 2014, Idris compiles to C and relies on a custom copying garbage collector using Cheney's algorithm. There also exist JavaScript and Java backends, and a partial LLVM backend. The name Idris goes back to the character of the singing dragon in the 1970s UK kids' program Ivor the Engine. (en)
dbo:influencedBy
dbo:latestReleaseVersion
  • 0.12
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 39035048 (xsd:integer)
dbo:wikiPageRevisionID
  • 741339539 (xsd:integer)
dbp:designer
  • Edwin Brady
dbp:fileExt
  • .idr, .lidr
dbp:license
  • -3.0
dbp:operatingSystem
dbp:paradigm
dct:subject
rdf:type
rdfs:comment
  • Idris 是一个通用的依赖类型纯函数式编程语言,其类型系统与 Agda 以及 Epigram 相似。 Idris 语言具备堪与 Coq 媲美的交互式定理证明能力,自带 tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。 Idris 通过一个依赖类型的核心语言 TT 生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java 和 LLVM 的编译器后端。 Idris 的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗》里,一条会唱歌的龙。 (zh)
  • Idris это чисто-функциональный язык программирования общего назначения с haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda. Язык поддерживает средства интерактивного доказательства теорем сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как язык программирования общего назначения. Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков. (ru)
  • Idris is a general-purpose purely functional programming language with dependent types. The type system is similar to the one used by Agda. The language supports interactive theorem-proving comparable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages. The name Idris goes back to the character of the singing dragon in the 1970s UK kids' program Ivor the Engine. (en)
rdfs:label
  • Idris (язык программирования) (ru)
  • Idris (zh)
  • Idris (programming language) (en)
owl:sameAs
prov:wasDerivedFrom
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • Idris (en)
foaf:page
is dbo:influenced of
is dbo:wikiPageDisambiguates of
is foaf:primaryTopic of