coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Typeclasses vs canonical instances, Igor Zhirkov, 04/24/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jason Gross, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/29/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
Archive powered by MHonArc 2.6.18.