翻译-a Few Constructions on Constructors

摘要 Abstract

We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach— they require less work than the standard techniques which inspired them. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style to the equivalent programs expressed in terms of induction principles and as such play a crucial behind-the-scenes rˆole in Epigram.

1. 简介 Introduction

In this paper, we show how to equip inductive families of datatypes with useful standard constructions. When you declare an inductive datatype, you expect the following to be available ‘for free’:

• the ability to write terminating computations by case analysis and structural recursion;

• proofs that its constructors are injective and disjoint; and

• proofs that cyclic equations are refutable.

We show these expectations to be well-founded by exhibiting constructions which fulfil them. These constructions may readily be mechanised, so that we may rely on these intuitive properties of datatypes implicitly as we go about our work.

In prior publications, we have indeed relied implicitly on these properties. Both the ‘elimination with a motive’ tactic and the Epigram programming language make heavy use of this equipment, but the constructions themselves have only appeared in. We hope that this paper will serve as a more accessible technical reference.

Our approach to all of these constructions is more directly computational than others in the literature. In effect, our presentation of the structural recursion operator reworks Giménez’s inductive justification of Coq’s fix primitive, but for us the notion of ‘guarded by constructors’ is expressed by a recursive computation. Meanwhile, the ‘constructors injective and disjoint’ properties are captured by a single ‘no confusion’ theorem which computes its conclusion from its input. This sidesteps the problems of extending the ‘equality respects predecessors’ method of proving injectivity (automated for simple types by Cornes and Terrasse, and still standard) to inductive families. It is, besides, rather neater. The ‘refutation of cyclic equations’ is again presented as a single theorem for each datatype family. To our knowledge, this construction is entirely original.

2. 归纳数据类型 Inductive Datatypes

Before we begin, let us be clear about the data with which we deal and also introduce our notational conventions. We mean the strictly positive inductive families of datatypes from Luo’s UTT. Modulo technical details, these correspond to the inductive families found in the Alf system, the Coq system and Epigram. The story we tell here is by no means specific to any one presentation. Here we follow Epigram’s presentational style, with declarations of datatype families and their constructors, and the type signatures of function definitions, given by ‘inference rules’ resembling those of natural deduction. As well as avoiding a cumbersome and scarcely legible linearised notation for dependent types, we exploit the ability to systematically omit declarations which may be inferred during typechecking.

The $Tree$ example. We require that a datatype be presented by a formation rule and constructors— $Tree$ provides the paradigm: