Introduction to Programming in ATS

查看原文 / View Original 编辑 / Edit

Introduction to Programming in ATS Hongwei Xi ATS Trustful Software, Inc. Copyright © 2010-201? Hongwei Xi

《ATS 编程入门》 Hongwei Xi，ATS Trustful Software, Inc. 版权所有 © 2010-201? Hongwei Xi。

As a programming language, ATS is both syntax-rich and feature-rich. This book introduces the reader to some core features of ATS, including basic functional programming, simple types, (recursively defined) datatypes, polymorphic types, dependent types, linear types, theorem-proving, programming with theorem-proving (PwTP), and template-based programming.

作为一种编程语言，ATS 既拥有丰富的语法，也具备强大的功能。本书向读者介绍了 ATS 的一些核心特性，包括基础函数式编程、简单类型、（递归定义的）数据类型、多态类型、依赖类型、线性类型、定理证明、基于定理证明的编程（PwTP）以及基于模板的编程。

Although the reader is not assumed to be familiar with programming in general, the book is likely to be rather dense for someone without considerable programming experience. All rights are reserved. Permission is granted to print this document for personal use.

尽管并不要求读者具备通用的编程基础，但对于缺乏丰富编程经验的人来说，本书的内容可能会显得相当晦涩。保留所有权利。允许打印本文档供个人使用。

Dedication To Jinning, Zoe, and Chloe. Table of Contents

献给 Jinning、Zoe 和 Chloe。目录

Preface I. Basic Functional Programming

  1. Preparation for Starting A Running Program A Template for Single-File Programs A Makefile Template

前言 第一部分：基础函数式编程

  1. 入门准备 一个可运行的程序 单文件程序模板 Makefile 模板

  2. Elements of Programming Expressions and Values Names and Bindings Scopes for Bindings Environments for Evaluation Static Semantics Primitive Types Tuples and Tuple Types Records and Record Types Conditional Expressions Sequence Expressions Comments in Code

  3. 编程要素 表达式与值 名称与绑定 绑定的作用域 求值环境 静态语义 原始类型 元组与元组类型 记录与记录类型 条件表达式 序列表达式 代码注释

  4. Functions Functions as a Simple Form of Abstraction Function Arity Function Interface Evaluation of Function Calls Recursive Functions Evaluation of Recursive Function Calls Example: Coin Changes for Fun Tail-Call and Tail-Recursion Example: The Eight-Queens Puzzle Mutually Recursive Functions Mutually Defined Tail-Recursion Envless Functions and Closure-Functions Higher-Order Functions Example: Binary Search for Fun Example: A Higher-Order Fun Puzzle Currying and Uncurrying

  5. 函数 作为简单抽象形式的函数 函数元数 函数接口 函数调用的求值 递归函数 递归函数调用的求值 示例：有趣的找零问题 尾调用与尾递归 示例：八皇后问题 互递归函数 互定义的尾递归 无环境函数与闭包函数 高阶函数 示例：有趣的二分查找 示例：一个高阶趣味谜题 柯里化与反柯里化

  6. Datatypes Patterns Pattern-Matching Matching Clauses and Case-Expressions Enumerative Datatypes Recursively Defined Datatypes Exhaustiveness of Pattern-Matching Example: Binary Search Tree Example: Evaluating Integer Expressions

  7. 数据类型 模式 模式匹配 匹配子句与 Case 表达式 枚举数据类型 递归定义的数据类型 模式匹配的完备性 示例：二叉搜索树 示例：整数表达式求值

  8. Parametric Polymorphism Function Templates Polymorphic Functions Polymorphic Datatypes Example: Function Templates on Lists Example: Mergesort on Lists

  9. 参数多态 函数模板 多态函数 多态数据类型 示例：列表上的函数模板 示例：列表的归并排序

II. Support for Practical Programming 6. Effectful Programming Features Exceptions Example: Testing for Braun Trees References Example: A Counter Implementation Arrays Example: Ordering Permutations Matrices Example: Estimating the Constant Pi Simple Input and Output

第二部分：实用编程支持 6. 有副作用的编程特性 异常 示例：Braun 树测试 引用 示例：计数器实现 数组 示例：排列排序 矩阵 示例：估算圆周率 Pi 简单的输入与输出

  1. Modularity Types as a Form of Specification Static and Dynamic ATS Files Generic Template Implementation Specific Template Implementation Abstract Types Example: A Package for Rationals Example: A Functorial Package for Rationals

  2. 模块化 作为规范形式的类型 静态与动态 ATS 文件 通用模板实现 特定模板实现 抽象类型 示例：有理数包 示例：有理数的函子包

  3. Interaction with C External Global Names External Types and Values in ATS Inclusion of External Code in ATS Calling External Functions in ATS Unsafe C-style Programming in ATS Exporting Types in ATS for Use in C Example: Constructing a Statically Allocated List

  4. 与 C 语言交互 外部全局名称 ATS 中的外部类型与值 在 ATS 中包含外部代码 在 ATS 中调用外部函数 ATS 中不安全的 C 风格编程 导出 ATS 类型供 C 使用 示例：构建静态分配的列表

