[Agda] Questions about unification

[András Kovács]

> What if "t = Nat"?


So in this case "u" is solvable both as "\x -> x" and "\_ -> Nat", right,
which is no good? I think I get it.

The occurs check is implemented in Agda.TypeChecking.MetaVars.Occurs [1],
> and is called before solving a meta in Agda


I did not meant the usual occurs check or the pruning on the right hand
side. I meant that we have meta "u" with type "Delta -> A", and we have "u
[ sigma ] = t" to be solved, and in this case what if "u" occurs in its own
"A [ sigma ]" type? In the link I sent, around the end of the slides,
Pientka talks about this kind of occurs check, and concludes that "u"
cannot occur in its own return type if we have an ordered metacontext where
solutions for a meta can only depend on metas declared to the left. This is
the kind of occurs check I couldn't find in the Agda sources, but I also
don't think Agda has ordered metacontexts. Does this mean that self-type
occurrence is not possible either with unordered metacxt as well?

2016-11-28 7:10 GMT+01:00 Ulf Norell <ulf.norell at gmail.com>:

>
> On Sun, Nov 27, 2016 at 4:22 PM, András Kovács <kovacsahun at hotmail.com>
> wrote:
>
>> I'm learning about pattern unification, and I have a couple of questions.
>>
>> First, in Agda, are types irrelevant for the purpose of unification, and
>> if not, why? I mean the following: suppose we have "u [ Nat ] = t", where
>> "u" is a meta, "[ Nat ]" is a substitution with one entry which is the
>> "Nat" type. Can we solve "u" as "\_ -> t"? No Agda terms can branch on
>> types in any way, so this seems correct at least on the first look, but I'm
>> not sure if this breaks something.
>>
>
> What if "t = Nat"? One could certainly imagine restrictions on "t" that
> would make it safe, but we don't do anything like that at the moment. I
> suspect constraints like that are not very common in practise.
>
> Second, does Agda do occurs check for the type of the meta to be solved? I
>> couldn't find it (as of now) in the sources. Pientka writes here
>> <http://wips.cs.umn.edu/slides/pientka.pdf> that ordered metacontexts
>> make occurs checks for types unnecessary. As far as I saw in the sources
>> Agda has no ordered contexts (and no reshuffling of contexts like in ch. 4
>> of Adam Gundry's thesis).
>>
>
> The occurs check is implemented in Agda.TypeChecking.MetaVars.Occurs [1],
> and is called before solving a meta in Agda.TypeChecking.MetaVars [2]. It
> also does pruning; removing impossible variable dependencies from metas in
> the right hand side. For instance given a constraint "U [x] = c (V [x, y])"
> for metas "U" and "V" and constructor "c", we can conclude that "V" cannot
> depend on "y" and solve it by "V [x, _] := W [x]" for a fresh meta "W".
> This then lets us solve "U [x] := c (W [x])".
>
> / Ulf
>
> [1] https://github.com/agda/agda/blob/509d481/src/full/
> Agda/TypeChecking/MetaVars/Occurs.hs
> [2] https://github.com/agda/agda/blob/509d481/src/full/
> Agda/TypeChecking/MetaVars.hs#L683
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161128/e281bb4a/attachment-0001.html