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

对此的“正确”解决方案需要（1）写一个形式(m1 : Monoid m, m2 : Monoid m) => m1 = m2的证明和2）能够从Monoid重新实现两个funcRespId实现以将它们提供给步骤1.虽然前者可以用假设/断言模拟，这是后一步成为问题，这可能与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