Idris2: How to specify named implementation as input to default implementation?

[James Cook]

Hi idris-lang,

Suppose I've got

    concatList : Monoid a => List a -> a

Then I can define sumList using:

    sumList : Num a => List a -> a
    sumList = concatList @{Additive}

But what if I want to write:

    sumAndConcat : Monoid a, Num b => List (a, b) -> (a, b)
    sumAndConcat = concatList @{???}

Is there anything I can replace "???" with that will make it work?


According to this "Auto implicit arguments" section, the compiler tries "Local variables, i.e. names bound in pattern matches or let bindings, with exactly the right type.". So, I tried this:

    sumAndConcat : Monoid a => Num b => List (a, b) -> (a, b)
    sumAndConcat =
      let monoidImpl : Monoid b
      monoidImpl = Additive
      in concatList

My hope was that since monoidImpl is available to search, Idris2 will be able to combine that with the default Monoid (a, b) implementation. But it didn't work: Idris2 says "Can't find an implementation for Monoid (a, b)".


I found this in Prelude:

sum : (Foldable t, Num a) => t a -> a
sum = concat @{(%search, Additive)}

Is "%search" documented anywhere? Can it be used to accomplish what I want?


My actual use case is slightly more complicated. I've implemented a mapping type with a default value, called "DefaultMap", and have a default implementation:

  Ord k => Monoid v => DecEq v => (d : v) => (d = Prelude.Interfaces.neutral) =>  Monoid (DefaultMap k v d) where

but I am having trouble getting Idris2 to use it when v = Int.

[James Cook]

I'm getting ahead of myself. The following doesn't work at the repl:

    Main> concat [((), ()), ((), ())]
    Error: Can't find an implementation for Monoid ((), ()).

    (Interactive):1:1--1:28
     1 | concat [((), ()), ((), ())]
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Prelude.Interfaces has default implementations for Monoid () and for Monoid a => Monoid b => Monoid (a, b). Am I being overly optimistic in expecting it to combine those? Or is the above behaviour a bug?

[Stefan Höck]

Can you print the output of `Idris2 --version`? When I try the example
below at the REPL, I get the following:

Main> concat [((),()), ((),())]
((), ())

Right now, I'm using Idris 2, version 0.5.1-bf0a15725.

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/ed2e7795-99aa-4f1f-9926-ad8f48586fa1n%40googlegroups.com.

[James Cook]

Hm, I might have some local changes to the libraries.

falsifian angel-dfly ~ $ idris2 --version

Idris 2, version 0.4.0

but that doesn't necessarily tell the whole story.

I will re-build everything at a later version, and report back.

[Denis Buzdalov]

According to this "Auto implicit arguments" section, the compiler tries "Local variables, i.e. names bound in pattern matches or let bindings, with exactly the right type.". So, I tried this:

    sumAndConcat : Monoid a => Num b => List (a, b) -> (a, b)
    sumAndConcat =
      let monoidImpl : Monoid b
      monoidImpl = Additive
      in concatList

My hope was that since monoidImpl is available to search, Idris2 will be able to combine that with the default Monoid (a, b) implementation. But it didn't work: Idris2 says "Can't find an implementation for Monoid (a, b)".

Wow, that's strange. But if you use a typed value instead of a function in the `let`-block, all typechecks as you expect:

sumAndConcat : (Monoid a, Num b) => List (a, b) -> (a, b)      

sumAndConcat =                                                                                                                                                      
  let u : Monoid b = Additive in                                                                                                                                  
  concatList

[James Cook]

Okay, I rebuilt at git commit bf0a15725 (0.5.1).

concat [((), ()), ((), ())] works now (repl says ((), ())). And I can confirm Denis's observation. Thanks!

I still haven't figured out an answer for my real question, which is a bit more complicated.

I can work around the problem easily enough, but if anyone feels like diving into the problem, here it is:

---

Here is a new example. The following compiles:

    data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Semigroup (DefaultMap k v d) where
      (<+>) = ?todo0

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Monoid (DefaultMap k v d) where
      neutral = ?todo1

    %hint
    monoidInt : Monoid Int
    monoidInt = Additive

    f : DefaultMap String Int (the Int 0)
    f = neutral

