IDRIS编程入门教程

需积分: 10 151 浏览量更新于2024-07-18 收藏 298KB PDF 举报

“Programming in IDRIS: A Tutorial” 这篇文章是一篇关于IDRIS编程语言的教程，IDRIS是一种通用的功能性编程语言，它支持依赖类型。这个项目的目的是创建一种适合可验证系统编程的依赖类型语言。IDRIS是编译型语言，目标是生成高效的执行代码，并具有轻量级的外部C库交互接口。教程首先介绍了IDRIS社区和教程的目标受众。内容包括基础的编程概念，如预设条件、下载与安装、以及交互式环境的使用。接下来，深入探讨了IDRIS的核心特性： 1. **类型和函数**：IDRIS有多种基本类型，如整型、浮点型等。数据类型可以通过模式匹配进行定义，函数则可以用于操作这些类型。依赖类型使得类型系统更加强大，允许类型本身依赖于值。 - **依赖类型**：例如，可以定义长度已知的向量类型`Vector`，这在编译时就能确保向量操作的正确性。 - **有限集**：IDRIS可以表示有限集，提供了一种安全存储和操作元素集合的方法。 - **隐式参数**：通过隐式参数，IDRIS可以自动推导一些参数，简化代码。 - **“using”语法**：这种语法允许重用已有的函数或类型定义，提高代码的可读性和复用性。 - **输入/输出（I/O）**：IDRIS提供了I/O操作，允许与外部世界交互。 - **“do”注解**：用于描述 monad 中的顺序操作。 - **惰性求值**：IDRIS支持惰性求值，只有在必要时才计算表达式的值。 - **常用数据类型**：包括列表(List)和向量(Vect)，以及可能值(Maybe)、元组(Tuples)和依赖对(Dependent Pairs)。 3. **类型类**：IDRIS中的类型类类似于其他语言的接口，提供了默认定义、类扩展、monad 和 do-notation 支持。类型类可以用来抽象共同的行为，如错误处理。 4. **模块和命名空间**：模块系统允许组织代码，通过导出修饰符控制可见性，明确的命名空间避免了名称冲突，而参数化块则允许模块接受参数。 5. **示例：Well-Typed Interpreter**：教程通过构建一个类型正确的解释器实例来展示如何在实践中应用IDRIS的特性。 6. **视图和“with”规则**：视图允许将值转换为其他形式，而“with”规则帮助简化了这种转换过程中的代码。这篇教程为初学者提供了一个全面的IDRIS语言入门，涵盖了从基本概念到高级特性的广泛内容，有助于读者逐步掌握IDRIS的编程技巧和依赖类型系统的强大功能。

Can’t unify

Vect (n + n) a

with

Vect (plus n m) a

Specifically:

Can’t unify

plus n n

with

plus n m

This error message suggests that there is a length mismatch between two vectors — we needed a vector

of length n + m, but provided a vector of length n + n.

3.4.2 The Finite Sets

Finite sets, as the name suggests, are sets with a ﬁnite number of elements. They are declared as follows

(again, in the prelude):

data Fin : Nat -> Type where

FZ : Fin (S k)

FS : Fin k -> Fin (S k)

is the zeroth element of a ﬁnite set with

S k

elements;

FS n

is the

n+1

th element of a ﬁnite set with

S k

elements.

Fin

is indexed by a

Nat

, which represents the number of elements in the set. Obviously

we can’t construct an element of an empty set, so neither constructor targets Fin Z.

A useful application of the

Fin

family is to represent bounded natural numbers. Since the ﬁrst

natural numbers form a ﬁnite set of

elements, we can treat

Fin n

as the set of natural numbers

bounded by n.

For example, the following function which looks up an element in a

Vect

, by a bounded index given

as a Fin n, is deﬁned in the prelude:

index : Fin n -> Vect n a -> a

index FZ (x :: xs) = x

index (FS k) (x :: xs) = index k xs

This function looks up a value at a given location in a vector. The location is bounded by the length of

