[Agda] A question on why "postulate" works but "variable" fails

[Jesper Cockx]

Hi Eduardo,

There is quite a big difference between how `postulate` and `variable` work
(both in their purpose and their implementations) so it is not surprising
that you can find some examples where `postulate` works but `variable`
doesn't.

The purpose of `variable` is essentially to allow you to omit writing
universal quantifications of the form `{x : A} → ...` over and over again
in each type signature. So if you write `variable B₁ : Set` then that means
any use of `B₁` will implicitly insert a `{B₁ : Set} → ...` in front of the
type signature where it occurs.

Things admittedly become more complicated when the type of a `variable`
contains itself a generalizable variable. In this case Agda will
recursively add quantifications for all the variables that occur in the
type, variables that occur in their types, etc. So a `variable B₂ : (y₁ :
B₁) → Set` means that any use of `B₂` will implicitly insert `{B₁ : Set}
{B₂ : (y₁ : B₁) → Set} → ...` in front of the type.

Actually this is not the full story of what happens, since Agda will always
first try to solve constraints before deciding on the set of variables to
generalize over. Variables that are solved during this process are not part
of the quantification. For example, suppose we have some type `P : (Bool →
Set) → Set` and we declare `f : P B₂`, then Agda's constraint solver will
figure out that the `B₁` in the type of `B₂` must be equal to `Bool` and
hence it will insert `{B₂ : (y₁ : Bool) → Set} → ...` instead of ` {B₁ :
Set} {B₂ : (y₁ : B₁) → Set} → ...`.

However, it is important to understand that Agda's constraint solver is not
perfect (actually the problem is undecidable so it cannot be) so it is
possible that there are unsolved constraints remaining and hence Agda does
not know which variables it should quantify over. Here's a small example:
```agda
postulate P : Nat → Set

variable f : Nat → Nat
variable q : P (f 0)

postulate test : (R : P 2 → Set) → R q
```
When trying to figure out what variables to quantify over, Agda gets the
constraint that `f 0 = 2`, but there are many different ways to solve this
constraint. Instead of making an arbitrary choice, Agda refuses to solve
this and reports the unsolved constraint instead.

So far so good. Now the final piece of the puzzle is what happens when one
variable appears in the types of two or more other variables. For example,
in your code the type `B₁` occurs in the type of `B₂`, in the type `A₁`,
and in the type of `y₁`. In this situation (and this might be a bit
unintuitive at first) each variable will get its own copy of the name `B₁`,
indicated by `B₂.B₁`, `A₁.B₁, and `y₁.B₁` respectively. So when you use
these variables together, such as in the type of `x₁`, Agda will not
automatically assume that these different copies of `B₁` are equal [Here
lies the real difference with using `postulate`]. Instead it will run the
constraint solver to figure out the relationship between them, which (as
noted above) might or might not succeed depending on the complexity of the
problem.

Now we can understand the error message you are getting from Agda. For
example, for `x₁` you get the following unsolved constraint
```
_y₂.B₂_33 _y₂.y₁_34 =< _A₁.B₂_32 y₁
```
>From this we can infer that Agda figured out that in order for the type `A₁
y₁ y₂` to be well-formed, it needs to know that `y₂.B₂` (the copy of `B₂`
used in the type of `y₂`) applied to `y₂.y₁` (the copy of `y₁` used in the
type of `y₂`) is equal to `A₁.B₂` (the copy of `B₂` used in the type of
`A₁`) applied to `y₁` (the "local" copy of `y₁` from the definition of `x₁`
itself. If Agda knew that `y₂.B₂ = A₁.B₂` then it could figure out that
`y₂.y₁ = y₁`, and vice versa if `y₂.y₁ = y₁` then it could figure out that
`y₂.B₂ = A₁.B₂`. However since it knows neither of those the constraint
remains unsolved and you get the error you are observing.

I hope this explanation made things clearer!

-- Jesper


ps: The page on opening record types that you are linking does not make use
of `variable`s (in fact I think it was written before those were even added
to Agda) so you shouldn't need to understand `variable` to read that page.
However, it is possibly out-of-date since we have moved all documentation
from the wiki to agda.readthedocs.io.

On Mon, Dec 27, 2021 at 11:21 PM Eduardo Ochs <eduardoochs at gmail.com> wrote:

> Hi! Help! Beginner question!
>
> Let me start with instructions to reproduce the problem.
> Put this in the file /tmp/test/P.agda,
>
> --snip--snip--
> postulate B₁ :                                              Set
> postulate B₂ : (y₁ : B₁) →                                  Set
> postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) →                   Set
> postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
> postulate y₁ : B₁
> postulate y₂ : B₂ y₁
> postulate x₁ : A₁ y₁ y₂
> postulate x₂ : A₂ y₁ y₂ x₁
> --snip--snip--
>
> and this in the file /tmp/test/V.agda:
>
> --snip--snip--
> variable B₁ :                                              Set
> variable B₂ : (y₁ : B₁) →                                  Set
> variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) →                   Set
> variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
> variable y₁ : B₁
> variable y₂ : B₂ y₁
> variable x₁ : A₁ y₁ y₂
> variable x₂ : A₂ y₁ y₂ x₁
> --snip--snip--
>
> When I use the key sequence `C-c C-l' from agda2-mode to load the two
> files in the file P.agda everything works, but in V.agda I get an
> error whose main message is "Failed to solve the following
> constraints"... and in another case in which I was working using
> "postulate" worked, but when I used "variable" I got an error that
> started with something like "Generalizable variables not allowed
> here".
>
> I just spent some hours trying to understand the section 3.14 -
> "Generalization of Declared Variables", link:
>
>   https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83
>
> - of the user manual, but it's too terse for me and it has too many
> prerequisites, and I am stuck.
>
> So, QUESTION: can you recommend me other places to learn the
> distinctions between "postulate" and "variable"?
>
>   Thanks in advance!
>     Eduardo Ochs
>     http://angg.twu.net/math-b.html
>
>
>
>
> P.S.: I am using Agda 2.6.1.3.
>
> P.P.S.: To be honest I was trying to understand this,
>
> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
> and to specialize its example to n:=2 and m:=2 and to check if the
> "(r : R Δ)" really works, but I have the impression that I need to
> understand variables first...
>
> _______________________________________________
> 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/20211228/dd9e88dc/attachment.html>