The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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/

Attachment: signature.asc
Description: This is a digitally signed message part