Interface resolution bug

[edwinb]

Issue by nickdrozd
Wednesday May 06, 2020 at 22:33 GMT
Originally opened as edwinb/Idris2-boot#356

---

Steps to Reproduce

Stick this code at the bottom of Prelude.idr:

interface Semigroup a => VerifiedSemigroup a where
  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
  monoidNeutralIsNeutralL : (l : a) -> l <+> Prelude.neutral = l
  monoidNeutralIsNeutralR : (r : a) -> Prelude.neutral <+> r = r

mtimes : Monoid a => (n : Nat) -> a -> a
mtimes Z x = Prelude.neutral
mtimes (S k) x = x <+> mtimes k x

mtimesTimes : VerifiedMonoid a => (x : a) -> (n, m : Nat) ->
  mtimes (n + m) x = mtimes n x <+> mtimes m x
mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes m x
mtimesTimes x (S k) m =
  rewrite mtimesTimes x k m in
    semigroupOpIsAssociative x (mtimes k x) (mtimes m x)

Expected Behavior

No problem

Observed Behavior

mtimesTimes fails with this error:

Prelude.idr:1703:5--1704:1:While processing right hand side of mtimesTimes at Prelude.idr:1701:1--1704:1:
Can't solve constraint between:
	Constraint (Semigroup a) (let 0 _ = \{rwarg:8186} => x <+> rwarg = (x <+> mtimes k x) <+> mtimes m x in let 0 _ = mtimesTimes x k m in Constraint (VerifiedSemigroup a) conArg)
and
	Constraint (Semigroup ty) (Constraint (Monoid a) conArg)

But the proof itself is fine, and it goes through with this change:

-mtimes : Monoid a => (n : Nat) -> a -> a
+mtimes : VerifiedMonoid a => (n : Nat) -> a -> a

mtimes, with the Monoid constraint, says, if you implement those syntactic elements, you get to use this syntactic element. mtimesTimes, with the VerifiedMonoid constraint, says, if you further prove certain guarantees about the behavior of those syntactic elements, you also get some guarantees about the behavior of this new element. So the "verified" constraint shouldn't be necessary for defining mtimes, because mtimes doesn't make any guarantees about behavior.

The inheritance structure looks like this:

Semigroup  -------------->  Monoid

    |	                      |
    |	                      |
    |	                      |
    |	                      |
   \/                        \/

VerifiedSemigroup  ------>  VerifiedMonoid

This bug is in Idris 1 too.

[edwinb]

Comment by edwinb
Thursday May 07, 2020 at 11:34 GMT

---

Diamond shaped inheritance structures are awkward because implementations of the same interface aren't guaranteed to be equal. There's a bit of noise in the error message, but it looks like it doesn't know whether to go to Semigroup via Monoid or VerifiedSemigroup.

So, this code as it stands isn't going to work without some modification. This diamond issue is a pain and I don't know if anyone has found a nice solution for this sort of problem (with proofs) yet.

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

[edwinb]

Comment by nickdrozd
Thursday May 07, 2020 at 14:02 GMT

---

I'm pretty sure this is what's responsible for blocking the proof at https://github.com/idris-lang/Idris-dev/pull/4848/files#diff-fb2a7c0a9ce133762a38755823a01d7aR73.

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

MonoidV would be economical in terms of characters, and it also looks decent. GroupV, RingV, etc. I would be happy to implement that change on the Idris 1 side.

[edwinb]

Comment by nickdrozd
Thursday May 07, 2020 at 14:05 GMT

---

This change does not fix the issue, or even affect the error message:

-interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
+interface (Monoid a, VerifiedSemigroup a) => VerifiedMonoid a where

[edwinb]

Comment by faserprodukt
Friday May 08, 2020 at 01:09 GMT

---

So, this code as it stands isn't going to work without some modification. This diamond issue is a pain and I don't know if anyone has found a nice solution for this sort of problem (with proofs) yet.

@edwinb I'm not sure if this fits the problem, but the comment reminds me of the recent Tabled Typeclass Resolution paper.

[edwinb]

Comment by Sventimir
Thursday May 14, 2020 at 17:45 GMT

---

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

@nickdrozd once suggested in a dicussion on Idris-dev repo, that these interfaces should actually be merged together (i.e. Semigroup with VerifiedSemigroup and so on). This would solve the problem of naming and remove the diamond-shaped inheritance pattern. In my opinion this is the way to go.

[gallais]

Another alternative would be to index the verified version by the raw one.
Like so:

public export
interface SemigroupV ty (sem : Semigroup ty) where
  semigroupOpIsAssociative : (l, c, r : ty) ->
    l <+> (c <+> r) = (l <+> c) <+> r

However trying to give an implementation for this interface currently
makes the typechecker loop.

More pressing matter: Should we remove contrib's Control.Algebra?
It is utterly unusable because of this diamond problem and can only trick
people into rediscovering this issue the hard way by going through a lot
of confusing and frustrating error messages.

[nickdrozd]

More pressing matter: Should we remove contrib's Control.Algebra?
It is utterly unusable because of this diamond problem and can only trick
people into rediscovering this issue the hard way by going through a lot
of confusing and frustrating error messages.