the vector (

in each case), so there is no need for a run-time bounds check. The type checker guarantees

that the location is no larger than the length of the vector.

Note also that there is no case for

Nil

here. This is because it is impossible. Since there is no element

Fin Z

, and the location is a

Fin n

, then

can not be

. As a result, attempting to look up an element

in an empty vector would give a compile time type error, since it would force n to be Z.

3.4.3 Implicit Arguments

Let us take a closer look at the type of index:

index : Fin n -> Vect n a -> a

It takes two arguments, an element of the ﬁnite set of

elements, and a vector with

elements of type

But there are also two names,

and

, which are not declared explicitly. These are implicit arguments to

index. We could also write the type of index as:

index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

Implicit arguments, given in braces

{}

in the type declaration, are not given in applications of

index

;

their values can be inferred from the types of the

Fin n

and

Vect n a

arguments. Any name with a

lower case initial letter which appears as a parameter or index in a type declaration, but which is otherwise

free, will be automatically bound as an implicit argument. Implicit arguments can still be given explicitly

in applications, using {a=value} and {n=value}, for example:

index {a=Int} {n=2} FZ (2 :: 3 :: Nil)

In fact, any argument, implicit or explicit, may be given a name. We could have declared the type of

index as:

index : (i:Fin n) -> (xs:Vect n a) -> a

It is a matter of taste whether you want to do this — sometimes it can help document a function by

making the purpose of an argument more clear.

3.4.4 “using” notation

Sometimes it is useful to provide types of implicit arguments, particularly where there is a dependency

ordering, or where the implicit arguments themselves have dependencies. For example, we may wish to

state the types of the implicit arguments in the following deﬁnition, which deﬁnes a predicate on vectors:

data Elem : a -> Vect n a -> Type where

Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

An instance of

Elem x xs

states that

is an element of

. We can construct such a predicate if the

required element is Here, at the head of the vector, or There, in the tail of the vector. For example:

testVec : Vect 4 Int

testVec = 3 :: 4 :: 5 :: 6 :: Nil

inVect : Elem 5 testVec

inVect = There (There Here)

If the same implicit arguments are being used a lot, it can make a deﬁnition difﬁcult to read. To avoid

this problem, a

using

block gives the types and ordering of any implicit arguments which can appear

within the block:

using (x:a, y:a, xs:Vect n a)

data Elem : a -> Vect n a -> Type where

Here : Elem x (x :: xs)

There : Elem x xs -> Elem x (y :: xs)

Note: Declaration Order and mutual blocks

In general, functions and data types must be deﬁned before use, since dependent types allow functions

to appear as part of types, and their reduction behaviour to affect type checking. However, this

restriction can be relaxed by using a

mutual

block, which allows data types and functions to be

deﬁned simultaneously:

mutual

even : Nat -> Bool

even Z = True

even (S k) = odd k

剩余54页未读，继续阅读

maxlee0916

粉丝: 1
资源: 1

IDRIS编程入门教程

sublime-idris:用于 Idris 语言的 Sublime Text 插件。 转移到@idris-hackers

programming-in-idris:按照 Idris 教程，也在玩

写一篇关于 群体饲养（群体效应）对动物和家蝇肠道菌群的影响 的文献综述 附引用文献

python数学建模算法电子书

各种函数声明和定义模块

湖北工业大学在河南2021-2024各专业最低录取分数及位次表.pdf

1805.06605v2 DEFENSE-GAN.pdf

【语音去噪】FIR和IIR低通+带通+高通语音信号滤波（含时域频域分析）【含Matlab源码 4943期】.mp4

java-ssm+jsp幼儿园管理系统实现源码(项目源码-说明文档)

hadoop_3_2_0-yarn-resourcemanager-3.3.4-1.el7.x86_64.rpm

最新资源

sublime-idris:用于 Idris 语言的 Sublime Text 插件。转移到@idris-hackers

写一篇关于群体饲养（群体效应）对动物和家蝇肠道菌群的影响的文献综述附引用文献