有沒有一種方法可以像在 Haskell 中一樣提供 Coq 型別類方法的默認實作？我在 Coq 型別類檔案中沒有看到任何提及。如果不存在這樣的功能，是否有模擬這種行為的通用模式？
uj5u.com熱心網友回復：
默認實作可以被視為一個函式，它在給定其他提供的方法的情況下構造默認方法。所以你可以定義一個函式。
Class C a :=
{ m1 : a
; m2 : a
}.
(* Construct an instance of C from an implementation of only m1. *)
Definition mkC {a} (m1_ : a) := {| m1 := m1_ ; m2 := m1_ |}.
#[global]
Instance C_nat : C nat := mkC 0.
另一個想法是將類分解為單一方法類。然后，您可以先為顯式實作的方法定義實體，然后再次使用函式獲取其他方法的默認實作。通過這種方式分解類，您無需將默認函式顯式應用于提供的方法。
Class N1 a :=
n1 : a.
Class N2 a :=
n2 : a.
(* Default implementation of N2 using N1 *)
Definition defaultN2 {a} {_ : N1 a} : N2 a := n1 (a := a).
#[global]
Instance N1_nat : N1 nat := 0.
#[global]
Instance N2_nat : N2 nat := defaultN2. (* N1 nat is passed implicitly here *)
uj5u.com熱心網友回復：
我希望您可以這樣做，但不支持。
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/517126.html
標籤：哈斯克尔库克类型类