<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Consider the "Dec" data type. At the moment, both agda-stdlib and agda-prelude have the same definition but written twice, meaning that from the point of view of agda, they are separate things. So at the moment, you cannot use proofs from one version to the other.<br></div><div><br></div><div>1. <a href="https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary.agda#L26">https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary.agda#L26</a></div><div>2. <a href="https://github.com/UlfNorell/agda-prelude/blob/master/src/Prelude/Decidable.agda#L6">https://github.com/UlfNorell/agda-prelude/blob/master/src/Prelude/Decidable.agda#L6</a><br></div></div><div dir="ltr"><br></div><div dir="ltr">> <span class="gmail-im"></span>What exactly would that amount to? Will that force me to use the <br>
> standard library?</div><div dir="ltr"><br></div><div>If there is a reason to keep a definition as it is, it will remain as it is, I suppose. The important thing for me is to reuse proofs from isomorphic data structures and not have to write them once more.<br></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Dec 6, 2018 at 11:51 AM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
<br>
On 06/12/2018 09:39, <a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a> wrote:<br>
> In favor of having instance arguments in agda-stdlib, in separate files. <br>
<br>
I am neutral to this, because I don't use the standard library.<br>
<br>
> In favor of merging agda-prelude into stdlib.<br>
<br>
What exactly would that amount to? Will that force me to use the <br>
standard library?<br>
<br>
Martin<br>
<br>
> We need to write isomorphisms between similar structures so that we can <br>
> switch between the most convenient at the time.<br>
> <br>
> And cubical will allow us to use the fastest version at compile time, right?<br>
> <br>
> On Thu, Dec 6, 2018 at 9:53 AM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a> <br>
> <mailto:<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>>> wrote:<br>
> <br>
> 'Data.Nat.Instance' certainly might be a way to go. Would it be a<br>
> problem that all the different useful instances that could<br>
> conceivably be created for Nat (presumably quite a lot?) would all<br>
> be in one file?<br>
> <br>
> On Thu, 6 Dec 2018, 06:48 Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a><br>
> <mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br>
> <br>
> The standard library could conceivably have separate files<br>
> containing instances, e.g. Data.Nat.Instances would re-export<br>
> Data.Nat.Literals.number as an instance. The fact that the<br>
> standard library doesn't have instances is certainly one of the<br>
> reasons I currently *don't* use it (and use Ulf's Prelude instead).<br>
> <br>
> -- Jesper<br>
> <br>
> On Thu, Dec 6, 2018 at 7:09 AM Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a><br>
> <mailto:<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>>> wrote:<br>
> <br>
> The Unit issue is due to Jesper's recent changes to instance<br>
> arguments.<br>
> See<br>
> <a href="https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f" rel="noreferrer" target="_blank">https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f</a><br>
> for the documentation. Instance goals solved by unification<br>
> still counts as<br>
> a missing instance if the solution isn't an instance.<br>
> <br>
> We are a bit reluctant to add instance declarations to<br>
> the standard<br>
> library because they can't be hidden upon module import<br>
> so users would<br>
> necessarily have them in scope even if they don't want them.<br>
> <br>
> <br>
> Instances can be hidden on import as follows:<br>
> <br>
> import Bar hiding (someInstance)<br>
> open Bar<br>
> <br>
> If you write `open import Bar hiding (someInstance)` this<br>
> desugars into<br>
> <br>
> import Bar<br>
> open Bar hiding (someInstance)<br>
> <br>
> which still leaves it in scope as `Bar.someInstance`<br>
> <br>
> / Ulf<br>
> <br>
> On Thu, Dec 6, 2018 at 2:21 AM Guillaume Allais<br>
> <<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a><br>
> <mailto:<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>>> wrote:<br>
> <br>
> I meant not importing anything unit-related.<br>
> I don't get any error (using either 2.5.4.2 or<br>
> 2.6.0-329b843) with:<br>
> <br>
> ```<br>
> open import Agda.Builtin.FromNat<br>
> open import Data.Nat<br>
> open import Data.Nat.Literals<br>
> open import Data.Fin<br>
> open import Data.Fin.Literals<br>
> <br>
> instance<br>
> _ = Data.Nat.Literals.number<br>
> _ = Data.Fin.Literals.number<br>
> <br>
> test-nat : ℕ<br>
> test-nat = 3<br>
> <br>
> test-fin : Fin 7<br>
> test-fin = 3<br>
> ```<br>
> <br>
> <br>
> On 06/12/2018 01:58, Martin Stone Davis wrote:<br>
> > Hi Guillaume,<br>
> ><br>
> > I'm not sure what you meant by your remark that it's<br>
> not necessary to import<br>
> > Data.Unit. Did you just mean that it could be<br>
> replaced with an import of<br>
> > Agda.Builtin.Unit? If you meant that it could simply<br>
> be removed, know that,<br>
> > without that import, I get the following error in<br>
> `test-nat`:<br>
> ><br>
> > ```<br>
> > No instance of type ;Agda.Builtin.Unit.⊤ was found in<br>
> scope.<br>
> > when checking that 3 is a valid argument to a<br>
> function of type<br>
> > {a : ;Agda.Primitive.Level} {A : Set a} ⦃ r : Number<br>
> A ⦄ (n : ℕ)<br>
> > ⦃ _ : r .Number.Constraint n ⦄ →<br>
> > A<br>
> > ```<br>
> ><br>
> > -M<br>
> ><br>
> ><br>
> > On 12/05/2018 12:04 PM, Guillaume Allais wrote:<br>
> >> Hi Martin,<br>
> >><br>
> >> That looks like a reasonable module definition (with<br>
> the side remark<br>
> >> that it's not necessary to import Data.Unit).<br>
> >><br>
> >> We are a bit reluctant to add instance declarations<br>
> to the standard<br>
> >> library because they can't be hidden upon module<br>
> import so users would<br>
> >> necessarily have them in scope even if they don't<br>
> want them.<br>
> >><br>
> >> As for the Data.Fin.Literals.number if we do need<br>
> the natural number<br>
> >> to be implicit for it to be usable directly as an<br>
> instance, I think<br>
> >> that should indeed be modified in the stdlib.<br>
> >><br>
> >> Cheers,<br>
> >> --<br>
> >> gallais<br>
> >><br>
> >><br>
> >> On 05/12/2018 06:31, Martin Stone Davis wrote:<br>
> >>> To get both Nat and Fin literals using the standard<br>
> library (latest development<br>
> >>> versions, including Jesper's latest re: instance<br>
> resolution), I write the<br>
> >>> following:<br>
> >>><br>
> >>> ```agda<br>
> >>> open import Agda.Builtin.FromNat<br>
> >>> open import Data.Nat<br>
> >>> open import Data.Nat.Literals<br>
> >>> open import Data.Fin<br>
> >>> open import Data.Fin.Literals<br>
> >>> open import Data.Unit -- or Agda.Builtin.Unit<br>
> >>><br>
> >>> instance<br>
> >>> _ = Data.Nat.Literals.number<br>
> >>><br>
> >>> _ : ∀ {n} → Number (Fin n)<br>
> >>> _ = Data.Fin.Literals.number _<br>
> >>><br>
> >>> test-nat : ℕ<br>
> >>> test-nat = 3<br>
> >>><br>
> >>> test-fin : Fin 7<br>
> >>> test-fin = 3<br>
> >>> ```<br>
> >>><br>
> >>> It's a bit annoying to need to import from<br>
> Agda.Builtin.FromNat and from<br>
> >>> Data.Unit, so I wonder if this is the recommended<br>
> approach? Also, should<br>
> >>> Data.Fin.Literals.number be updated to take a<br>
> hidden argument (given that the<br>
> >>> new instance resolution does not count explicit<br>
> arguments as instance arguments<br>
> >>> anymore)?<br>
> >>><br>
> >>> _______________________________________________<br>
> >>> Agda mailing list<br>
> >>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
> >>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> ><br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
-- <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>
</blockquote></div>