coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Joachim Breitner <mail AT joachim-breitner.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mutual Fixpoints into mutual inductive types
- Date: Fri, 05 Jan 2018 21:37:00 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
- Ironport-phdr: 9a23:RkhjjhPLonlXcg90Hc8l6mtUPXoX/o7sNwtQ0KIMzox0Iv/4rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkEKjA38H/ZhMJyg6JVvB2voBNwzpXbYI2JLvdzZLnQcc8YSGdHQ81fVzZBAoS5b4YXC+QBOvxXoJX9p1sPqBu1GBShBPnxxT9Jmn/227M10/48GgzB2QwvBdMOsHDPodX3M6cdS/y6zKnJzTXGdv9Zwi3955bJchA9p/GDQ6hwfdDMxkYxDg7IiEibp4LiPzOQzOsNsm6b4vJiVeKokWEotwFxojmqxss1kYbJnJwaylHY9SV/3ok1P8e0R1NlbtK8H5tQtj2aN4trQsw5WW1npCE6yrgetZ6gYCgF0ogoxx3Ya/yZbYeI+BzjVOKWITZ2nn5qZLW/hxO0/EO9yeP8TtG53EtIoydEiNXBsmoB2wLO5sWJUPdx40ms1DiJ2gvO8O9LO1o0mrDeK5M5wr4/iJ4TsUPbEy/2hkr2lqqWeVs/+uSy8OTofK/mpoGCOI9ukA7+N74hltaiDusmKgQOXm6b9vqg1LD74EH0QrRHgucyn6XDrpzWOMoWqrSkDwJb3Isv8xO/AC2n0NQck3kHNlVFeBefgojsIV7OIfT4AOy9g1Srijhk2/DGPrzkApnUNXfDiqnufbdh605a1gUz18pT6I9KBb0ZOvL8RlfxtMDEDh8+KwG73+HnCMxk2owCXWKPH7SWPbjJsV6I4+IvO/ODaJUUuDb7Mfgl5uThgWU3mV8HLuGV2s4cb2n9FfB7KW2YZ2Dti5EPCzQkpA07Gc7tgVaCUDsbTWy/Xr466ytzXIevDIPrRIeki7yA2WKxBJBXemZLEBaAHCG7JM2/R/4QZXfKcYdamTseWO35Rg==
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/
Attachment:
signature.asc
Description: This is a digitally signed message part
- [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.