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: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Typeclasses vs canonical instances
  • Date: Wed, 27 Apr 2016 11:04:05 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
  • Ironport-phdr: 9a23:UIeT5RfmJ5kGdQpng/ZkU1CzlGMj4u6mDksu8pMizoh2WeGdxc65bR7h7PlgxGXEQZ/co6odzbGG4+awASdZusvJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uDO04R32f1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDvxxSAgPCpC3zRYzw+n/3sPB80y7cIcTtVrEcWDK47q4tRgW+23RPDCIw7GyC0p84t6lcuh/0/xE=

On Wed, Apr 27, 2016 at 09:57:59AM +0200, Pierre-Marie Pédrot wrote:
> On 27/04/2016 06:59, Gregory Malecha wrote:
> > My understanding is that canonical structures are canonical, i.e. there
> > are not multiple solutions to them.
>
> According to this nice half-survey half-tutorial article, you can
> actually encode backtracking using canonical structures (Section 8):
>
> https://hal.inria.fr/hal-00816703v2/document

But... it is rather tricky. The best documentation for such (advanced)
technique is:

https://www.mpi-sws.org/~beta/lessadhoc/lessadhoc-extended.pdf

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.


I think that all these extensions to type inference are just "Prolog in
disguise". I've nothing ready to show, but I'm currently working on an
embeddable higher order Prolog interpreter one could use to express the
current type inference algorithm and all its user-extensions in an
single (and hopefully appropriate) language.

Hope it helps,
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page