Идрис - использовать тот же экземпляр интерфейса - PullRequest
Новая
       34

Идрис - использовать тот же экземпляр интерфейса

0 голосов
/ 21 февраля 2019

У меня есть структура данных 

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?

1 Ответ

0 голосов
/ 22 февраля 2019

«Правильное» решение этой проблемы требует (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
...