[Agda] A question on why "postulate" works but "variable" fails
Eduardo Ochs
eduardoochs at gmail.com
Wed Dec 29 06:53:27 CET 2021
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/1dab5e92/attachment.html>
More information about the Agda
mailing list