Interface issues: a tentative summary

[nicolabotta]

There are a number of open issues on interfaces that make it difficult to use interfaces and interface implementations. Some of these issues have been around for a while, others are relatively new. I am going to use this post to collect what seem (to me) the most obvious misbehaviors. I hope that this summary can help tackling the problems that affect interfaces more effectively. I am listing first those issues that seem more severe to me.

1) The type checker does not recognize certain Num implementations. This is issue 2830. On a fresh installation of https://github.com/nicolabotta/SeqDecProbs,
you should be able to do

cd SeqDecProbs-master/issue_reports/num_type_mismatch/
make

and get something like

Type mismatch between
        PNat (Type of _ + _)
and
        Subset (Nat, Subset Nat Positive) Normal (Expected type)

Replacing line 25 of "NonNegRationalTest.lidr" with

> z = x `plus` y

makes the program type check.

2) The type checker rejects multiple constraints that are refinements of the same interface. This is issue 2497. It makes it very cumbersome to use interfaces to define new interfaces and requires users to implement linear hierarchies like

> interface (Num t) => NumPlusZeroNeutral t where
> interface (NumPlusZeroNeutral t) => NumPlusAssociative t where
> interface (NumPlusAssociative t) => NumMultZeroOne t where
> interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where

instead of the more natural

> interface (Num t) => NumPlusZeroNeutral t where
> interface (Num t) => NumPlusAssociative t where
> interface (Num t) => NumMultZeroOne t where
> interface (Num t) => NumMultDistributesOverPlus t where

Please, see also issue 2498 and 3078!

3) Trivial interface declarations fail to type check with less than useful error messages. This is issue 2505. Since I first came across this problem, the error message has changed but has not become more understandable (to me). Please, see also issue 2053.

4) Implementing Show for sequences of dependent pairs: how to do it? This is issue 3113. Please also note the error message referring to Prelude.Show.idr!

[edwinb]

I've been through all of these now, and either fixed the misbehaviour, or established that Idris is doing the right thing (even if it is reporting the problem unhelpfully).

The main issue we need to consider from the language design point of view is what to do about diamond shaped interface hierarchies. I'm not going to change the core language, which means there is no way Idris is going to deduce that, for example, x, y : Num a -> x = y, but we should put some thought into how properties of such hierarchies should be dealt with.

[nicolabotta]

I see the possibility of a "multiple inheritance" problem here, but I would expect such problem to shoiw up when interfaces are implemented, not when they are declared.

The other thing is that, as I commented in #2497 and #3078, we have new errors with 0.11-git:7e7d0eb which I am not sure are directly related with this problem.

[ahmadsalim]

@edwinb Can't diamond shaped hierarchies in this case be solved with linearisation ?

[edwinb]

@ahmadsalim I don't know what you mean by linearisation here... do you have an example? Do you mean making the hierarchy linear? I think that can help... Generally if you need a specific implementation you could be precise about it in the type too (e.g. parameterising by an implementation).

The point is that Idris cannot make any assumptions about the path through an interface hierarchy, or whether one implementation is equal to another, purely based on types. The type theory doesn't support it, the possibility of named implementations further spoils it.

[ahmadsalim]

@edwinb Yeah, exactly. Like the C3 linearisation.

I understand the second part, which makes perfect sense.
However, I think it would be nice if we could at term level have a better equality on instances. When I last time made a Set that was indexed by a type class instance dictionary, it was even hard for me to show what would appear to be the same default implementation to be equal.

[edwinb]

@ahmadsalim Yes, reasoning about instances can be annoyingly awkward at the moment. Does naming the constructor help? Perhaps giving access to the name somehow would be useful...

[ahmadsalim]

@edwinb Sorry, it has been a long time now, but I thought that it might be a good idea to mention it while the idea was discussed. Perhaps giving access to the name might not be a bad idea :).

[ahmadsalim]

I believe that #2233 mentions that it would be nice if manually created instances could somehow be registered in interface resolution, which could be another alternative.

[ahmadsalim]

One syntax could be

%hint implementation
a : P
a = ...

Where P may only depend on implicit parameters (perhaps with default/auto arguments).
I am unsure how one would report an error if using such implementation fails because implicits could not be solved however.

[mrkgnao]

This works:

NatSemigroupAdditive : Semigroup Nat NatPlus
NatSemigroupAdditive = MkSemigroup undefined

but not

[NatSemigroup]
Semigroup Nat NatPlus where
  composition_associative = undefined

NatPlus is a wrapper for the (+) operation on Nats, so the implementation complains about it not being a "type or data constructor". But the explicit impl with MkSemigroup works. What gives?

(I'd be sorry to find out that the implementation shouldn't work as part of expected behavior. Oh well.)

[mrkgnao]

This compiles:

interface SemigroupL (a : Type) (impl : Type) | w where

even though w appears nowhere either in the head or the methods of the interface.

Edit: I feel such "phantom" constraining parameters might have interesting uses if combined with named implementations or the "using" syntax.

[mrkgnao]

One very nice thing would be, given the following code,

interface
    (am : Monoid a zero add, mm : Monoid a one mul)
  => Semiring (a : Type) (zero : a) (add : Type) (one : a) (mul : Type)
   | a, add, mul
  where

to make am and mm available in the body of the interface's default implementation.

I'm not sure if that's actually sensible considering the scope for multiple implementations, but this:

(eq : Eq a) => Eq (Vect n a) where
   (==) = (===) @{eq}

