[Agda] Unification assumes injective postulates?

[Jan Malakhovski]

On Wed, 14 Nov 2012 11:03:54 +0100
Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> The basic question here is how we should understand
> 
>    postulate foo : Nat -> Nat
> 
> I see two basic interpretations here:
> 
> 1. foo is a fixed, arbitrary unknown function.
> 2. foo is a fixed, specific unknown function.
> 
> Interpretation 1, which seems to be the one taken by Agda, allows to 
> reduce foo x == foo y to x == y, since there are non-constant functions. 
>   A postulate behaves like a module parameter or a function parameter 
> (free variable).
> 
> Interpretation 2 is what you seem to expect.  You get this behavior when 
> you write
> 
>    foo : Nat -> Nat
>    foo = ?
> 
> Then, Agda only complains about unsolved constraints.
> 
> One solution for your issue could be that you replace your postulates by 
> holes.  However, that might litter your Agda session with distracting 
> goals.  Another take would be to have a second form of postulate, an 
> "existential postulate" opposed to the current "universal postulate".

Ok, so I carefully thought about this and there are still things I don't understand fully.
Correct me if I'm wrong somewhere.

It looks that
~~~~
postulate foo : ℕ → ℕ

bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
bar refl = {!!}
~~~~

and

~~~~
module Postulate (foo : ℕ → ℕ) where
  bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
  bar refl = {!!}
~~~~
work the same way.

So, if I think about postulates as "unknown exported module
parameters" (consider two modules, where the former postulates
something and the latter imports the former) interpretation 1 makes
sense (e.g. for "Level" terms that depend on it should work for any
internal structure of "Level").

Personally, I use module parameters explicitly when I need my proof to
work universally (so does the standard library, except for Level and
primitives).  So, up until now I expected postulates to be "named
holes" (e.g. I think LF-style definition from Dan Licata's message
assumes this interpretation for "if", and I think I can interpret
Level and primitives from this point of view too), but they are not.

I don't quite understand why the "universal interpretation" is the
default, but I wouldn't say that "existential interpretation" should
be the default either, because I don't clearly understand when I
should use which.

Anyway, the fact that changing postulate into a hole changes behavior was
quite unexpected.
I certainly think this should be clearly documented somewhere.

Having an "existential version" of a postulate would also be really
nice, yes.

By the way, abstracting a hole makes it into a "postulate" again
~~~~
abstract
  foo : ℕ → ℕ
  foo = ?

bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
bar refl = ?
~~~~

On Wed, 14 Nov 2012 18:51:37 +0100
Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> On 14.11.2012 15:40, Dan Licata wrote:
> > On the other hand, the intuition that
> >
> >    if two neutral terms with the same head are definitionally equal,
> >    then they have the same spine
> >
> > makes sense to me.  Is this the property that justifies the move you're
> > making above?
> >
> > On the other other hand, I can imagine situations where that fails,
> > because e.g. you have eta for coproducts definitionally.
> >
> > So, what is it about definitional equality that justifies that move from
> > foo x == foo y to x == y, and how does Agda know not to apply the same
> > reasoning to propositional equality?
> 
> The unifier called during pattern-checking behaves different than the 
> constraint solver called during equality-checking.  The unifier is based 
> on extensional equality (run-time equality of closed things) while the 
> constraint solver is based on intensional equality (compile-time 
> definitional equality of open things).
> 
> This is a bit subtle, I keep mixing this up myself...

This is really interesting, could you please elaborate on that
a bit more? Is there a term that shows the difference?

Form my naive skin-deep understanding of when pattern-checking and
equality-checking happen they are both existential to a certain degree:

~~~~
dom-easy : (f : ℕ → ℕ) → f ≡ (λ x → f x) → ⊤
dom-easy f refl = _

dom : (f g : ℕ → ℕ) → g ≡ (λ x → f x) → ⊤
dom f .f refl = _

cdom : (f : ℕ → ℕ) → f ≡ (λ x → f x)
cdom f = refl

both : (f g : ℕ → ℕ) → g ≡ (λ x → f x) → f ≡ g
both f .f refl = refl
~~~~

Also, I would explain
> > So, what is it about definitional equality that justifies that move from
> > foo x == foo y to x == y, and how does Agda know not to apply the same
> > reasoning to propositional equality?
to myself as: "It is not. Unification of "foo x == foo y" doesn't
imply x == y, but *requires* them to be equal definitionally."  Am I
wrong? If I'm not then how does it correlate to
extensional-intensional explanation?

Best regards,
  Jan