Agda中的类型层次结构 [英] Type Hierarchy in Agda

问题描述

我正在尝试弄清类型层次结构在Agda中的工作方式.

I am trying to figure out how type hierarchies work in Agda.

假设我定义了一个集合类型X:

Assuming I define a set type X:

X : Set 

，然后继续构建归纳类型

and then proceed to constructing an inductive type

data Y : X -> Set where

X -> Set的类型是什么?是设置还是类型?

What is the type of X -> Set? Is it Set or Type?

谢谢！

推荐答案

那么，为什么不问Agda本身呢?我将对Emacs使用出色的Agda模式.我们从以下内容开始:

Well, why not ask Agda itself? I'm going to use excellent Agda mode for Emacs. We start with:

module Hierarchy where

postulate
  X : Set

data Y : X → Set where
  -- empty

我们必须使用C-c C-l加载文件；这种类型检查文件，将?变成空洞，进行语法高亮显示等等.

We have to load the file using C-c C-l; this typechecks the file, turns ?s into holes, does syntax highlighting and so on.

现在，通过C-c C-d可以使用推断(推断)类型"命令，因此让我们使用它:

Now, there is a command "Infer (deduce) type" available via C-c C-d, so let's use that:

> C-c C-d
Expression:
> Y
X → Set

对，这很有意义.我们定义了Y : X → Set，因此它不足为奇.让我们再问一次:

Right, that makes sense. We defined Y : X → Set, so it should come as no surprise. Let's ask again:

> C-c C-d
Expression:
> X → Set
Set₁

因此，您已找到它:Y : X → Set : Set₁.

So, there you have it: Y : X → Set : Set₁.

尽管第一部分回答了该问题并向您展示了如何亲自检查这些东西，但至少每次这样做都会很乏味.运作方式如下:

While the first part answers the question and shows you how to check this stuff yourself, doing that everytime would be dull, at least. Here's how it works:

为避免自相矛盾，我们要求

To avoid paradoxes, we require

Set i : Set (i + 1)

为您提供Set s的(无限)层次结构.如果具有Set : Set(Agda通过--type-in-type标志允许)，则可能会产生诸如

which gives you the (infinite) hierarchy of Sets. If you had Set : Set (which Agda allows via the --type-in-type flag), you could derive contradiction such as this one.

这也为我们提供了一个简单的函数规则:

This also gives us a simple rule for functions:

A : Set i
B : A → Set j

(a : A) → B a : Set (max i j)

将此应用于您的示例:

X   : Set
Set : Set₁

X → Set : Set (max 0 1)
X → Set : Set₁

这篇关于Agda中的类型层次结构的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！