Idris

Idris

编程范型	函数式编程
設計者	Edwin Brady
发行时间	2007年，​17年前​（2007）[1]
当前版本	1.3.3（2020年5月23日）[2]
型態系統	静态类型, 强类型, 依赖类型
操作系统	跨平台
許可證	BSD-3
文件扩展名	.idr, .lidr
網站	Idris
啟發語言
Agda, Coq, Epigram（英语：Epigram (programming language)）, Haskell, ML

Idris是一个通用的依赖类型纯函数式编程语言，其类型系统与Agda以及Epigram（英语：Epigram (programming language)）相似。

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

Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码，并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。^[4]

Idris的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗（英语：Ivor_the_Engine#Idris_the_Dragon）》里，一条会唱歌的龙。^[5]

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

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)

Idris 对嵌入式领域特定语言的支持主要包括以下方面^[6]：

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

Idris 拥有与 F# 相似的类型提供器，它允许编译器在编译期间根据所执行代码的需求而生成新的类型信息。这使得静态类型系统更具可扩展性。^[7]

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

module Main

main : IO ()
main = putStrLn "Hello, World!"

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

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

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

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

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

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

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

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

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

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

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;

• The Idris homepage（页面存档备份，存于互联网档案馆）, including documentation, frequently asked questions and examples
• Idris at the Hackage repository（页面存档备份，存于互联网档案馆）
• Idris Tutorial