The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

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