<div dir="ltr"><div>Thanks, Sergei. Even if the use of postulate is not enough to allow me to <br>advance in this particular case, your help is greatly appreciated <br>(I will consider using postulate from now on).<br></div>
<div><br>Cheers,<br><br>Carlos<br><div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 7, 2013 at 9:39 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div>On Wed, 2013-11-06 at 15:14 -0200, Carlos Camarao wrote:<br>
> I am trying to write in Agda the simplest piece of code I can for<br>
> proving soundness and completeness of a most general unification<br>
> function; I think this is a good, instructive example of a problem<br>
> that<br>
> should have a simple but non-structurally recursive solution.<br>
><br>
> In Unif.agda (all Agda files are annexed) I restricted the problem<br>
> first to a function, mgu2, that is supposed to give the most general<br>
> unifier of only two simple types, if it exists, together with the<br>
> proofs that they are the least unifiers. Types are in Ty.agda and<br>
> substitutions in Subst_list.agda.<br>
><br>
> When Unif.agda is compiled (question marks are used in places to be<br>
> filled latter), the compiler inserts holes, starting with { }₀ (do<br>
> this, if you want, after copying all agda files into a subdirectory).<br>
> When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed<br>
> (meaning 'try to automatically fill the hole yourself if you can'),<br>
> the compiler inserts "nothing" in the place of { }₀.<br>
><br>
> That is a bug (I think).<br>
><br>
> Furthermore, if I delete the inserted "nothing" and insert "just ?"<br>
> the program is accepted by the compiler. The compiler replaces "?" by<br>
> "{ }₀":<br>
> an inconsistency, since "nothing" was considered before the<br>
> only possibility ("just ?" should thus not be accepted).<br>
><br>
> Trying to continue, if the "case-of" piece of code below is inserted<br>
> (instead of a question mark):<br>
><br>
> case mgu2 (Var v) (Con c) of λ<br>
> { nothing → nothing ;<br>
> (just (s , _ , p₁)) → just ?<br>
><br>
> then the compiler again replaces the question mark inside the case-of<br>
> by a hole, say { }₀ (it becomes { }₀ by loading the file, i.e. by<br>
> typing<br>
> Cntrl-c Cntrl-l). By refining { }₀ (by typing Cntrl-c Cntrol-r), it<br>
> becomes:<br>
><br>
> case mgu2 (Var v) (Con c) of λ<br>
> { nothing → nothing ;<br>
> (just (s , _ , p₁)) → just ({ }₀ , { }₁)<br>
><br>
> Now, if I type Cntrl-c Cntrl-a inside the new hole { }₀,<br>
> created by the compiler, the case-of becomes:<br>
><br>
> case mgu2 (Var v) (Con c) of λ<br>
> { nothing → nothing ;<br>
> (just (s , _ , p₁)) → just (proj₁ (p₁ .proj₁) , {!!}₁)<br>
><br>
> But this code, inserted by the compiler itself, does not<br>
> compile: typing Cntrl-c Cntrl-l gives the error message:<br>
><br>
<br>
</div></div>So far, my impression is that using interactive help with holes of {?}<br>
and such, cannot give an essential help in developing a program.<br>
<br>
(Though, I am a newbie, I may mistake).<br>
<br>
Instead, I proceed this way:<br>
<br>
... → just v1 where<br>
postulate v1 : Foo<br>
<br>
and set for Foo the type which I guess is needed.<br>
If the type checker rejects this, I try to improve Foo.<br>
After Foo is done, I remove `postulate', and start with defining<br>
v1 = ...<br>
After everything is checked, I remove some declarations like v1 : Foo<br>
-- the ones that do not essentially help with readability.<br>
<br>
The idea is that if I do not know where and what is the error, I split<br>
the code into the type declaration for its parts. Then, run the checker<br>
by C-c C-l, and split each part further -- until I find which type<br>
needs improvement.<br>
<br>
Regards,<br>
<br>
-------<br>
Sergei<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
</blockquote></div><br></div></div></div></div>