Overlapping implementations

[nicolabotta]

Elaborating on the example given in https://stackoverflow.com/questions/47464426/idris-eq-for-enumerated-type, I have tried to implement

> import Data.Vect

> %default total
> %access public export

> interface Enumerated (t : Type) (len : Nat) | t where
>   values : Vect len t
>   toFin  : t -> Fin len
>   values_match_toFin : map toFin values = range

> using (t : Type, len : Nat)
>   implementation (Enumerated t len) => Eq t where
>     x == y = toFin x == toFin y

This fails to type check with

- + Errors (1)
 `-- ./Enumerated/Enumerated.lidr line 12 col 19:
     Overlapping implementation: Eq () already defined

Is this the expected behavior? Is it an Idris error? How can I state that every implementation of Enumerated is also an implementation of Eq?

[ahmadsalim]

@nicolabotta I believe this is expected behavior, but the solution in your case should be quite simple. Just make Eq a super-interface of Enumerated.

[nicolabotta]

@ahmadsalim What do you mean by making Eq a super-interface of Enumerated? The point here is that, with Enumerated one can implement Eq implementations of types that are isomorphic to Fin n with a program of length n instead of n * n. For instance:

> data Sky = Sunny | Cloudy | Rainy
>
> implementation Enumerated Sky 3 where
>   values = [Sunny, Cloudy, Rainy]
>   toFin Sunny  = 0
>   toFin Cloudy = 1
>   toFin Rainy  = 2
>   values_match_toFin = Refl
>   
> implementation Eq Sky where
>   x  == y  = toFin x == toFin y

as suggested in the stackoverflow post. This is still very annoying because the last two lines of the example have to be rewritten over and over again for every type that is enumerated. This is tedious and a program like

> using (t : Type, len : Nat)
>   implementation Enumerated t len => Eq t where
>     x == y = toFin x == toFin y

seems a very natural mechanism for avoiding these repetitions altogether, at least to me.

I frankly do not understand why the original program should not be expected to type check. I understand that an implementation of Eq for Unit has already been provided in prelude/Prelude/Interfaces.idr. But this should not prevent deriving an implementation of Eq for every type for which an implementation of Enumerated is available.

The type checker complain when one tries to use (==) for a type for which two or more implementations of Eq are available, but this does not happen here. In the case (==) is used for a type for which two or more implementations of Eq are available, the type checker should report an ambuguity and the programmer should be able to resolve such ambiguity by fully qualifying the implementation.

[ahmadsalim]

@nicolabotta So Idris unlike Haskell, currently forbids overlapping instances.

But in your case you could write something like

interface Eq t => Enumerated (t : Type) (len : Nat) | t where
   values : Vect len t
   toFin  : t -> Fin len
   values_match_toFin : map toFin values = range

You may also be able to give a default implementation of Eq in here, but I forgot whether that works in Idris or not.

[nicolabotta]

@ahmadsalim As explained in my previous post, the whole point of the exercise is not to derive implementations of Enumerated from implementations of Eq but rather to derive implementations from Eq from implementations of Enumerated!

I understand that Idris forbids overlapping instances but I believe that this basically sucks. I have tried to use interfaces in Idris for about 5 years and I have to conclude that I never managed to do so in a profitable way, see, among others #4194 and the many issue reports on interfaces preceding it. #4194 is also the reason why I am still stuck with Idris 0.99.

The fact that Prelude implementations of Prelude interfaces prevent users from being able to derive implementations of those interfaces is, in my view, a major design mistake.

[ahmadsalim]

@nicolabotta Maybe, this is something worth discussing with @edwinb regarding Blodwen, when the time arrives.

I do understand the frustration and agree that there are things to improve regarding interfaces. Unfortunately I do not hold much sway regarding design and I am unsure how much effort is required regarding extending the interface implementation.

[nicolabotta]

@ahmadsalim I understand, thanks for looking into this issue! Best, Nicola

[edwinb]

It's expected behaviour, but you're right, it is annoying (I've been bitten by it myself a couple of times recently, so familiar with the annoyance...). The problem would be that, if you add an instance of Enumerated for a type which already has an Eq implementation, which should Idris choose?

Incidentally, Haskell only allows this sort of thing with UndecidableInstances (I've just tried it).

I have tried a hack around this, which is the %overlapping flag on an instance, and makes the above snippet compile:

using (t : Type, len : Nat)
  %overlapping
  implementation (Enumerated t len) => Eq t where
    x == y = toFin x == toFin y

I'm not convinced it's a good idea, though. And I really don't think it's fair to say it sucks to prioritise predictable behaviour from the compiler over absolute convenience - in the past I have sometimes preferred the latter, but it has led to surprising problems too often. So, we should try to find a non hacky solution.

Blodwen is gathering pace. It'll soon be time to think seriously about how interfaces should work.

[edwinb]

By the way, I do think this pattern is a legitimate thing to do as long as it's the only implementation of Eq for types which implement Enumerated. But I don't know a good, efficient, way to check that, and the elaborator is already too slow.

[ahmadsalim]

@edwinb Would default super-interfaces not solve this issue?
Now that I recall, I believe we have some support for them, but I do not remember whether they work correctly or not.

[ahmadsalim]

Another thing one could consider is to allow that super-interfaces are added later provided they are given a default implementation using sub-interfaces. This may be easier to check than arbitrary constraints, but still requires some work.

[nicolabotta]

@edwinb Thanks for looking into this issue Edwin! The reason why I am saying that forbidding overlapping interfaces sucks is that it makes it practically impossible to use interface derivation in a profitable way.

Logically, it is as if a proof that 3 < 5 somewhere in the Prelude would prevent one from being able to prove that n < n + 2 for every n in a user-specific module. This would be, I think, hardly acceptable.

I have probably developed the specific skill of trying to use Idris interfaces in ways they are not meant to be used. As a matter of fact, most of the times I try to use interfaces, I run into issues that seem to be hard to fix. That was the case with #3727 that kept me on 0.99 from April 2017 until November and then with #4194 that still keeps me on that Idris version.

I have probably very naive expectations but, in the specific case, I would think that whenever the type checker runs into an overlapping implementation of an interface, it just turn it into a named implementation.

If it subsequently happens to run into expressions that use a member of that interface, i would expect the type checker to report an ambiguous usage of that member and require the programmer to resolve the ambiguity with an using directive. If not, there should be no problem.

[edwinb]

Hmm, so this does work, and I think it's what @ahmadsalim is suggesting:

interface Eq t => Enumerated (t : Type) (len : Nat) | t where
  implementation Eq t where
    x == y = toFin x == toFin y
  values : Vect len t
  toFin  : t -> Fin len
  values_match_toFin : map toFin values = range

So, when you implement Enumerated, if there isn't already an Eq instance then it'll create one for you. It does, however, mean that you have to know when you write the Enumerated interface that it always needs an Eq instance.

It's probably a better solution than my %overlapping hack, at least.

[nicolabotta]

@edwinb Thanks, I was not aware of this possibility! I will have to understand what it means and how to use it.