III. Programming with Dependent Types 9. Introduction to Dependent Types Enhanced Expressiveness for Specification Constraint-Solving during Typechecking Example: String Processing Example: Binary Search on Arrays Termination-Checking for Recursive Functions Example: Dependent Types for Debugging

第三部分：依赖类型编程 9. 依赖类型简介 增强规范的表达能力 类型检查期间的约束求解 示例：字符串处理 示例：数组上的二分查找 递归函数的终止性检查 示例：用于调试的依赖类型

  1. Datatype Refinement Dependent Datatypes Example: Function Templates on Lists (Redux) Example: Mergesort on Lists (Redux) Sequentiality of Pattern Matching Example: Functional Red-Black Trees

  2. 数据类型细化 依赖数据类型 示例：列表上的函数模板（重构） 示例：列表的归并排序（重构） 模式匹配的顺序性 示例：函数式红黑树

  3. Theorem-Proving in ATS/LF Encoding Relations as Dataprops Constructing Proofs as Total Functions Example: Distributivity of Multiplication Example: Commutativity of Multiplication Algebraic Datasorts Example: Establishing Properties on Braun Trees Programmer-Centric Theorem-Proving

  4. ATS/LF 中的定理证明 将关系编码为数据属性（Dataprops） 将证明构造为全函数 示例：乘法分配律 示例：乘法交换律 代数数据排序（Datasorts） 示例：建立 Braun 树的属性 以程序员为中心的定理证明

  5. Programming with Theorem-Proving Circumventing Nonlinear Constraints Example: Safe Matrix Subscripting Specifying with Enhanced Precision Example: Another Verified Factorial Example: Verified Fast Exponentiation

  6. 基于定理证明的编程 规避非线性约束 示例：安全的矩阵下标访问 以更高精度进行规范 示例：另一个已验证的阶乘 示例：已验证的快速幂运算

IV. Programming with Views and Viewtypes 13. Introduction to Views and Viewtypes Views for Memory Access through Pointers Viewtypes as a Combination of Views and Types Left-Values and Call-by-Reference Stack-Allocated Variables Heap-Allocated Linear Closure-Functions

第四部分：视图与视图类型编程 13. 视图与视图类型简介 通过指针访问内存的视图 作为视图与类型组合的视图类型 左值与引用传递 栈分配变量 堆分配的线性闭包函数

  1. Dataviews as Linear Dataprops Optional Views Disjunctive Views Dataview for Linear Arrays Dataview for Linear Strings Dataview for Singly-Linked Lists Proof Functions for View-Changes

  2. 作为线性数据属性的数据视图 可选视图 析取视图 线性数组的数据视图 线性字符串的数据视图 单向链表的数据视图 视图变更的证明函数

  3. Dataviewtypes as Linear Datatypes Linear Optional Values Linear Lists Example: Merge-Sort on Linear Lists Example: Insertion Sort on Linear Lists Example: Quick-Sort on Linear Lists Linear Binary Search Trees Transition from Datatypes to Dataviewtypes

  4. 作为线性数据类型的数据视图类型 线性可选值 线性列表 示例：线性列表的归并排序 示例：线性列表的插入排序 示例：线性列表的快速排序 线性二叉搜索树 从数据类型到数据视图类型的转换

  5. Abstract Views and Viewtypes Simple Linear Objects Memory Allocation and Deallocation Example: Array-Based Circular Buffers Locking and Unlocking Linear Channels for Asynchronous IPC

  6. 抽象视图与视图类型 简单的线性对象 内存分配与释放 示例：基于数组的循环缓冲区 加锁与解锁 用于异步进程间通信（IPC）的线性通道

V. Programming with Function Templates 17. From Genericity to Late-Binding Genericity of Template Implementations Example: Generic Operations on Numbers Templates as a Special Form of Functors Example: Templates for Loop Construction Template-Based Support for Late-Binding Next Preface

第五部分：函数模板编程 17. 从泛型到后期绑定 模板实现的泛型 示例：数字的通用操作 作为特殊函子形式的模板 示例：循环构造模板 基于模板的后期绑定支持 下一页 前言

← 返回新闻列表 / Back to news list