The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

sure. My guess would be that I messed up the encoding of the hierarchy and the fmap call in the implementation of traverse is therefore not resolved to be be the Vector.map call.

https://gist.github.com/mgttlinger/db35a3748f1dfe68c152678f9a714c06

What is the "local go" pattern? A quick google lead me only to things related to Go-lang.

Cheers,

Merlin

Joachim Breitner <mail AT joachim-breitner.de> schrieb am So., 7. Jan. 2018 um 23:00 Uhr:

Hi,

can you show us your definitions of traverse, sequence or map? Probably
you can fix this by adjusting your definition of traverse (e.g. by not
passing f in the recursive function, but rather follow the “local go”
pattern).

Cheers,
Joachim

Am Sonntag, den 07.01.2018, 12:02 +0000 schrieb Merlin Göttlinger:
> Hi,
>
> after rewriting all my typeclasses to this CPS-transformed ones, it
> was still one indirection too many for the termination checker BUT if
> I additionally change traverse to sequence after Vector.map it works
> as expected. It is also entirely possible that I made a mistake
> somewhere that causes this behaviour but at any rate it works now
> without having to inline the vector definition or other tricks.
> Thanks for your help.
>
> Cheers,
> Merlin
>
> Joachim Breitner <mail AT joachim-breitner.de> schrieb am Fr., 5. Jan. 2018 um 21:37 Uhr:
> > Hi,
> >
> > I at least found the time to search for where I wrote about this
> > before. I think you are hitting the problem that I describe in
> > https://stackoverflow.com/q/47082796/946226
> > The question talks about records, and not classes, but since Coq
> > classes are (normally) record type, it is the same problem – the
> > termination checker runs after type class resolution and sees the
> > underlying record.
> >
> > I describe our solution with CPS-transformed types for classes in the
> > first answer.
> >
> > Feel free to ask for further clarification, either here or on SE.
> >
> > Cheers,
> > Joachim
> >
> >
> > Am Freitag, den 05.01.2018, 18:55 +0000 schrieb Merlin Göttlinger:
> > > Hi,
> > >
> > > that sounds promising. I would be interrested to hear how this trick works because it certainly isn't obvious to me from looking a tthe code.
> > > So if you find the time later on to explain this I would be greatfull, but in any case thank you both for your help.
> > >
> > > Cheers,
> > > Merlin
> > >
> > > Joachim Breitner <mail AT joachim-breitner.de> schrieb am Fr., 5. Jan. 2018 um 19:14 Uhr:
> > > > Hi,
> > > >
> > > > Am Freitag, den 05.01.2018, 11:54 +0000 schrieb Merlin Göttlinger:
> > > > > VectorUtils.traverse depends on a bunch of stuff I implemented and is
> > > > > the usual operation known from e.g. Haskell with signature G A -> (A
> > > > > -> F B) -> F (G B) where G is (fun T => Vector.t T n) and F is list
> > > > > in my case.
> > > >
> > > > Coq’s termination checker cannot look through type class instances.
> > > >
> > > > There is a trick, however, if you get to choose the type class. See
> > > > https://github.com/antalsz/hs-to-coq/blob/master/base/GHC/Base.v#L41-L54
> > > > and let me know if you want more explanation (I am on the run right
> > > > now).
> > > >
> > > > Joachim
> > > >
> > > > --
> > > > Joachim Breitner
> > > >   mail AT joachim-breitner.de
> > > >   http://www.joachim-breitner.de/
> > --
> > Joachim Breitner
> >   mail AT joachim-breitner.de
> >   http://www.joachim-breitner.de/
--
Joachim Breitner
  mail AT joachim-breitner.de
  http://www.joachim-breitner.de/