Параметризованные индуктивные типы в Агде - PullRequest
Новая
       63

Параметризованные индуктивные типы в Агде

14 голосов
/ 22 января 2012

Я просто читаю Зависимые типы на работе .Во введении к параметризованным типам автор упоминает, что в этом объявлении 

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

тип List равен Set → Set и что A становится неявным аргументом для обоих конструкторов, т. Е. 

[]   : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A

Ну, я пытался переписать это немного по-другому 

data List : Set → Set where
  []   : {A : Set} → List A
  _::_ : {A : Set} → A → List A → List A

, что, к сожалению, не работает (я пытаюсь изучать Агду в течение двух дней или около того, но из того, что я собралэто потому, что конструкторы параметризованы над Set₀, и поэтому List A должно быть в Set₁).

Действительно, следующее принимается 

data List : Set₀ → Set₁ where
  []   : {A : Set₀} → List A
  _::_ : {A : Set₀} → A → List A → List A

однако я небольше не в состоянии использовать {A : Set} → ... → List (List A) (что вполне понятно).

Так что мой вопрос: какова реальная разница между List (A : Set) : Set и List : Set → Set?

Спасибо за ваше время!

1 Ответ

14 голосов
/ 27 января 2012

Я позволю себе переименовать типы данных.Первый, индексированный по Set, будет называться ListI, а второй ListP имеет Set в качестве параметра: 

data ListI : Set → Set₁ where
  []  : {A : Set} → ListI A
  _∷_ : {A : Set} → A → ListI A → ListI A

data ListP (A : Set) : Set where
  []  : ListP A
  _∷_ : A → ListP A → ListP A

В типах данных параметры идут перед двоеточием,и аргументы после двоеточия называются указами.Конструкторы могут быть использованы таким же образом, вы можете применить неявный набор: 

nilI : {A : Set} → ListI A
nilI {A} = [] {A}

nilP : {A : Set} → ListP A
nilP {A} = [] {A}

Разница возникает при сопоставлении с образцом.Для индексированной версии у нас есть: 

null : {A : Set} → ListI A → Bool
null ([]  {A})     = true
null (_∷_ {A} _ _) = false

Этого нельзя сделать для ListP: 

-- does not work
null′ : {A : Set} → ListP A → Bool
null′ ([]  {A})     = true
null′ (_∷_ {A} _ _) = false

Сообщение об ошибке: 

The constructor [] expects 0 arguments, but has been given 1
when checking that the pattern [] {A} has type ListP A

ListPтакже может быть определен с помощью фиктивного модуля, как ListD: 

module Dummy (A : Set) where
  data ListD : Set where
    []  : ListD
    _∷_ : A → ListD → ListD

open Dummy public

Возможно, немного удивительно, ListD равен ListP.Мы не можем сопоставить шаблон с аргументом Dummy: 

-- does not work
null″ : {A : Set} → ListD A → Bool
null″ ([]  {A})     = true
null″ (_∷_ {A} _ _) = false

Это выдает то же сообщение об ошибке, что и для ListP.

ListP - пример параметризованного типа данных, что проще, чем ListI, который является индуктивным семейством: он «зависит» от признаков, хотя в этом примере это тривиальным образом.

Параметризованные типы данных определены в в вики и здесь - небольшое введение.

Индуктивные семейства на самом деле не определены, а детально проработаны в вики с каноническим примером чего-то, что кажетсянужны индуктивные семейства: 

data Term (Γ : Ctx) : Type → Set where
  var : Var Γ τ → Term Γ τ
  app : Term Γ (σ → τ) → Term Γ σ → Term Γ τ
  lam : Term (Γ , σ) τ → Term Γ (σ → τ)

Вне зависимости от индекса типа упрощенная версия этого не может быть записана с помощью Dummy -модуля из-за конструктора lam.

Другойхороший пример - Индуктивные семьи Питера Дайбджера с 1997 года.

Счастливого кодирования Agda!

...