<div dir="ltr"><div dir="ltr">Hi Jesper!<br><br>Three things:<br><br>1) Thanks and REALLY WOW! That was super clear! =)<br><br>2) How do I inspect what Agda knows about a variable? Suppose that we<br> have this in the file /tmp/test/V.agda...<br><br><font face="monospace"> --snip--snip--<br> variable B₁ : Set<br> variable B₂ : (y₁ : B₁) → Set<br> variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set<br> variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set<br> variable y₁ : B₁<br> variable y₂ : B₂ y₁<br> -- variable x₁ : A₁ y₁ y₂<br> -- variable x₂ : A₂ y₁ y₂ x₁<br> --snip--snip--<br></font><br> My newbiesh instincts suggested a) to try `C-c C-d B₁ RET' at the<br> end of that file, and, if that failed, b) to insert this at the<br> end of the file,<br><br><font face="monospace"> --snip--snip--<br> foo : ?<br> foo = B₁<br> --snip--snip--<br></font><br> and then type `C-c C-l'. Both things gave this error:<br><br> Generalizable variable Variable1.B₁ is not supported here<br> when scope checking B₁<br><br>3) You're right, this old tutorial<br><br><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening">https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening</a><br><br> doesn't use variables or postulates, but I had to use postulates to<br> produce a version of some of its examples that Agda could parse and<br> load... It is here:<br><br> <a href="http://angg.twu.net/AGDA/Postulate1.agda.html">http://angg.twu.net/AGDA/Postulate1.agda.html</a><br> <a href="http://angg.twu.net/AGDA/Postulate1.agda">http://angg.twu.net/AGDA/Postulate1.agda</a><br><br>Cheers! =)<br> Eduardo Ochs<br> <a href="http://angg.twu.net/#eev">http://angg.twu.net/#eev</a><br> <a href="http://angg.twu.net/math-b.html">http://angg.twu.net/math-b.html</a><br></div><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 28 Dec 2021 at 08:37, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Eduardo,</div><div><br></div><div>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. <br></div><div><br></div><div>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. <br></div><div><br></div><div>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.</div><div><br></div><div>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} → ...`.</div><div><br></div><div>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:</div><div></div><div>```agda</div><div>postulate P : Nat → Set<br><br>variable f : Nat → Nat<br>variable q : P (f 0)<br><br>postulate test : (R : P 2 → Set) → R q</div><div>```</div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>Now we can understand the error message you are getting from Agda. For example, for `x₁` you get the following unsolved constraint<br></div><div>```</div><div>_y₂.B₂_33 _y₂.y₁_34 =< _A₁.B₂_32 y₁</div><div>```<br></div><div>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.</div><div><br></div><div>I hope this explanation made things clearer!</div><div><br></div><div>-- Jesper</div><div><br></div><div><br></div><div>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 <a href="http://agda.readthedocs.io" target="_blank">agda.readthedocs.io</a>.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Dec 27, 2021 at 11:21 PM Eduardo Ochs <<a href="mailto:eduardoochs@gmail.com" target="_blank">eduardoochs@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi! Help! Beginner question!<br><br>Let me start with instructions to reproduce the problem.<br>Put this in the file /tmp/test/P.agda,<br><br>--snip--snip--<br><font face="monospace">postulate B₁ : Set<br>postulate B₂ : (y₁ : B₁) → Set<br>postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set<br>postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set<br>postulate y₁ : B₁<br>postulate y₂ : B₂ y₁<br>postulate x₁ : A₁ y₁ y₂<br>postulate x₂ : A₂ y₁ y₂ x₁</font><br>--snip--snip--<br><br>and this in the file /tmp/test/V.agda:<br><br>--snip--snip--<br><font face="monospace">variable B₁ : Set<br>variable B₂ : (y₁ : B₁) → Set<br>variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set<br>variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set<br>variable y₁ : B₁<br>variable y₂ : B₂ y₁<br>variable x₁ : A₁ y₁ y₂<br>variable x₂ : A₂ y₁ y₂ x₁</font><br>--snip--snip--<br><br>When I use the key sequence `C-c C-l' from agda2-mode to load the two<br>files in the file P.agda everything works, but in V.agda I get an<br>error whose main message is "Failed to solve the following<br>constraints"... and in another case in which I was working using<br>"postulate" worked, but when I used "variable" I got an error that<br>started with something like "Generalizable variables not allowed<br>here".<br><br>I just spent some hours trying to understand the section 3.14 -<br>"Generalization of Declared Variables", link:<br><br> <a href="https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83" target="_blank">https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83</a><br><br>- of the user manual, but it's too terse for me and it has too many<br>prerequisites, and I am stuck.<br><br>So, QUESTION: can you recommend me other places to learn the<br>distinctions between "postulate" and "variable"?<br><br> Thanks in advance!<br> Eduardo Ochs<br> <a href="http://angg.twu.net/math-b.html" target="_blank">http://angg.twu.net/math-b.html</a><br><br><br><br><br>P.S.: I am using Agda 2.6.1.3.<br><br>P.P.S.: To be honest I was trying to understand this,<br><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening" target="_blank">https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening</a><br>and to specialize its example to n:=2 and m:=2 and to check if the<br>"(r : R Δ)" really works, but I have the impression that I need to<br>understand variables first...<br><div><br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div></div>