Idris

Idris编程范型| 函数式编程

|

設計者| Edwin Brady
发行时间| 2007年，​18年前​（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 } ）的定义。如下定义了 Vec ( a , n ) {\displaystyle {\mbox{Vec}}(a,n)} ，即元素类型  a {\displaystyle a} 的  n {\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)

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

[编辑]

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

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

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

[编辑]

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;

## 参考文献

[编辑]

1. ^ Brady, Edwin. Index of /~eb/darcs/Idris. University of St Andrews School of Computer Science. 2007-12-12. （原始内容存档于2008-03-20）.
2. ^ Release 1.3.3. 2020年5月23日  [2020年5月24日].
3. ^ Release 1.3.3.  [2020-05-25]. （原始内容存档于2021-02-04）.
4. ^ Idris - News.  [2013-12-24]. （原始内容存档于2013-12-24）.
5. ^ Idris - FAQ.  [2013-12-24]. （原始内容存档于2012-03-11）.
6. ^ Slides from Systems Programming with Dependent Types at DTP11 (PDF). [永久失效連結]
7. ^ Christiansen, David. Dependent type providers (PDF). 2013  [2014-08-26]. （原始内容 (PDF)存档于2017-08-09）.

## 外部链接

[编辑]

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

* 查
* 论
* 编

编程语言

范型|

| 过程式|

* FORTRAN
* COBOL
* JOVIAL
* ALGOL 60
* JOSS（英语：JOSS）
* BASIC
* PL/I
* MUMPS（英语：MUMPS）
* ALGOL 68
* Forth
* Pascal
* Turbo Pascal
* C
* Modula-2
* Ada 83
* occam
* Oberon
* Go
* Ballerina（英语：Ballerina (programming language)）

|

面向对象|

* Simula 67
* Smalltalk
* Objective-C
* Eiffel
* Object Pascal
* Delphi
* Self
* CLOS
* Visual Basic
* Gambas
* Ada 95
* Java
* C#
* Vala
* Crystal（英语：Crystal (programming language)）

多范型|

* C++
* Modula-3
* Dylan
* Python
* Lua
* JavaScript
* Ruby
* D
* Factor
* Scala
* F#
* Haxe
* Nim
* Chapel（英语：Chapel (programming language)）
* Rust
* Kotlin
* Dart
* Swift
* Zig
* Ring（英语：Ring (programming language)）
* V（英语：V (programming language)）
* Mojo
* Carbon

函数式|

* LISP
* Scheme
* Common Lisp
* Clojure
* Logo
* APL/`J`
* ML
* Standard ML
* OCaml
* Erlang
* Elixir
* Haskell
* SAC
* Agda
* Idris
* jq
* Gleam（英语：Gleam (programming language)）

逻辑式|

* Prolog
* Datalog
* Mercury
* AnsProlog
* ProbLog（英语：ProbLog）

脚本语言|

| 动态语言|

* SNOBOL
* Icon
* REXX
* Perl
* Raku
* Tcl/Tk
* Python
* Lua
* Ruby
* PHP
* Hack
* CFML（英语：ColdFusion Markup Language）
* REBOL
* Red（英语：Red (programming language)）
* Io
* Julia
* jq

|

Shell语言|

* Unix shell
* sh/ash/dash
* csh/tcsh
* ksh
* bash
* zsh
* rc（英语：rc (Unix shell)）
* AWK
* PowerShell

ECMA-262|

* ECMAScript
* JavaScript
* TypeScript
* CoffeeScript/LiveScript（英语：LiveScript (programming language)）
* Elm
* PureScript
* Reason
* Bosque（英语：Bosque (programming language)）

特定平台|

| .NET|

* C#
* C++/CLI
* F#
* PowerShell
* VB.NET
* Small Basic

|

JVM|

* Java
* AspectJ（英语：AspectJ）
* Scala
* Clojure
* Groovy
* Kotlin

特定领域|

| 科学计算|

* Speakeasy（英语：Speakeasy (computational environment)）
* IDL
* GDL
* Maxima
* Maple
* MATLAB
* Octave
* Scilab
* Wolfram
* R
* Yorick（英语：Yorick (programming language)）
* SageMath
* Julia

|

GPU计算|

* Cg/HLSL
* GLSL/GLSL ES
* Brook（英语：BrookGPU）
* CUDA/PTX（英语：Parallel Thread Execution）
* OpenCL/SPIR-V（英语：Standard Portable Intermediate Representation）
* Futhark
* WGSL（英语：WebGPU Shading Language）

数据查询|

* CODASYL（英语：CODASYL）
* SQL
* PL/SQL
* T-SQL
* SQL/PSM（英语：SQL/PSM）
* xBase（英语：xBase）
* XPath
* XQuery（英语：XQuery）
* GraphQL

可视化|

* Prograph（英语：Prograph）
* Simulink
* LabVIEW
* Orange（英语：Orange (software)）
* KNIME（英语：KNIME）
* Scratch
* Snap!
* App Inventor
* Power Fx

传媒设计|

* SuperCollider
* Pure Data
* AviSynth
* Processing
* ChucK

其它|

* 汇编语言
* APT（英语：APT (programming language)）
* GPSS（英语：GPSS）
* CLIPS（英语：CLIPS）
* AMPL
* dc
* sed
* yacc
* make
* PostScript
* XSLT
* LLVM IR
* WebAssembly
* 深奥的编程语言

* 目录
* 列表
* 按类型排列（英语：List of programming languages by type）
* 历史
* 比较（英语：Comparison of programming languages）
* 时间线

*[查]: 查看该模板
*[论]: 讨论该模板
*[编]: 编辑该模板