(Note: I tried simplifying the Semigroup implementation to "Monoid v => Semigroup (DefaultMap k v (the v Prelude.Interfaces.neutral)) where", but then the compiler said it couldn't find a Semigroup implementation to go with the Monoid implementation.)

I would like to be able to get rid of the %hint, since it affects other places in the code. But I can't quite seem to make it work. Simply saying "f = let monoidInt : Monoid Int = Additive in neutral" doesn't do it: "Can't find an implementation for Monoid (DefaultMap String Int (the Int 0))"

Here's  a more involved attempt

    data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Semigroup (DefaultMap k v d) where
      (<+>) = ?todo0

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Monoid (DefaultMap k v d) where
      neutral = ?todo1

    f : {d : Int} -> {eq : d = Prelude.Interfaces.neutral @{Additive}} -> DefaultMap String Int d
    f = let monoidInt : Monoid Int := Additive
        in neutral

This still gives:

Error: While processing right hand side of f. Can't find an implementation      
for Monoid (DefaultMap String Int d).

I also tried the following, which adds an explicit "dIsNeutral" local variable with value d = neutral. It also replaces (d = Prelude.Interfaces.neutral) with a more explicit (d = Prelude.Interfaces.neutral @{m}) in the Monoid implementation, just to be more sure we're talking about the same implementation.

    data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Semigroup (DefaultMap k v d) where
      (<+>) = ?todo0

    (m : Monoid v) => (d : v) => (d = Prelude.Interfaces.neutral @{m}) => Monoid (DefaultMap k v d) where
      neutral = ?todo1

    f : {d : Int} -> {eq : d = Prelude.Interfaces.neutral @{Additive}} -> DefaultMap String Int d
    f = let monoidInt : Monoid Int := Additive
            dIsNeutral : (d = Prelude.Interfaces.neutral @{monoidInt}) := eq
        in neutral

But this gives:

Error: While processing right hand side of f. Can't solve constraint            
between: 0 and neutral.

pointing to the "eq" identifier implementing dIsNeutral.

[Denis Buzdalov]

I also tried the following, which adds an explicit "dIsNeutral" local variable with value d = neutral. It also replaces (d = Prelude.Interfaces.neutral) with a more explicit (d = Prelude.Interfaces.neutral @{m}) in the Monoid implementation, just to be more sure we're talking about the same implementation.

    data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

    Monoid v => (d : v) => (d = Prelude.Interfaces.neutral) => Semigroup (DefaultMap k v d) where
      (<+>) = ?todo0

    (m : Monoid v) => (d : v) => (d = Prelude.Interfaces.neutral @{m}) => Monoid (DefaultMap k v d) where
      neutral = ?todo1

    f : {d : Int} -> {eq : d = Prelude.Interfaces.neutral @{Additive}} -> DefaultMap String Int d
    f = let monoidInt : Monoid Int := Additive
            dIsNeutral : (d = Prelude.Interfaces.neutral @{monoidInt}) := eq
        in neutral

But this gives:

Error: While processing right hand side of f. Can't solve constraint            
between: 0 and neutral.

Yeah, this is expected because `monoidInt` being defined not as function does not reduce to the RHS, i.e. to `Additive`.

You can use `Syntax.WithProof` trick. That is, this typecheks:

```

import Syntax.WithProof

data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

(m : Monoid v) => (d = neutral @{m}) => Semigroup (DefaultMap k v d) where

  (<+>) = ?todo0

(m : Monoid v) => (d = neutral @{m}) => Monoid (DefaultMap k v d) where
  neutral = ?todo1

f : {d : Int} -> {auto eq : d = neutral @{Additive}} -> DefaultMap String Int d
f = let (monoidInt ** meq) : (m : Monoid Int ** _) := @@ Monoid.Additive in
    let x : (d = neutral @{monoidInt}) := rewrite sym meq in eq in
    neutral

```

[James Cook]

Thanks, that was very helpful. I didn't realize the two let syntaxes were so different (but now I've read this and this.)

For future reference: based on your example, I wrote this:

IntMap : Type -> Type
IntMap key = DefaultMap key Int (the Int 0)

additiveIntMap : Ord k => Monoid (IntMap k)
additiveIntMap =
   let (monoidInt ** meq) : (m : Monoid Int ** Additive = m) = @@Additive in
   let (defaultValue ** deq) : (d : Int ** 0 = d) := @@0 in
   let eqAdditive : (defaultValue = Prelude.Interfaces.neutral @{Additive}) := sym deq in
   let eq : (defaultValue = Prelude.Interfaces.neutral @{monoidInt}) := replace {p = (\i => defaultValue = Prelude.Interfaces.neutral @{i})} meq eqAdditive in
   replace {p = \d => Monoid (DefaultMap k Int d)} (sym deq) %search

and then all I need is:

f : IntMap String
f = let impl : Monoid (IntMap String) = additiveIntMap in neutral

That was fun, but as a practical matter, I might switch to something simpler. E.g. removing the "default" argument to DefaultMap and forcing the default to always be neutral. I did that before and it was much less fuss.

[Denis Buzdalov]

Yeah, but that's all too complicated. Showing you the `WithProof` trick, I pushed you in the wrong direction because I forgot about *local hints*. Local functions can be marked as hints and local functions reduce well.

Look at these, it's better:

```

data DefaultMap : (k : Type) -> (v : Type) -> (defaultValue : v) -> Type where

(m : Monoid v) => (d = neutral @{m}) => Semigroup (DefaultMap k v d) where
  (<+>) = ?todo0
                                                      
(m : Monoid v) => (d = neutral @{m}) => Monoid (DefaultMap k v d) where
  neutral = ?todo1
                                                 
f : {d : Int} -> {auto eq : d = neutral @{Additive}} -> DefaultMap String Int d

f = let %hint
        monoidInt : Monoid Int
        monoidInt = Monoid.Additive
    in neutral       

IntMap : Type -> Type
IntMap key = DefaultMap key Int 0

additiveIntMap : Ord k => Monoid (IntMap k)
additiveIntMap =

   let %hint

       monoidInt : Monoid Int
       monoidInt = Additive                                                                 

   in %search

```

пн, 27 сент. 2021 г. в 03:10, James Cook <fals...@falsifian.org>:

--

You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/09875e2a-b3a5-4a00-b26f-03f723bd8372n%40googlegroups.com.

[James Cook]

Much better, thanks! Maybe I will continue to use it, since it's not too bad.