Idris
Idris 是一个通用的依赖类型纯函数式编程语言,其类型系统与 Agda 以及 Epigram 相似。
函数式编程 | |
設計者 | Edwin Brady |
2007年[1] | |
穩定版本 | 1.3.3[2]
( 2020年5月24日
) |
型態系統 | 静态类型, 强类型, 依赖类型 |
作業系統 | 跨平台 |
許可證 | BSD-3 |
文件扩展名 | .idr, .lidr |
網站 | Idris |
啟發語言 | |
Agda, Coq, Epigram, Haskell, ML |
Idris 语言具备堪与 Coq 媲美的交互式定理证明能力,自带 tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。
Idris 通过一个依赖类型的核心语言 TT 生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java 和 LLVM 的编译器后端。[3]
语言特性
依赖类型
Idris 支持对依赖类型()的定义。如下定义了,即元素类型 的 -元组类型:
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 的语法与 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 Num。注意在这里,该函数被认为是完整的(total),尽管并未定义一个参数是 Nil 而另一个参数非 Nil 的模式。原因在于两个作为参数的 vector 只能具备相同的长度,这一点通过依赖类型系统得到了保证,因此在编译时两者长度不同的情形绝无可能发生。这使得该函数定义仍然是完整的。
参考文献
外部链接
- The Idris homepage页面存档备份,存于, including documentation, frequently asked questions and examples
- Idris at the Hackage repository页面存档备份,存于
- Idris Tutorial