coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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/
- [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/07/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/07/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/07/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
Archive powered by MHonArc 2.6.18.