[Agda] Agda implementation of McBride's unification paper?

[Nils Anders Danielsson]

On 2013-11-18 00:26, Kenichi Asai wrote:
> I wonder if there is an agda implementation of Conor McBride's paper
> "First-order unification by structural recursion".  Any information is
> welcome.

I believe that Andrea Vezzosi made use of this approach in his
implementation of pattern unification:

   https://github.com/Saizan/miller

> The Data.List.Countdown module in the standard library appears to be
> related to the paper.  If there is any document on how to use it,
> please let me know.  (I am rather new to agda, and it is a bit
> difficult for me to read through the module, although I am trying.)

I used this module to prove that a certain subtyping relation for
recursive types is decidable, using an algorithm due to Brandt and
Henglein.

Initialisation of the countdown structure:

   http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping/RecursiveTypes.Subterm.RestrictedHypothesis.html

Use of the countdown structure:

   http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping/RecursiveTypes.Subtyping.Axiomatic.Inductive.html

(The code is related to a paper, but this paper does not discuss the
implementation of the algorithm.)

The basic idea:

* You want to perform recursion on the number of elements left to
   inspect.

* _⊕_ has type List A → ℕ → Set. A value of type xs ⊕ n represents a
   state where we have inspected all the elements in xs, and there are at
   most n other elements of type A.

* You can construct a value of type [] ⊕ n if you can prove that the
   type A contains at most n elements (up to some decidable equivalence
   relation).

* The function lookupOrInsert tells you whether you have already
   inspected a certain element. If not, then it is added to the list, and
   you get a proof showing that the natural number has the form "suc n".
   If you perform a recursive call on "n", then the termination checker
   sees that "n" is structurally smaller than "suc n".

I'm not sure that this is the best approach, but it worked at the time.

-- 
/NAD