Cơ chế phát sinh Haskell cho Agda

Question

Tôi tự hỏi nếu có bất kỳ điều gì trong Agda giống với mệnh đề deriving Eq của Haskell --- thì tôi cũng có một câu hỏi liên quan bên dưới.

Ví dụ, giả sử tôi có các loại cho một món đồ chơi ngôn ngữ,

data Type : Set where 
    Nat : Type 
    Prp : Type 

Sau đó, tôi có thể thực hiện bình đẳng decidable bởi mô hình kết hợp và C-c C-a,

_≟ₜ_ : Decidable {A = Type} _≡_ 
Nat ≟ₜ Nat = yes refl 
Nat ≟ₜ Prp = no (λ()) 
Prp ≟ₜ Nat = no (λ()) 
Prp ≟ₜ Prp = yes refl 

tôi tò mò nếu điều này có thể được cơ giới hóa hoặc tự động bằng cách nào đó tương tự như cách thức được thực hiện trong Haskell:

data Type = Nat | Prp deriving Eq 

Cảm ơn bạn!

Trong khi chúng ta đang ở trên chủ đề của các loại, tôi muốn nhận ra các loại chính thức của tôi như các loại Agda: Nat chỉ là số tự nhiên trong khi Prp là các mệnh đề nhỏ.

⟦_⟧Type : Type → Set ? 
⟦ Nat ⟧Type = ℕ 
⟦ Prp ⟧Type = Set 

Đáng buồn là điều này không có tác dụng. Tôi đã cố gắng sửa lỗi này bằng cách nâng nhưng không thành công vì tôi không biết cách sử dụng mức nâng. Bất kỳ trợ giúp được đánh giá cao!

Một cách sử dụng ví dụ của hàm trên sẽ là,

record InterpretedFunctionSymbol : Set where 
    field 
    arity : ℕ 
    src tgt : Type 
    reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type 

Thank-you cho humouring tôi!

Answer 1

Chương trình "7.3.2. Hoạt động phát sinh trên kiểu dữ liệu" của A Cosmology of Datatypes cho biết cách lấy hoạt động bằng mô tả. Mặc dù, các nguồn gốc Eq là khá yếu ở đó.

Ý tưởng cơ bản là đại diện cho kiểu dữ liệu sử dụng mã hóa đơn hàng đầu tiên, nghĩa là về một số loại dữ liệu chung và xác định hoạt động trên loại dữ liệu này, vì vậy mọi thứ được mã hóa theo điều khoản có thể được xử lý bởi các hoạt động chung này . Tôi đã xây dựng một phiên bản đơn giản của máy móc này here.

Bạn có thể lấy được Eq mạnh mẽ hơn, nếu bạn có vũ trụ kín. Sử dụng phương pháp tiếp cận tương tự như mô tả (phải mang tính biểu cảm như nhau, nhưng tôi không kiểm tra) và một vũ trụ kín tôi đã xác định chung là showhere, cho phép ví dụ: in một vector của các bộ sau khi bạn đặt tên cho các nhà thầu:

instance 
    named-vec : {A : Type} -> Named (vec-cs A) 
    named-vec = record { names = "nil" ∷ "cons" ∷ [] } 

test₂ : show (Vec (nat & nat) 3 ∋ (7 , 8) ∷ᵥ (9 , 10) ∷ᵥ (11 , 12) ∷ᵥ []ᵥ) 
     ≡ "(cons 2 (7 , 8) (cons 1 (9 , 10) (cons 0 (11 , 12) nil)))" 
test₂ = prefl 

nơi Vec được định nghĩa trong điều khoản của một tương tự như Desc kiểu dữ liệu. Trường hợp Eq phải tương tự, nhưng phức tạp hơn.

Sau đây là cách Lift thể được sử dụng:

⟦_⟧Type : Type → Set₁ 
⟦ Nat ⟧Type = Lift ℕ 
⟦ Prp ⟧Type = Set 

ex₁ : ∀ A -> ⟦ A ⟧Type 
ex₁ Nat = lift 0 
ex₁ Prp = ℕ 

ex₂ : ∀ A -> ⟦ A ⟧Type -> Maybe ℕ 
ex₂ Nat n = just (lower n) -- or (ex₂ Nat (lift n) = just n) 
ex₂ Prp t = nothing 

Nếu A : Set α sau đó Lift A : Set (α ⊔ ℓ) cho bất kỳ ℓ. Vì vậy, khi bạn có ℕ : Set và Set : Set₁, bạn muốn nâng ℕ từ Set tới Set₁, chỉ là Lift ℕ - trong trường hợp đơn giản, bạn không cần phải cung cấp ℓ một cách rõ ràng.

Để tạo thành phần dữ liệu được bao bọc trong Lift bạn sử dụng lift (như trong lift 0). Và để lấy lại yếu tố này, bạn sử dụng lower, do đó, lift và lower là các điểm nghịch đảo của nhau. Lưu ý rằng mặc dù lift (lower x) không nhất thiết phải nằm trong cùng một vũ trụ như x, vì lift (lower x) "làm mới" ℓ.

Answer 2

Để triển khai thực hiện "bắt nguồn Eq" trong Agda, bạn có thể xem qua sơ đồ khối của Ulf tại https://github.com/UlfNorell/agda-prelude. Đặc biệt, mô-đun Tactic.Deriving.Eq chứa mã để tự động tạo ra sự bình đẳng có thể giải quyết được cho một lớp dữ liệu khá đơn giản (đơn giản và được lập chỉ mục).