# 翻译-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 {#S1}

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 {#S2}

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:



---

> 作者: [采石场的主人](https://ych817.github.io)  
> URL: https://ych817.github.io/posts/2ceeee8/