Các loại quy nạp được mô tả trong Agda

Question

Tôi chỉ đọc Dependent Types at Work. Trong phần giới thiệu parametrised loại, tác giả đề cập rằng trong tuyên bố này

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

loại List là Set → Set và A trở thành tranh cãi tiềm ẩn cho cả nhà thầu, tức là.

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

Vâng, tôi đã cố gắng để viết lại nó một chút khác nhau

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

mà buồn bã không hoạt động (Tôi đang cố gắng tìm hiểu Agda trong hai ngày hoặc lâu hơn, nhưng từ những gì tôi thu thập được nó bởi vì các nhà xây dựng được parametrised qua Set₀ và do đó List A phải ở trong Set₁).

Thật vậy, sau đây được chấp nhận

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

Tuy nhiên, tôi không còn có thể sử dụng {A : Set} → ... → List (List A) (đó là hoàn toàn dễ hiểu).

Vì vậy, câu hỏi của tôi: Sự khác biệt thực sự giữa List (A : Set) : Set và List : Set → Set là gì?

Cảm ơn bạn đã dành thời gian!

Answer 1

Tôi lấy quyền tự do đổi tên các loại dữ liệu. Đầu tiên, đó là lập chỉ mục trên Set sẽ được gọi ListI, và lần thứ hai ListP, có Set như một tham số:

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 

Trong kiểu dữ liệu thông số đi trước dấu hai chấm, và lập luận sau khi ruột được gọi là chỉ dẫn. Các nhà thầu có thể được sử dụng theo cùng cách , bạn có thể áp dụng bộ ẩn:

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

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

Có sự khác biệt khi khớp mẫu. Đối với phiên bản được lập chỉ mục chúng ta có:

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

này không thể được thực hiện cho ListP:

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

Các thông báo lỗi là

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

ListP cũng có thể được định nghĩa với một mô-đun giả, như ListD:

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

open Dummy public 

Có lẽ một chút đáng ngạc nhiên, ListD bằng ListP. Chúng ta không thể mô hình trận đấu trên lập luận để Dummy:

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

này đưa ra thông điệp báo lỗi tương tự như đối với ListP.

ListP là một ví dụ về một kiểu dữ liệu parameterised, đó là đơn giản hơn ListI, mà là một gia đình quy nạp: nó "phụ thuộc" vào indicies, mặc dù trong ví dụ này một cách tầm thường.

Loại dữ liệu tham số được xác định trên the wiki, và here là một phần giới thiệu nhỏ.

gia đình Inductive không thực sự xác định, nhưng xây dựng trên trong the wiki với ví dụ kinh điển của một cái gì đó mà dường như cần quy nạp gia đình:

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

Bất chấp chỉ số Type, một phiên bản đơn giản này có thể không được được viết bằng Dummy cách thức mô-đun vì công cụ xây dựng lam.

Một tài liệu tham khảo tốt là Inductive Families Peter Dybjer từ năm 1997.

Chúc mừng Agda mã hóa!