[Agda] pattern matching order

Andreas Abel abela at chalmers.se
Mon Apr 3 22:31:27 CEST 2017 

Yes, for this reason we have the pragma {-# CATCHALL #-}.

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

   data Test : Set where
     A B C D : Test

   fun : Test → Set
   fun A = Test
   {-# CATCHALL #-}
   fun x = {!!}

On 03.04.2017 21:36, Apostolis Xekoukoulotakis wrote:
> 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
> <mailto: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
>     <mailto:agda-bounces at lists.chalmers.se> on behalf of
>     abela at chalmers.se <mailto:abela at chalmers.se>> wrote:
>     >
>     >> Hi Thorsten,
>     >>
>     >> this is this issue #408
>     >>
>     >>   https://github.com/agda/agda/issues/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 <mailto:Agda at lists.chalmers.se>
>     >>> https://lists.chalmers.se/mailman/listinfo/agda
>     <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 <mailto:andreas.abel at gu.se>
>     >> http://www.cse.chalmers.se/~abela/
>     <http://www.cse.chalmers.se/~abela/>
>     >> _______________________________________________
>     >> Agda mailing list
>     >> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     >> https://lists.chalmers.se/mailman/listinfo/agda
>     <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 <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>     >
>
>     --
>     Martin Escardo
>     http://www.cs.bham.ac.uk/~mhe
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <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/

More information about the Agda mailing list