[Agda] some yellow, for your amusement

[Ulf Norell]

On Fri, Jul 25, 2008 at 12:24 PM, Conor McBride <conor at strictlypositive.org>
wrote:

>
> I think it's a bunch of unsolved constraints that are holding
> things up. More particularly, I suspect that
>
>  f (x , y) = t
>
> is not being solved (for f) in situations where
>
>  f x y = t
>
> would be. Is that the trouble? If so, one possibly cheap,
> possibly nasty fix is to solve a metavariable which is
> functional over a record with another which is functional
> over the individual fields. That way, the former reduces
> to the latter without any weird poking about inside the
> unification algorithm.
>

> A more principled solution, also incorporating patterns
> for records, may be worth seeking.
>

I think the more principled solution is what we have to go for here.
Consider the constraint

 f r = t

where f is a metavariable and r is variable of record type. This
fix would solve f with \r -> g (fst r) (snd r) and we'd end up with
the new constraint

g (fst r) (snd r) = t

The left hand side of the first constraint is a perfectly acceptable
Miller pattern, whereas the left hand side of the new constraint isn't,
so if we do solve f with g we also have to change the notion of
Miller patterns to include projections from variables. If we're playing
with the Miller patterns anyway, we might as well make f (x, y) a
valid pattern and not have to introduce g in the first place.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080729/98927b3a/attachment.html