解决精益中的“钻石继承”类

Question

对于精益，我有一个非常基本的循环结构。我构造了一个岩浆类、一个准群（抵消岩浆）类和一个整体岩浆类。从那里开始，一个循环就是一个既是准群又是单位岩浆的东西。

在 Haskell 中，这看起来像

class Magma a where
  add :: a -> a -> a

class Magma a => Unital a where
  unit :: a

class Magma a => Quasigroup a where
  left_div :: a -> a -> a
  right_div :: a -> a -> a

class (Quasigroup a, Unital a) => Loop a

所以我试着把它翻译成精益：

universe u

class magma (α : Type u) :=
  ( add : α → α → α )

class unital (α : Type u) extends magma α :=
  ( unit : α )
  ( left_id : ∀ a : α, add unit a = a )
  ( right_id : ∀ a : α, add a unit = a )

class quasigroup (α : Type u) extends magma α :=
  ( left_div : α → α → α )
  ( right_div : α → α → α )
  ( left_cancel : ∀ a b : α, add a (left_div a b) = b )
  ( right_cancel : ∀ a b : α, add (right_div b a) a = b )

class loop (α : Type u) extends quasigroup α, unital α

但精益抱怨：

invalid 'structure' header, field 'to_magma' from 'unital' has already been declared

这很神秘，但如果我们玩弄一些东西，就会发现这是某种类似于钻石继承的问题。不喜欢我们从loop到magma做了两条路径。

我怎样才能判断出这些是同一个岩浆并解决这个问题？

Answer 1

在精益 3.35.1 中，您有几种可能的解决方案。对于类似 Haskell 的记录合并，有old_structure_cmd：

universe u

class magma (α : Type u) :=
(add : α → α → α)

class unital (α : Type u) extends magma α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

class quasigroup (α : Type u) extends magma α :=
(left_div : α → α → α)
(right_div : α → α → α)
(left_cancel : ∀ a b : α, add a (left_div a b) = b)
(right_cancel : ∀ a b : α, add (right_div b a) a = b)

set_option old_structure_cmd true

class loop (α : Type u) extends quasigroup α, unital α.

这将按您的预期工作。然而，old_structure_cmd 的缺点是结构都“扁平化”并且尺寸变大。 “新”方式是拥有一个主“主干”结构，并创建分支继承：

universe u

class magma (α : Type u) :=
(add : α → α → α)

class unital (α : Type u) extends magma α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

class quasigroup (α : Type u) extends magma α :=
(left_div : α → α → α)
(right_div : α → α → α)
(left_cancel : ∀ a b : α, add a (left_div a b) = b)
(right_cancel : ∀ a b : α, add (right_div b a) a = b)

class loop (α : Type u) extends quasigroup α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

instance loop.to_unital {α : Type u} [h : loop α] : unital α :=
{ ..h }