The Idris Tutorial Version 2.3.0

• 语言: 英语
• 格式: .pdf
• 来源: docs.idris-lang.org

摘要

This document provides a comprehensive introduction to Idris, a dependently typed functional programming language. It covers the installation process, the interactive environment, type systems, implicit conversions, and foreign function calls. The tutorial also explores advanced topics such as theorem proving and effect handling, offering practical examples and guiding users through the language's features. The document emphasizes Idris' ability to generate efficient executable code and its lightweight foreign function interface for interacting with external libraries.

AI总结

《The Idris Tutorial Version 2.3.0》是一份关于Idris编程语言的教程，重点介绍了Idris的基本功能、语法、类型系统以及使用方法。以下是文档的核心内容总结：

### 1. Idris语言概述
- **Idris** 是一种通用的函数式编程语言，支持依赖类型（dependent types），旨在实现可验证的通用编程。
- 它是一个编译型语言，能够生成高效的可执行代码，并提供轻量级的外部函数接口（FFI），便于与C库交互。
- Idris的目标是通过依赖类型进行程序验证，从而提高程序的正确性。

### 2. 目标读者
- 适合熟悉函数式编程语言（如Haskell或OCaml）的读者。
- 读者应具备对依赖类型编程的兴趣，尤其是用于系统软件开发。

### 3. 示例代码
- 文档包含一些示例代码，这些代码已在Idris环境中测试通过。
- 建议读者手动输入代码，以加深理解。

### 4. 安装指南
#### 先决条件
- 需要安装较新版本的GHC（建议7.10.3或更高）。
- 需要GNU多精度算术库（GMP）。

#### 安装步骤
- 使用Cabal进行安装：

  cabal update; cabal install idris

- 如果需要最新开发版本，可从GitHub下载：

  https://github.com/idris-lang/Idris-dev

#### 验证安装
- 创建一个名为`hello.idr`的文件，内容如下：

  module Main
  main : IO ()
  main = putStrLn "Hello world"

- 编译并运行：

  idris hello.idr -o hello
  ./hello

### 5. 交互式环境
- 启动交互式环境：

  idris

- 提供类似GHCi的接口，支持表达式求值、类型检查、定理证明和代码编译等操作。
- 常用命令：
- `:?`：显示支持的命令列表。
- `:p`：查看当前目标。
- `:q`：退出交互式环境。

### 6. 类型系统
- **Vect**：向量类型，表示长度固定的列表，类型定义为`Vect n a`，其中`n`是向量的长度。
- **依赖类型**：类型可以依赖于值，例如`Vect : Nat -> Type -> Type`。
- **隐式转换**：允许自动将一个类型转换为另一个类型，以提高编程的便利性。

### 7. 字面编程
- Idris支持字面编程，文件扩展名为`.lidr`。
- 字面文件中，代码行以`>`开头，其余为注释。

### 8. 外联函数调用
- Idris提供轻量级的FFI，用于调用外部C库。
- 定义外部类型：

  data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit

- 对应的C类型分别为：`int`, `double`, `char`, `char*`, `void*`, `void`。

### 9. 效应处理
- Idris支持副作用编程，包括状态管理、异常处理和资源管理。
- 提供`Control.ST`模块，用于创建和管理可变状态。

### 10. 交互式定理证明
- Idris的交互式定理证明器可用于验证程序的正确性。
- 示例：证明加法的结合律`plusAssoc`。

### 11. 常见问题解答
- **自举**：Idris目前不是自举语言，但支持通过库实现部分自举功能。
- **宇宙层次**：Idris采用累积宇宙层次，`Type : Type 1`，且无法显式指定宇宙级别。
- **类型名称**：Idris使用`Double`表示双精度浮点数，不支持单精度`Float32`。

### 12. 文档许可
- 文档遵循Creative Commons CC0 License，所有版权和相关权利已放弃。

### 总结
《The Idris Tutorial》是一份全面介绍Idris语言的指南，涵盖了从安装、基本语法到高级功能（如依赖类型、交互式定理证明和效应处理）的详细内容。对于希望学习依赖类型编程或进行系统软件开发的读者来说，这是一份非常有价值的参考资料。