IMO the value of that code is to illustrate how dependent types can be
used in math proofs. Of course proving math stuff is not the primary
use case for Idris, but nonetheless the language affords formal
proofs, and Control.Algebra shows how that can be done. I think
deleting it would leave the library poorer. Sure, there are some
difficulties, but those should be viewed as opportunities rather than
problems.

[gallais]

"Some difficulties" being that it's unusable to prove anything
at all and produces errors impossible to understand.

There are actual proofs in the library and the fact that they
are valid & usable is a better demonstration of the language's
abilities IMO.

[nickdrozd]

"Some difficulties" being that it's unusable to prove anything at all

I'm not sure what you mean. Lots of things are proved there. It's proved that monoids have unique inverses. Cancellation and unique solution laws are proved for groups. It's proved that group homomorphisms preserve neutrals and inverses. In Idris 1 it was possible to prove that the inverse operation is distributive in commutative groups. Last I checked it wasn't possible in Idris 2, but again, that's an opportunity for improvement.

@Sventimir What do you think?

[Sventimir]

@gallais is probably right in that the code shouldn't be left in the current state. However, a few solutions have been proposed and I don't think that deleting the module is the best one. In my opinion we should just merge these Verified interfaces into their "unverified" counterparts. This would have the following benefits:

• simplify the inheritance structure, avoiding nasty diamonds.
• make the code more clear and easier to understand.
• fix the situation where you can implement a group or a monad that doesn't fully conform to its appropriate axioms.

A possible danger may be in that some existing implementations might require extensions to prove that they actually obey these axioms (which may or may not have been proven so far). This might require more work than it seems, but hopefully shouldn't break anything, so it would all be to the good.

[gallais]

However, a few solutions have been proposed and
I don't think that deleting the module is the best one.

I am not saying it's the best one but it is a first step and it is
compatible with other solutions: they can start from a clean slate.
Changing the definitions of semigroup, monoid, functor, applicative,
monad, bifunctor, etc. to include laws will entail a lot of work on
the Idris2 compiler itself to prove these laws & keep the bootstrapping
path given you're modifying something in the Prelude.

In the meantime I think it makes sense to remove the code that lulls
you into trying to use it only to struggle with incomprehensible error
messages & eventually rediscover this issue. This has been my experience
trying to work with MonoidV in Data.Monoid.Exponentiation.

[ohad]

In my opinion we should just merge these Verified interfaces into their "unverified" counterparts.

This opinion is actually quite extreme and radical in the programming language landscape. I am not comfortable with following up on this decision in the language's standard library, even under contrib.

A moderate way forward would be to create a copy somewhere visible, say as a project with the Idris Community organisation until we have a mature proposal for a usable Verified hierarchy. Then it becomes a concrete proposal.

[rvs314]

I apologize if this is a dead issue or discussion has been moved elsewhere, but it seems like you can flatten the diamond issue (at least in the case @nickdrozd points out) by having MonoidV implement Monoid rather than have Monoid be a requirement for MonoidV. Here's the original example rewritten in a way that typechecks as of Idris 2, version 0.6.0-936b7270a:

module Ex

%default total

interface SemigroupV ty where
  (<+>) : ty -> ty -> ty
  semigroupOpIsAssociative : (l, c, r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r
 
interface SemigroupV ty => MonoidV ty where
  neutral : ty
  monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral = l
  monoidNeutralIsNeutralR : (r : ty) -> neutral <+> r = r

SemigroupV ty => Semigroup ty where
  (<+>) = Ex.(<+>)

MonoidV ty => Monoid ty where
  neutral = Ex.neutral

%hide Ex.(<+>)

mtimes : Monoid a => (n : Nat) -> a -> a
mtimes Z x = Prelude.neutral
mtimes (S k) x = x <+> mtimes k x

mtimesTimes : MonoidV a => (x : a) -> (n, m : Nat) ->
  mtimes (n + m) x = mtimes n x <+> mtimes m x
mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes m x
mtimesTimes x (S k) m =
  rewrite mtimesTimes x k m in
    semigroupOpIsAssociative x (mtimes k x) (mtimes m x)

This requires a bit more code than the original, and because of (what I believe to be) #2244, I can't exclude the redundant <+> operator without %hide-ing it manually.

[buzden]

it seems like you can flatten the diamond issue (at least in the case @nickdrozd points out) by having MonoidV implement Monoid rather than have Monoid be a requirement for MonoidV.

What you suggest would lead to ambiguity errors for all types which already implement Monoid and have also MonoidV in all functions that require Monoid, because you can get it either directly or via you suggested universal implementation.

[rvs314]

The idea is that types in the stdlib which can be proven to follow the appropriate laws wouldn't have a direct Monoid instance - they'd just have a MonoidV instance which would then derive their Monoid instances indirectly.

[emdash]

The idea is that types in the stdlib which can be proven to follow the appropriate laws wouldn't have a direct Monoid instance - they'd just have a MonoidV instance which would then derive their Monoid instances indirectly.

Total outsider here, but to the degree that I understand any of this, it seems plausible.