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

Wed Dec 29 12:27:50 CET 2021

Hi Eduardo,

Regarding 2, I actually think it is currently not possible to ask the full
type of a generalizable variable because of the error you describe. What
you'd need is a way to ask for the type of a particular *symbol* as opposed
to the type of an *expression*, but there is currently no command for that.
I've created an issue on Github to discuss the possibility of adding such a
command: https://github.com/agda/agda/issues/5714

-- Jesper

On Wed, Dec 29, 2021 at 6:54 AM Eduardo Ochs <eduardoochs at gmail.com> wrote:

> Hi Jesper!
>
> Three things:
>
> 1) Thanks and REALLY WOW! That was super clear! =)
>
> 2) How do I inspect what Agda knows about a variable? Suppose that we
>    have 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--
>
>    My newbiesh instincts suggested a) to try `C-c C-d B₁ RET' at the
>    end of that file, and, if that failed, b) to insert this at the
>    end of the file,
>
>    --snip--snip--
>    foo : ?
>    foo = B₁
>    --snip--snip--
>
>    and then type `C-c C-l'. Both things gave this error:
>
>      Generalizable variable Variable1.B₁ is not supported here
>      when scope checking B₁
>
> 3) You're right, this old tutorial
>
>
> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
>
>    doesn't use variables or postulates, but I had to use postulates to
>    produce a version of some of its examples that Agda could parse and
>    load... It is here:
>
>    http://angg.twu.net/AGDA/Postulate1.agda.html
>    http://angg.twu.net/AGDA/Postulate1.agda
>
> Cheers! =)
>   Eduardo Ochs
>   http://angg.twu.net/#eev
>   http://angg.twu.net/math-b.html
>
>
> On Tue, 28 Dec 2021 at 08:37, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> 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/20211229/b291d8f9/attachment.html>