Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Typeclasses vs canonical instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclasses vs canonical instances


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Typeclasses vs canonical instances
  • Date: Wed, 27 Apr 2016 21:28:55 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
  • Ironport-phdr: 9a23:gHsfgB9EiAFQVP9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdWdu6kP17WempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiC1I/riKibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhSg2G+nsVVC0ynxtWDg7ZpEX4WZHwsSb+u+dV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9



On 04/27/2016 05:04 AM, Enrico Tassi wrote:
...
In short unification already performs some backtracking, in particular
when constants are unfolded. By crafting a chain of aliases (constants
begin just another name for the same value) one can trick unification
into trying many "canonical" solutions for the "same" problem.

If so, then there should be open_constrs X and Y such that "unify X Y" succeeds but "exactly_once (unify X Y)" fails due to multiple successes. I tried a few cases involving constant unfolding, but can't seem to get this to occur. Can anyone else?

I'm not doubting that canonical structures can do backtracking - but it might be "confined" backtracking, just like typeclasses backtracking is confined to within a single invocation of typeclasses eauto, such that one cannot backtrack back into a successful case from the outside.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page