<div dir="ltr"><div><div><div>Exact split is too restrictive. I think that it needs to be relaxed if it is to be used. I had to disable it.<br><br></div>Consider this example : This is a vert common programming pattern.<br><br>```<br>{-# OPTIONS --exact-split #-}<br><br>module test where<br><br>open import Data.Nat<br><br>data Test : Set where<br>  A : Test<br>  B : Test<br>  C : Test<br>  D  : Test<br><br><br>fun : Test → ℕ → ℕ<br>fun A n = zero<br>fun x n = {!!}<br><br>```<br><br></div>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.<br><br></div>Maybe we can relax the exact-split to not take this case into account. <br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 3, 2017 at 10:12 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
<br>
On 03/04/17 17:21, Thorsten Altenkirch wrote:<br>
> Thank you, Andreas.<br>
><br>
> Wouldn’t it be possible to have a flag to say wether one wants the old<br>
> behaviour or the new one?<br>
<br>
</span>In any case, please, please try to not break code: some of us have spent<br>
countless hours, days, months and years producing proofs, some of which<br>
haven't been written down in research papers yet. If you have to break<br>
my proofs because they are wrong, then so be it. But please think twice<br>
if you are going to break them just to improve the language.<br>
<br>
Thanks!<br>
<br>
Best,<br>
Martin<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
><br>
> Cheers,<br>
> Thorsten<br>
><br>
> On 03/04/2017, 15:21, "Agda on behalf of Andreas Abel"<br>
> <<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.<wbr>se</a> on behalf of <a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> wrote:<br>
><br>
>> Hi Thorsten,<br>
>><br>
>> this is this issue #408<br>
>><br>
>>   <a href="https://github.com/agda/agda/issues/408" rel="noreferrer" target="_blank">https://github.com/agda/agda/<wbr>issues/408</a><br>
>><br>
>> You can read there that I implemented a split strategy that would make<br>
>> your code work, but did not activate it, since fixes the split strategy<br>
>> to an extend where changing the order of clauses could not give you the<br>
>> other behavior.  In particular, it was not backwards-compatible.<br>
>> Whether we should turn on the new split strategy is still undecided<br>
>> (since 2012).<br>
>><br>
>> However, now you can use the --exact-split flag to let Agda alert you<br>
>> when your clauses do not lead to definitional equalities.<br>
>><br>
>> Cheers,<br>
>> Andreas<br>
>><br>
>> On 03.04.2017 15:08, Thorsten Altenkirch wrote:<br>
>>> Hi,<br>
>>><br>
>>> I tried to define the following function by pattern matching<br>
>>><br>
>>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)<br>
>>> codeDouble {zero} (b , ())<br>
>>> codeDouble {suc n} (false , zero) = zero<br>
>>> codeDouble {suc n} (true , zero) = suc zero<br>
>>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )<br>
>>><br>
>>> But to my confusion the term "codeDouble {suc n} (b , suc x) “ didn’t<br>
>>> reduce. This can be fixed by changing the order<br>
>>><br>
>>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)<br>
>>> codeDouble {zero} (b , ())<br>
>>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )<br>
>>> codeDouble {suc n} (false , zero) = zero<br>
>>> codeDouble {suc n} (true , zero) = suc zero<br>
>>><br>
>>> I guess I can answer this myself: since I first match on the boolean<br>
>>> agda decides also to do case analysis first on the boolean and then on<br>
>>> the Fin which duplicates my last line and has the effect that the<br>
>>> defining equality doesn’t hold definitionally (this is always a bit<br>
>>> agda). In this case agda could have matched my definition by changing<br>
>>> the order. Is this too much to ask for?<br>
>>><br>
>>> Cheers,<br>
>>> Thorsten<br>
>>><br>
>>><br>
>>><br>
>>> This message and any attachment are intended solely for the addressee<br>
>>> and may contain confidential information. If you have received this<br>
>>> message in error, please send it back to me, and immediately delete it.<br>
>>><br>
>>> Please do not use, copy or disclose the information contained in this<br>
>>> message or in any attachment.  Any views or opinions expressed by the<br>
>>> author of this email do not necessarily reflect the views of the<br>
>>> University of Nottingham.<br>
>>><br>
>>> This message has been checked for viruses but the contents of an<br>
>>> attachment may still contain software viruses which could damage your<br>
>>> computer system, you are advised to perform your own checks. Email<br>
>>> communications with the University of Nottingham may be monitored as<br>
>>> permitted by UK legislation.<br>
>>><br>
>>><br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>><br>
>><br>
>><br>
>> --<br>
>> Andreas Abel  <><      Du bist der geliebte Mensch.<br>
>><br>
>> Department of Computer Science and Engineering<br>
>> Chalmers and Gothenburg University, Sweden<br>
>><br>
>> <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
>> <a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~<wbr>abela/</a><br>
>> ______________________________<wbr>_________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
><br>
><br>
><br>
> This message and any attachment are intended solely for the addressee<br>
> and may contain confidential information. If you have received this<br>
> message in error, please send it back to me, and immediately delete it.<br>
><br>
> Please do not use, copy or disclose the information contained in this<br>
> message or in any attachment.  Any views or opinions expressed by the<br>
> author of this email do not necessarily reflect the views of the<br>
> University of Nottingham.<br>
><br>
> This message has been checked for viruses but the contents of an<br>
> attachment may still contain software viruses which could damage your<br>
> computer system, you are advised to perform your own checks. Email<br>
> communications with the University of Nottingham may be monitored as<br>
> permitted by UK legislation.<br>
><br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
<br>
</div></div><span class="HOEnZb"><font color="#888888">--<br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</font></span><div class="HOEnZb"><div class="h5">______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>