[Agda] Extending Pattern Unification to Records

[Conor McBride]

On 3 Feb 2011, at 12:56, Andreas Abel wrote:

> Brigitte and I have written a draft on higher-order unification  
> using constraints.
>
>  Higher-Order Dynamic Pattern Unification for
>    Dependent Types and Records
>  http://www2.tcs.ifi.lmu.de/~abel/unif-sigma.pdf

I haven't read it yet, but APPLAUSE for addressing this problem!

Conor


>
> It contains some ideas that are relevant for Agda:
>
> 1. Detailed theoretical treatment of constraints that are outside of  
> the pattern fragment and how they can be molded towards patterns by
>
>  - pruning
>  - eta-contraction
>  - ignoring non-linear variable occurrences that do not appear on  
> the right hand side
>
> These techniques are in essence already implemented in Agda.
>
> However, eta-contraction in Agda was found to be buggy; in the paper  
> we argue that eta-contraction can be restricted to terms t_i in a  
> l.h.s.
>
>  X t1 ... tn = t   (X a meta-variable)
>
> where eta-contraction is sound.
>
> 2. Full integration of record types by applying the (dependent  
> version of the) isomorphisms
>
>  A -> B * C = (A -> B) * (A -> C)
>  A * B -> C = A -> B -> C
>
> This allows to solve constraints like
>
>  X (x , y) = t
>  X (fst x) = t
>
> Find more details in the paper.  Comments welcome!
>
> Andreas
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda