Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual Fixpoints into mutual inductive types


Chronological Thread 
  • From: Merlin Göttlinger <megoettlinger AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Mutual Fixpoints into mutual inductive types
  • Date: Mon, 08 Jan 2018 08:23:43 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f48.google.com
  • Ironport-phdr: 9a23:JvkPThERcQaPGg7Hcatv551GYnF86YWxBRYc798ds5kLTJ7zpMuwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe0fMuZCq4n9pl0OogO/CxGqGOPv1jtIhn7w3a01zeshCxzN0QslH90Qv3TUq8v6NLsOUeCxzanIyzrDYO1M2Trm54jIdwouofCIXb5qbcXRzkwvGhrDg16Np4LlODaV2f4Ms2id9+dgV+WvhHQ7pAFxozivw94ghZLTho0Ly1DE6SN5z5gvJdGiVUF0f8aoEJRRtyGGN4t2X9gtT3t0tyY9z70KoYW7fDQQx5s7xB7fbOKHfJaS4hLtUOaRJjl5iGh5d7K4gha/91WrxO7kVsSszlpGsi5InsPPu30NzRDf9NWLR/Rn8kqu2juC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBir2l1/3jK+Sb0kk+/So5/j+brXoqZKRNJV4ig75MqQplcy/Bfo3PhISUGic/OSwzLzj/UvnT7VWlvA6jLXVvZTAKckYpqO1GRFZ3pss5hqlADqr08wUnXwdI1JEfBKHgZLpO1bLIP3gCPewnVuskDB1yPDaIr3hBpTNLn7MkLj/Z7Zw8EFcyA8pwtBe45JYEK0OIPX2WkPprtzXEgc5MxCow+bgENhyyoQeWXuWDqCFNKPSrESH6/k0I+iMYY8VoCzyJ+Ik5/7ol385mEUScbOn3ZsNOziEGaFtJFzcan7xiP8AF30Lt0wwVr/EklqHBBtefXKzWZUTeC0nDIOgAorZDtSojbOG0TunGpxQaW1cIl+JGHbsMY6DXqFfO2qpPsZ9n2lcBvCaQIg72ET2uQ==

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/



Archive powered by MHonArc 2.6.18.

Top of Page