Idris

Question

我有一个数据结构

record IdentityPreservingMorphism domain codomain where
constructor MkMorphismOfMonoids
  func : domain -> codomain
  funcRespId : (Monoid domain, Monoid codomain) => func (Algebra.neutral) = Algebra.neutral

这只是说 IdentityPreservingMorphism 是幺半群之间的态射，需要尊重身份。

我试图证明恒等态射是 IdentityPreservingMorphism

monoidIdentity : Monoid m => MorphismOfMonoids m m
monoidIdentity = MkMorphismOfMonoids
  id
  ?respId

?respId 在 Refl 的简单拍摄无效，因为可用的 Monoid 实例太多。我如何告诉编译器我只想使用来自 monoidIdentity 定义的实例？

Answer 1

对此的 "proper" 解决方案需要 (1) 编写形式证明 (m1 : Monoid m, m2 : Monoid m) => m1 = m2 和 2) 能够从 funcRespId 中具体化两个 Monoid 实现将它们输入到步骤 1 中。虽然前者可以用 postulate/assert 模拟，但后者会出现问题，这可能与 https://github.com/idris-lang/Idris-dev/issues/4591 有关。

一个更简单的解决方法是通过直接在记录中存储实现来简化具体化：

record MorphismOfMonoids domain codomain where
  constructor MkMorphismOfMonoids
  func : domain -> codomain
  mon1 : Monoid domain
  mon2 : Monoid codomain
  funcRespId : func (Algebra.neutral @{mon1}) = Algebra.neutral @{mon2}

monoidIdentity : Monoid m => MorphismOfMonoids m m
monoidIdentity @{mon} = MkMorphismOfMonoids id mon mon Refl

Idris - 使用相同的接口实例

Idris - use same interface instance

monoids