[Agda] pattern matching order

Mon Apr 3 21:36:44 CEST 2017

Exact split is too restrictive. I think that it needs to be relaxed if it
is to be used. I had to disable it.

Consider this example : This is a vert common programming pattern.

```
{-# OPTIONS --exact-split #-}

module test where

open import Data.Nat

data Test : Set where
  A : Test
  B : Test
  C : Test
  D  : Test

fun : Test → ℕ → ℕ
fun A n = zero
fun x n = {!!}

```

If Test has 100 constructors and all 99 are used by fun in the same way,
exact split would force the programmer to write the same code for the 99
remaining constructors.

Maybe we can relax the exact-split to not take this case into account.

On Mon, Apr 3, 2017 at 10:12 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
>
> On 03/04/17 17:21, Thorsten Altenkirch wrote:
> > Thank you, Andreas.
> >
> > Wouldn’t it be possible to have a flag to say wether one wants the old
> > behaviour or the new one?
>
> In any case, please, please try to not break code: some of us have spent
> countless hours, days, months and years producing proofs, some of which
> haven't been written down in research papers yet. If you have to break
> my proofs because they are wrong, then so be it. But please think twice
> if you are going to break them just to improve the language.
>
> Thanks!
>
> Best,
> Martin
>
>
> >
> > Cheers,
> > Thorsten
> >
> > On 03/04/2017, 15:21, "Agda on behalf of Andreas Abel"
> > <agda-bounces at lists.chalmers.se on behalf of abela at chalmers.se> wrote:
> >
> >> Hi Thorsten,
> >>
> >> this is this issue #408
> >>
> >>   https://github.com/agda/agda/issues/408
> >>
> >> You can read there that I implemented a split strategy that would make
> >> your code work, but did not activate it, since fixes the split strategy
> >> to an extend where changing the order of clauses could not give you the
> >> other behavior.  In particular, it was not backwards-compatible.
> >> Whether we should turn on the new split strategy is still undecided
> >> (since 2012).
> >>
> >> However, now you can use the --exact-split flag to let Agda alert you
> >> when your clauses do not lead to definitional equalities.
> >>
> >> Cheers,
> >> Andreas
> >>
> >> On 03.04.2017 15:08, Thorsten Altenkirch wrote:
> >>> Hi,
> >>>
> >>> I tried to define the following function by pattern matching
> >>>
> >>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
> >>> codeDouble {zero} (b , ())
> >>> codeDouble {suc n} (false , zero) = zero
> >>> codeDouble {suc n} (true , zero) = suc zero
> >>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
> >>>
> >>> But to my confusion the term "codeDouble {suc n} (b , suc x) “ didn’t
> >>> reduce. This can be fixed by changing the order
> >>>
> >>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
> >>> codeDouble {zero} (b , ())
> >>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
> >>> codeDouble {suc n} (false , zero) = zero
> >>> codeDouble {suc n} (true , zero) = suc zero
> >>>
> >>> I guess I can answer this myself: since I first match on the boolean
> >>> agda decides also to do case analysis first on the boolean and then on
> >>> the Fin which duplicates my last line and has the effect that the
> >>> defining equality doesn’t hold definitionally (this is always a bit
> >>> agda). In this case agda could have matched my definition by changing
> >>> the order. Is this too much to ask for?
> >>>
> >>> Cheers,
> >>> Thorsten
> >>>
> >>>
> >>>
> >>> This message and any attachment are intended solely for the addressee
> >>> and may contain confidential information. If you have received this
> >>> message in error, please send it back to me, and immediately delete it.
> >>>
> >>> Please do not use, copy or disclose the information contained in this
> >>> message or in any attachment.  Any views or opinions expressed by the
> >>> author of this email do not necessarily reflect the views of the
> >>> University of Nottingham.
> >>>
> >>> This message has been checked for viruses but the contents of an
> >>> attachment may still contain software viruses which could damage your
> >>> computer system, you are advised to perform your own checks. Email
> >>> communications with the University of Nottingham may be monitored as
> >>> permitted by UK legislation.
> >>>
> >>>
> >>>
> >>> _______________________________________________
> >>> Agda mailing list
> >>> Agda at lists.chalmers.se
> >>> https://lists.chalmers.se/mailman/listinfo/agda
> >>>
> >>
> >>
> >> --
> >> Andreas Abel  <><      Du bist der geliebte Mensch.
> >>
> >> Department of Computer Science and Engineering
> >> Chalmers and Gothenburg University, Sweden
> >>
> >> andreas.abel at gu.se
> >> http://www.cse.chalmers.se/~abela/
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >> https://lists.chalmers.se/mailman/listinfo/agda
> >
> >
> >
> >
> >
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please send it back to me, and immediately delete it.
> >
> > Please do not use, copy or disclose the information contained in this
> > message or in any attachment.  Any views or opinions expressed by the
> > author of this email do not necessarily reflect the views of the
> > University of Nottingham.
> >
> > This message has been checked for viruses but the contents of an
> > attachment may still contain software viruses which could damage your
> > computer system, you are advised to perform your own checks. Email
> > communications with the University of Nottingham may be monitored as
> > permitted by UK legislation.
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
> _______________________________________________
> 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/20170403/ccf4c0c3/attachment-0001.html>