[Agda] some yellow, for your amusement

[Conor McBride]

Hi Ulf

On 29 Jul 2008, at 10:17, Ulf Norell wrote:
> 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,

That's fair.

> so if we do solve f with g we also have to change the notion of
> Miller patterns to include projections from variables.

Or else we need to split r as well, but more generally,...

> 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.

...one approach to doing that is to flatten out records
(you either do it up front, or you do it on the fly). But
there are more related questions. Here's one

data Fun : Nat -> Set where
   fun : {f : (Nat -> Nat) -> Nat}(g : Nat -> Nat) -> Fun (f g)
   dun : {f : (Nat -> Nat) -> Nat}(g : Nat -> Nat) -> Fun (f (\x -> g  
x))

foo : (g : Nat -> Nat) -> Fun (g zero)
foo = fun

doo : (g : Nat -> Nat) -> Fun (g zero)
doo = dun  -- goes yellow, as you might expect, with

{- _42 := dun  |  [_41 (\x -> g x) = g zero : Nat] -}

There's clearly some thinking to do here, when it comes
to eta-laws and pattern unification.

Another potential payoff from such a technology would be
in allowing more complex patterns in binders to do
eta-harmless rearrangement, as in

   ((x , y) : Sigma A B) -> Blah x y

rather than

   (p : Sigma A B) -> Blah (fst p) (snd p)

The container crew have recently been playing with types
like

   (s : S) -> Sigma T \t -> (q : Q t) -> Maybe (P s)

abstract members of which might be bound more choice-ly

   \s -> (f s , \q -> g s q)

   where  f : S -> T
          g : (s : S) -> Q (f s) -> Maybe (P s)
   are the pattern variables

one day, if we bang our heads off this enough. It seems
to me that one needs to replace "pattern variable"
with "Miller pattern" in an appropriate sense, discharging
all the lambda-bound variables we've gone under.

But I worry that I'm not communicating all that
intelligibly here. Installing Miller/mixed-prefix/pattern
unification as a familiar and sensible thing in the minds
of programmers seems a bit further down the line, I fear,
partly because we haven't smoothed out its corners yet. I
don't think first-order unification seems like voodoo in
the same way, so there's a comprehension gap to fill.

Interesting times

Conor