Ответ 1
Я беру на себя смелость переименовывать типы данных. Первый, который
индексированный на 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 года.
Счастливое кодирование Агда!