[Agda] Path to success with Agda?
Pedro Abreu
abreu223 at gmail.com
Tue Aug 30 14:26:28 CEST 2022
Since a lot of this discussion is around pattern matching, you may find
this interview with Jesper Cocx helpful:
https://www.typetheoryforall.com/2022/04/02/16-Agda,-K-Axiom,-HoTT,-Rewrite-Theory-(Jesper-Cockx).html#c359641b
Best,
Pedro Abreu.
On Tue, Aug 30, 2022 at 7:00 AM <agda-request at lists.chalmers.se> wrote:
>
> Send Agda mailing list submissions to
> agda at lists.chalmers.se
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.chalmers.se/mailman/listinfo/agda
> or, via email, send a message with subject or body 'help' to
> agda-request at lists.chalmers.se
>
> You can reach the person managing the list at
> agda-owner at lists.chalmers.se
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Agda digest..."
>
>
> Today's Topics:
>
> 1. Re: Path to success with Agda? (Andrew Pitts)
> 2. Re: Path to success with Agda? (Mi?tek Bak)
> 3. Re: Path to success with Agda? (Andrew Pitts)
> 4. Re: Path to success with Agda? (mechvel at scico.botik.ru)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 30 Aug 2022 08:58:14 +0100
> From: Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
> To: Ignat Insarov <kindaro at gmail.com>, "agda at lists.chalmers.se"
> <agda at lists.chalmers.se>
> Subject: Re: [Agda] Path to success with Agda?
> Message-ID: <EB4861D3-C3DE-461D-BAAB-59E2770AF075 at cl.cam.ac.uk>
> Content-Type: text/plain; charset=utf-8
>
>
> > On 30 Aug 2022, at 00:02, Ignat Insarov <kindaro at gmail.com> wrote:
> >
> > Cool, let us dig in!
>
> Personally, Agda?s implementation of dependent pattern matching was what
got me using Adga rather than Coq when I first needed to use one of these
systems (Lean was not an option at the time). Stick with it ? it?s great,
honestly.
>
> But I sympathise about your problems with ?with? (and was interested to
read Peter Hancock?s confession). It can be very annoying in the middle of
a big proof to try to work around why a particular use of ?with? won?t type
check.
>
> So I wanted to mention the humble ?case? expression, which functional
programmers can more easily relate to, maybe. It?s less powerful that
?with?, but sometimes works (wrt the not typechecking thing) when ?with?
won?t.
>
> It?s not a built-in, so one is just disguising ?ordinary? Type Theory
with some user-defined syntax. For example, defining
>
> open import Agda.Primitive public
> case :
> {l m : Level}
> {A : Set l}
> {B : A ? Set m}
> (x : A)
> (f : (x : A) ? B x)
> ? -----------------
> B x
> case x f = f x
>
> then the first example of ?with? at <
https://agda.readthedocs.io/en/latest/language/with-abstraction.html>
becomes
>
> open import Agda.Builtin.Bool public
> open import Agda.Builtin.List public
> filter : {A : Set} ? (A ? Bool) ? List A ? List A
> filter p [] = []
> filter p (x ? xs) = case (p x) \{
> true ? x ? filter p xs ;
> false ? filter p xs }
>
> (of course you can write ? rather than \ if you prefer).
>
> Andy
>
>
>
>
>
>
>
>
> ------------------------------
>
> Message: 2
> Date: Tue, 30 Aug 2022 10:29:47 +0200
> From: Mi?tek Bak <mietek at bak.io>
> To: Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
> Cc: Ignat Insarov <kindaro at gmail.com>, "agda at lists.chalmers.se"
> <agda at lists.chalmers.se>
> Subject: Re: [Agda] Path to success with Agda?
> Message-ID: <02A6748C-8542-4FBF-A059-FADF7BD130A0 at bak.io>
> Content-Type: text/plain; charset=utf-8
>
> > On 30 Aug 2022, at 09:58, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
wrote:
> >
> > So I wanted to mention the humble ?case? expression, which functional
programmers can more easily relate to, maybe. It?s less powerful that
?with?, but sometimes works (wrt the not typechecking thing) when ?with?
won?t.
>
> It would be interesting to see an example in which `case` works and
`with` does not.
>
> --
> MB
>
>
>
>
> ------------------------------
>
> Message: 3
> Date: Tue, 30 Aug 2022 09:42:55 +0100
> From: Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
> To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>, Mi?tek Bak
> <mietek at bak.io>
> Subject: Re: [Agda] Path to success with Agda?
> Message-ID: <FA909DCB-11AC-487A-B2B0-0F128A147036 at cl.cam.ac.uk>
> Content-Type: text/plain; charset=utf-8
>
>
>
> > On 30 Aug 2022, at 09:29, Mi?tek Bak <mietek at bak.io> wrote:
> >
> >> On 30 Aug 2022, at 09:58, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
wrote:
> >>
> >> So I wanted to mention the humble ?case? expression, which functional
programmers can more easily relate to, maybe. It?s less powerful that
?with?, but sometimes works (wrt the not typechecking thing) when ?with?
won?t.
> >
> > It would be interesting to see an example in which `case` works and
`with` does not.
>
> I have some and will try to extract them from their context when I get a
mo. However, I should qualify what I said:
>
> "but sometimes [case] works (wrt the not typechecking thing) when
?with? won?t?
>
> What I really meant was that, at the time, it was easier for me to use a
?case" expression than to figure out how to still use ?with? by moving
lemmas to the top level, generalizing arguments a bit more, etc, etc. I
expect there?s always a way with ?with?.
>
> And if you are heavily in to using ?rewrite? (?with? disguised), then I
guess ?case? is not helpful.
>
> Andy
>
>
>
> ------------------------------
>
> Message: 4
> Date: Tue, 30 Aug 2022 11:45:20 +0300
> From: mechvel at scico.botik.ru
> To: Ignat Insarov <kindaro at gmail.com>
> Cc: Jason Hu <fdhzs2010 at hotmail.com>, agda at lists.chalmers.se
> Subject: Re: [Agda] Path to success with Agda?
> Message-ID: <8aaacc2155a1655df702849f5b15cdf9 at scico.botik.ru>
> Content-Type: text/plain; charset=UTF-8; format=flowed
>
> Section 1.2 in
>
> http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc/manual.pdf
>
> has practical advises on how to write proofs in Agda.
> I do not know why, but these guidelines help me, and I have managed to
> write
> many different proofs.
> One of the advises is to use a helper function instead of `with',
> `case', `let'
> -- if they fail to type-check.
> And if the helper helps, then one could also consider returning back to
> `with' or `case' or `let' with improvements.
>
> ------
> Sergei
>
>
>
> On 2022-08-30 02:02, Ignat Insarov wrote:
> > Cool, let us dig in!
> >
> >> 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.
> >
> > I am all for it, but how do I write such a helper??I tried to follow
> > the
> > language reference, but it does not make sense.?It reads more like a
> > remainder
> > for someone who is already familiar with the principles, than as an
> > introduction.
> >
> >> 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.
> >
> > What do you mean when you say _?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.
> >
> > What does it mean to _?generalize?_ here??Following your example, how
> > would a
> > generalized _bar_ look??What does it mean for _bar_ and _foo bar_ to be
> > abstracted??How does this help with type checking?
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> ------------------------------
>
> End of Agda Digest, Vol 204, Issue 8
> ************************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220830/644b0e21/attachment.html>
More information about the Agda
mailing list