Idris - 使用相同的接口实例

【问题标题】：Idris - use same interface instanceIdris - 使用相同的接口实例
【发布时间】：2019-07-15 17:04:55
【问题描述】：

我有一个数据结构

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

?respIdRefl 的简单操作不起作用，因为可用的Monoid 实例太多。如何告诉编译器我只想使用来自monoidIdentity 定义的实例？

【问题讨论】：

标签： idris monoids

【解决方案1】：

对此的“正确”解决方案需要 (1) 编写表单证明 (m1 : Monoid m, m2 : Monoid m) => m1 = m2 和 2) 能够从 funcRespId 中具体化两个 Monoid 实现以将它们提供给步骤 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

【讨论】：

非常有趣。 +1