Idris

维基百科,自由的百科全书
跳转至: 导航搜索
Idris
编程范型 函数式编程
設計者 Edwin Brady
最新发行时间 0.9.14 / 2014年7月16日;9天前 (2014-07-16)
型態系統 静态类型强类型, 依赖类型
啟發語言 Agda, Coq, Epigram, Haskell, ML
作業系統 跨平台
許可證 BSD-3
常用文件扩展名 .idr, .lidr
網站 Idris

Idris是一个通用的依赖类型函数式编程语言,其类型系统Agda相似。

Idris语言具备堪与Coq媲美的交互式定理证明能力,包含tactics,而其侧重于通用编程更甚于定理证明。Idris的其他设计目标还包括“可观的”代码性能,副作用的控制,以及对于实现嵌入式领域特定语言(EDSL)的支持。

目前,Idris通过一个依赖类型的核心语言TT(core language)生成C语言的中间代码并编译到本地机器码,利用了一个基于Cheney算法垃圾收集器实现。Idris亦拥有JVMJavaScriptLLVM的编译器后端。[1]

Idris的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗》(Ivor the Engine)里,一条会唱歌的[2]

特性[编辑]

语法[编辑]

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

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

该程序与Haskell的等效写法仅有两点不同:类型签名中使用单个冒号“:”而不是双冒号“::”;开头的module声明中不必使用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 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;

参考文献[编辑]

外部链接[编辑]