[Agda] Path to success with Agda?

[Jason Hu]

Indeed, pattern matching in Agda is very powerful, often more powerful than expected if you come from Coq, but usually the complete opposite if you just follow your nose. I think you fall into the latter case.

If you ignore some bugs in the pattern matcher (which you might well bump into), from my learning experience, I think it is the best to learn why Agda refuses your pattern by writing out a helper function supposedly generated by the pattern matcher and with-patterns; recall that this is also how Agda handles it after all (at least this is how the doc phrases it). By writing a helper out, you might obtain some information about why Agda rejects you, or you might just succeed. The latter case could mean that you just phrased a smarter helper than Agda could, or you worked around an Agda bug.

To answer your questions directly, if a case split fails, it is likely that the variable you are splitting is depended on by some other type, which triggers some further mechanisms that eventually fails the case split. Another common possibility is that you turned on without-K, but your case split effectively is doing that. This case can be checked by observing whether a case split will cause unification of the same variable.

If your with-pattern fails, it could mean that you are not generalizing enough. For example, if you are with-patterning a term of type (foo bar) and it fails, it might be fixed by generalizing bar before (foo bar), which causes both bar and (foo bar) being abstracted and thus making the Typechecker happy.

In general, I don’t think you need to read anybody’s thesis to have a high-level impression on how to please Agda. However, having experience in another proof assistant or type theory in general definitely helps. If you have more questions I think many can answer you if you ask here.

Thanks,
Jason

From: Ignat Insarov<mailto:kindaro at gmail.com>
Sent: Monday, August 29, 2022 5:12 PM
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: [Agda] Path to success with Agda?

Hello!

I have been trying to learn Agda time and again and I have not made much headway
yet. Once I stray a little aside from the happy path of _Programming Language
Foundations with Agda_, things start to get sour. Even the exercises in the book
give me a hard time whenever they let me a little freedom to get myself lost.

* You cannot always make cases for a given parameter. If you want to understand
  when you can and cannot make cases for a parameter, you have to read a thesis
  of the person that has written the pattern matching code.

* You cannot always have a with-abstraction — sometimes the auxiliary functions
  it compiles to do not type check. If you want to understand when you can and
  cannot make a with-abstraction, you only have the language reference to help
  you out, and it does not explain the problem in enough detail.

But there is nothing in the language to help me write proofs but pattern
matching and with-abstractions!

My first language is Haskell and it was a bit hard to learn, but there was the
amazing community to support my efforts. With Agda, the main venue seems to be
the Zulip chat, but it is more dead than alive. No one is rushing to explain
anything to me.

I have no problem learning Type Theory by itself, since there are great books
out there. Σ types, eliminators, you name it — no problem. My problem seems to
be rooted in the technical difficulties that are specific to Agda — the pattern
matching algorithm and the ill-typed with-abstractions.

Are there any success stories from people that did not learn Agda as a student
with the people that have written Agda itself or do research in Type Theory with
Agda or something to that end? I can see how someone might get good with Agda if
one is near to an expert, but doing it on my own seems to be a hard task. Ars
longa, vita brevis! What is the path I should take so that I get to write
realistic proofs and still have time left to enjoy the success?
_______________________________________________
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/20220829/9feed6c2/attachment.html>