would really be nice. This kind of "parametric" generation of instances is moving into ML module functor territory, I suppose (although I don't know anything about those!), but it's really weird to be able to name the constraints in my first example and then not use them at all (outside of the determining parameters, as I've discovered:

interface
    (monoid : Monoid a e tag)
  => AbelianGroup (a : Type) (e : a) (tag : Type)
   | a, tag, monoid {- e? -}
  where

This typechecks.)

Edit: Oh, apparently the named constraints are available in some cases. But they're hard to work with.

[mrkgnao]

Here's an amusing one that seems like a bug or a syntax limitation.

interface
   ( ring : Ring a zero add one mul
   , ab   : AbelianGroup' a one mul zero)
  => Field
       (a : Type)
       (zero : a) (add : Type)
       (one : a) (mul : Type)
   | a
  where
  (+...) : a -> a -> a
  (+...) = (+..)
  (*...) : a -> a -> a
  (*...) = (*..)

Trying to do a deriving instance-like

implementation Field Double 0.0 Add 1.0 Mul where
  -- empty

makes Emacs pronounce this implementation a hole. But adding a parameter lol : a to the interface, and then doing

implementation Field Double 0.0 Add 1.0 Mul where
  lol = 1.0

works fine.

[nicolabotta]

I am completely lost with Idris interfaces at this point. To the issues mentioned in my original post, #3727 has come on board and has forced me to downgrade to 0.99. I thought that, first and foremost, interfaces were designed to improve code understandability and support name overloading. I do not understand the | notation and some of the constructions presented by mrkgnao. His findings seem a bit worrying. Perhaps time for me to go back to Haskell?

[ahmadsalim]

@nicolabotta I understand your frustration, and we highly appreciate your bug reports.
I think that it takes some time to resolve Idris issues, since there are not many full-time developers on the project (must of us being volunteers).

Regarding, #3727 I think that this is currently a limitation in Idris which hopefully will be resolved at some point if we get better unification; a workaround is to inline the given type definition.
The | construct allows you to choose which parameters should be the determining ones in the implementation resolution mechanism when having a multi-argument interface (a light-weight alternative to the Haskell functional dependencies).

[nicolabotta]

Ahmad, could you please elaborate a little bit on #3727? I do not know a workaround for the issue and I am still torn between rewriting IdrisLibs to make it comply with 1.0 and staying with 0.99. If a workaround is available, I could try to upgrade without braking too much legacy code.

Thanks for the | explanations! Is there some documentation on this construct?

I understand that Idris is a collaborative project. My frustration comes from the fact that the two basic idioms for organizing programs -- modules and interfaces -- have been struggling with more or less the same issues since years. This makes it very difficult (for me) to write maintainable code in Idris. It is possible that I am doing something fundamentally wrong, of course. Best, Nicola

[ahmadsalim]

@nicolabotta The documentation for | is here: http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#determining-parameters

[mrkgnao]

@nicolabotta I think I should say that it wasn't my intention to say "look, Idris is broken!" but rather to provide as much data as I could for people familiar with the internals. It was to help them figure out if there were any underlying causes that could be dealt with easily to fix a bunch of interface quirks at once.

The problem is that many, many features have been added that are not on the Idris docs website (which, of course, I understand the reasons for) and they are obviously interacting in nontrivial ways whose shortcomings have not yet been identified completely -- especially since I think that most users exercise either the proofish/Agda side of things, or the low-level Buffer-like code, instead of all this messing around with passing interface implementations around :)

[atacratic]

FWIW, an example of a diamond inheritance problem, taken from #3791:

-- idris 1.0
-- idris --noprelude

module Main

interface A a where
  p : a

interface A a => B a where
  q : (x : a) -> (x = Main.p) -> a

interface A a => C a where

interface (B a, C a) => D a where
  e : (x : a) -> (y : x = Main.p) -> q x y = Main.p

...producing:

t.idr:14:11:When checking type of Main.e:
Can't find implementation for Main.A bqty

Possible cause:
        t.idr:15:40:When checking an application of function Main.q:
                Type mismatch between
                        (=) {A = a}
                            {B = a}
                            x
                            (Main.p {a = a}
                                    {{constructor of Main.C#A a {a = a}
                                                                {{constructor of
 Main.D#C a a

            _}}}}) (Type of y)
                and
                        (=) {A = a}
                            {B = a}
                            x
                            (Main.p {a = a}
                                    {{constructor of Main.B#A a {a = a}
                                                                {{constructor of
 Main.D#B a a

            _}}}}) (Expected type)

                Specifically:
                        Type mismatch between
                                Main.p {a = a}
                                       {{constructor of Main.C#A a {a = a}
                                                                   {{constructor
 of Main.D#C a a

               _}}}}
                        and
                                Main.p {a = a}
                                       {{constructor of Main.B#A a {a = a}
                                                                   {{constructor
 of Main.D#B a a

               _}}}}

[jeroennoels]

@atacratic It works in Idris 1.2 if you define C first and then B. Or equivalently, if B and C were defined in separate modules, it works if you import C first, then B.
I am not sure that this would still be a solution if the dependencies between the interfaces are more complicated. But I think at least we make progress here, as the following compiles and runs fine:

module Main

interface A a where
  p : a

interface A a => C a where

interface A a => B a where
  q : (x : a) -> (x = Main.p) -> a

interface (B a, C a) => D a where
  e : (x : a) -> (y : x = Main.p) -> q x y = Main.p

implementation A Integer where p = 42
implementation B Integer where q x _ = x
implementation C Integer where 
implementation D Integer where e x y = y

test : 42 = 42
test = e 42 Refl