MiniAgda: Integrating Sized and Dependent Types
MiniAgda: Integrating Sized and Dependent Types
复制标题
DOI：
10.4204/eptcs.43.2
复制
发表时间：
2010-01-01
影响因子：
--
通讯作者：
Abel, Andreas
中科院分区：
文献类型：
--
作者：
Abel, Andreas
大小类型是一种模块化的、理论上很容易理解的工具，用于检查递归定义的终止和共递归定义的生产率。其基本思想是跟踪类型系统中的结构下降和保护，以使终止检查具有鲁棒性，并适合于高阶函数和多态性等强抽象。为了研究大小类型在证明助手和基于依赖类型理论的编程语言中的应用，我们实现了一个核心语言MiniAgda，它显式地处理大小。为了将大小的类型与依赖关系和模式匹配完美地集成在一起，需要考虑新的因素，这可以通过不可访问模式和参数函数空间等概念实现。本文通过示例介绍了MiniAgda，并非正式地解释了其基本原理。
Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.