查看“︁Idris”︁的源代码

{{Infobox programming language
| name                   = Idris
| logo                   = 
| paradigm               = [[函数式编程]]
| year                   = 
| designer               = Edwin Brady
| developer              = 
| released = {{Start date and age|2007}}<ref>{{cite web |last=Brady |first=Edwin |date=2007-12-12 |title=Index of /~eb/darcs/Idris |url=http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/ |website=[[University of St Andrews]] School of Computer Science |archive-url=https://web.archive.org/web/20080320233322/http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/ |archive-date=2008-03-20 }}</ref>
| latest_release_version = 1.3.3<ref>{{cite web|title=Release 1.3.3|url=https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.3/|access-date=2020-05-25|archive-date=2021-02-04|archive-url=https://web.archive.org/web/20210204084713/https://github.com/idris-lang/Idris-dev/releases/tag/v1.3.3}}</ref>
| latest_release_date = {{Start date and age|2020|05|24}}
| latest_test_version    = 
| latest_test_date       = 
| typing                 = [[静态类型]], [[强类型]], [[依赖类型]]
| implementations        = 
| dialects               = 
| influenced             = 
| influenced_by          = [[Agda]], [[Coq]], {{en-link|Epigram (编程语言)|Epigram (programming language)|Epigram}}, [[Haskell]], [[ML语言|ML]]
| license                = BSD-3
| website                = [http://idris-lang.org/ Idris]
| file ext               = .idr, .lidr
| operating_system       = [[跨平台]]
}}

'''Idris'''是一个通用的[[依赖类型]][[纯函数式编程语言]]，其[[类型系统]]与[[Agda]]以及{{en-link|Epigram (编程语言)|Epigram (programming language)|Epigram}}相似。

Idris语言具备堪与[[Coq]]媲美的交互式定理证明能力，自带tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能，对[[函数副作用|副作用]]的控制，以及对于实现嵌入式[[领域特定语言]]（Embedded Domain Specific Language，EDSL）的支持。

Idris通过一个依赖类型的核心语言TT生成[[C语言]]的中间代码并编译到本地机器码，并利用了一个基于[[Cheney算法]]的[[垃圾回收_(計算機科學)|垃圾收集器]]实现。Idris亦拥有 [[JavaScript]]、[[Java]]和[[LLVM]]的编译器后端。<ref>{{cite web|url=http://idris-lang.org/news|title=Idris - News|access-date=2013-12-24|archive-url=https://web.archive.org/web/20131224124749/http://www.idris-lang.org/news/|archive-date=2013-12-24|dead-url=yes}}</ref>

Idris的名字来自于20世纪70年代的英国儿童动画片《{{link-en|火车头艾弗|Ivor_the_Engine#Idris_the_Dragon}}》里，一条会唱歌的[[龙_(西方)|龙]]。<ref>{{cite web|url=http://idris-lang.org/documentation/faq|title=Idris - FAQ|deadurl=yes|archiveurl=https://web.archive.org/web/20120311111339/http://idris-lang.org/documentation/faq|archivedate=2012-03-11|accessdate=2013-12-24}}</ref>

== 语言特性 ==

=== 依赖类型 ===

Idris 支持对[[依赖类型]]（<math>\lambda \Pi</math>）的定义。如下定义了<math>\mbox{Vec}(a,n)</math>，即元素类型 <math>a</math> 的 <math>n</math>-元组类型：

<syntaxhighlight lang="haskell">
data Nat = O | S Nat
infixr 5 ::

data Vect : Type -> Nat -> Type where
    VNil : Vect a O
  | (::) : a -> Vect a k -> Vect a (S k)
</syntaxhighlight>

=== 嵌入式领域特定语言（EDSL） ===

Idris 对嵌入式领域特定语言的支持主要包括以下方面<ref>{{cite web|url=http://www.cs.st-andrews.ac.uk/~eb/writings/dtp11.pdf|title=Slides from Systems Programming with Dependent Types at DTP11}}{{dead link|date=2017年11月 |bot=InternetArchiveBot |fix-attempted=yes }}</ref>：

# [[编译期间]]求值。
# 可[[重载]]的语法。
# 与C语言库的接口，以及高效的[[代码生成]]。

=== 类型提供器（Type Provider） ===

Idris 拥有与 [[F♯|F#]] 相似的类型提供器，它允许编译器在编译期间根据所执行代码的需求而生成新的类型信息。这使得静态类型系统更具可扩展性。<ref>{{cite journal|last=Christiansen|first=David|title=Dependent type providers|year=2013|url=http://itu.dk/people/drc/pubs/dependent-type-providers.pdf|journal=|access-date=2014-08-26|archive-date=2017-08-09|archive-url=https://web.archive.org/web/20170809082518/http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf|dead-url=yes}}</ref>

== 示例 ==
=== 语法 ===
Idris 的语法与 [[Haskell]] 有许多相似之处。一个最简单的 [[Hello World]] 程序如下：

<syntaxhighlight lang="haskell">
module Main

main : IO ()
main = putStrLn "Hello, World!"
</syntaxhighlight>

该程序与 Haskell 的等效写法仅有两点不同：类型签名使用单个冒号“:”而不是双冒号“::”；开头的模块声明中不必使用 where 从句。

Idris 亦支持 where 从句、let 表达式、with 规则、简单的 case 表达式和模式匹配等。

=== 依赖类型 ===
一个在 Idris 中使用依赖类型的示例：

<syntaxhighlight lang="haskell">
total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys
</syntaxhighlight>

该函数将一个包含 m 个类型 a 的元素的 vector 连接到一个包含 n 个类型 a 的元素的 vector 之后。由于输入 vector 的确切类型依赖于它的值，故在编译（类型检查）时即可保证输出的 vector 必将包含 (n + m) 个类型 a 的元素。

关键字“total”将会执行函数的完整性（totality）检查。若函数定义未涵盖所有可能的情形（partial function），则检查器会报错。

另一个使用依赖类型的示例：

<syntaxhighlight lang="haskell">
total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
</syntaxhighlight>

Num a 标志着类型 a 属于 {{link-en|Type class|Type class}} Num。注意在这里，该函数被认为是完整的（total），尽管并未定义一个参数是 Nil 而另一个参数非 Nil 的模式。原因在于两个作为参数的 vector 只能具备相同的长度，这一点通过依赖类型系统得到了保证，因此在编译时两者长度不同的情形绝无可能发生。这使得该函数定义仍然是完整的。

=== 求值策略 ===
Idris 默认采取[[及早求值]]（Eager evaluation），而非 Haskell 的[[惰性求值]]（Lazy evaluation）方式。Idris 支持使用 Lazy 关键字显式地指定惰性求值：

<syntaxhighlight lang="haskell">
data Lazy : Type -> Type where
  Delay : (val : a) -> Lazy a

Force : Lazy a -> a

boolCase : Bool -> Lazy a -> Lazy a -> a;
boolCase True t e = t;
boolCase False t e = e;
</syntaxhighlight>

== 参考文献 ==
{{reflist}}

== 外部链接 ==
* [http://idris-lang.org/ The Idris homepage]{{Wayback|url=http://idris-lang.org/ |date=20201112032249 }}, including documentation, frequently asked questions and examples
* [http://hackage.haskell.org/package/idris Idris at the Hackage repository]{{Wayback|url=http://hackage.haskell.org/package/idris |date=20201127003350 }}
* [https://web.archive.org/web/20120315161110/http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdf Idris Tutorial]

{{程序设计语言|Idris}}

[[Category:程序设计语言]]
[[Category:函数式编程语言]]
[[Category:2007年建立的程式語言]]