[Agda] using literals and the standard library
Martin Escardo
m.escardo at cs.bham.ac.uk
Thu Dec 6 11:44:31 CET 2018
On 06/12/2018 10:37, Thorsten Altenkirch wrote:
> Why are you not using the standard library?
Are you telling me off? :-)
Best,
Martin
>
> Thorsten
>
> On 06/12/2018, 09:51, "Agda on behalf of Martin Escardo" <agda-bounces at lists.chalmers.se on behalf of m.escardo at cs.bham.ac.uk> wrote:
>
>
>
> On 06/12/2018 09:39, apostolis.xekoukoulotakis at gmail.com wrote:
> > In favor of having instance arguments in agda-stdlib, in separate files.
>
> I am neutral to this, because I don't use the standard library.
>
> > In favor of merging agda-prelude into stdlib.
>
> What exactly would that amount to? Will that force me to use the
> standard library?
>
> Martin
>
> > We need to write isomorphisms between similar structures so that we can
> > switch between the most convenient at the time.
> >
> > And cubical will allow us to use the fastest version at compile time, right?
> >
> > On Thu, Dec 6, 2018 at 9:53 AM Matthew Daggitt <matthewdaggitt at gmail.com
> > <mailto:matthewdaggitt at gmail.com>> wrote:
> >
> > 'Data.Nat.Instance' certainly might be a way to go. Would it be a
> > problem that all the different useful instances that could
> > conceivably be created for Nat (presumably quite a lot?) would all
> > be in one file?
> >
> > On Thu, 6 Dec 2018, 06:48 Jesper Cockx <Jesper at sikanda.be
> > <mailto:Jesper at sikanda.be> wrote:
> >
> > The standard library could conceivably have separate files
> > containing instances, e.g. Data.Nat.Instances would re-export
> > Data.Nat.Literals.number as an instance. The fact that the
> > standard library doesn't have instances is certainly one of the
> > reasons I currently *don't* use it (and use Ulf's Prelude instead).
> >
> > -- Jesper
> >
> > On Thu, Dec 6, 2018 at 7:09 AM Ulf Norell <ulf.norell at gmail.com
> > <mailto:ulf.norell at gmail.com>> wrote:
> >
> > The Unit issue is due to Jesper's recent changes to instance
> > arguments.
> > See
> > https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f
> > for the documentation. Instance goals solved by unification
> > still counts as
> > a missing instance if the solution isn't an instance.
> >
> > We are a bit reluctant to add instance declarations to
> > the standard
> > library because they can't be hidden upon module import
> > so users would
> > necessarily have them in scope even if they don't want them.
> >
> >
> > Instances can be hidden on import as follows:
> >
> > import Bar hiding (someInstance)
> > open Bar
> >
> > If you write `open import Bar hiding (someInstance)` this
> > desugars into
> >
> > import Bar
> > open Bar hiding (someInstance)
> >
> > which still leaves it in scope as `Bar.someInstance`
> >
> > / Ulf
> >
> > On Thu, Dec 6, 2018 at 2:21 AM Guillaume Allais
> > <guillaume.allais at ens-lyon.org
> > <mailto:guillaume.allais at ens-lyon.org>> wrote:
> >
> > I meant not importing anything unit-related.
> > I don't get any error (using either 2.5.4.2 or
> > 2.6.0-329b843) with:
> >
> > ```
> > open import Agda.Builtin.FromNat
> > open import Data.Nat
> > open import Data.Nat.Literals
> > open import Data.Fin
> > open import Data.Fin.Literals
> >
> > instance
> > _ = Data.Nat.Literals.number
> > _ = Data.Fin.Literals.number
> >
> > test-nat : ℕ
> > test-nat = 3
> >
> > test-fin : Fin 7
> > test-fin = 3
> > ```
> >
> >
> > On 06/12/2018 01:58, Martin Stone Davis wrote:
> > > Hi Guillaume,
> > >
> > > I'm not sure what you meant by your remark that it's
> > not necessary to import
> > > Data.Unit. Did you just mean that it could be
> > replaced with an import of
> > > Agda.Builtin.Unit? If you meant that it could simply
> > be removed, know that,
> > > without that import, I get the following error in
> > `test-nat`:
> > >
> > > ```
> > > No instance of type ;Agda.Builtin.Unit.⊤ was found in
> > scope.
> > > when checking that 3 is a valid argument to a
> > function of type
> > > {a : ;Agda.Primitive.Level} {A : Set a} ⦃ r : Number
> > A ⦄ (n : ℕ)
> > > ⦃ _ : r .Number.Constraint n ⦄ →
> > > A
> > > ```
> > >
> > > -M
> > >
> > >
> > > On 12/05/2018 12:04 PM, Guillaume Allais wrote:
> > >> Hi Martin,
> > >>
> > >> That looks like a reasonable module definition (with
> > the side remark
> > >> that it's not necessary to import Data.Unit).
> > >>
> > >> We are a bit reluctant to add instance declarations
> > to the standard
> > >> library because they can't be hidden upon module
> > import so users would
> > >> necessarily have them in scope even if they don't
> > want them.
> > >>
> > >> As for the Data.Fin.Literals.number if we do need
> > the natural number
> > >> to be implicit for it to be usable directly as an
> > instance, I think
> > >> that should indeed be modified in the stdlib.
> > >>
> > >> Cheers,
> > >> --
> > >> gallais
> > >>
> > >>
> > >> On 05/12/2018 06:31, Martin Stone Davis wrote:
> > >>> To get both Nat and Fin literals using the standard
> > library (latest development
> > >>> versions, including Jesper's latest re: instance
> > resolution), I write the
> > >>> following:
> > >>>
> > >>> ```agda
> > >>> open import Agda.Builtin.FromNat
> > >>> open import Data.Nat
> > >>> open import Data.Nat.Literals
> > >>> open import Data.Fin
> > >>> open import Data.Fin.Literals
> > >>> open import Data.Unit -- or Agda.Builtin.Unit
> > >>>
> > >>> instance
> > >>> _ = Data.Nat.Literals.number
> > >>>
> > >>> _ : ∀ {n} → Number (Fin n)
> > >>> _ = Data.Fin.Literals.number _
> > >>>
> > >>> test-nat : ℕ
> > >>> test-nat = 3
> > >>>
> > >>> test-fin : Fin 7
> > >>> test-fin = 3
> > >>> ```
> > >>>
> > >>> It's a bit annoying to need to import from
> > Agda.Builtin.FromNat and from
> > >>> Data.Unit, so I wonder if this is the recommended
> > approach? Also, should
> > >>> Data.Fin.Literals.number be updated to take a
> > hidden argument (given that the
> > >>> new instance resolution does not count explicit
> > arguments as instance arguments
> > >>> anymore)?
> > >>>
> > >>> _______________________________________________
> > >>> Agda mailing list
> > >>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > >>> https://lists.chalmers.se/mailman/listinfo/agda
> > >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> >
> > _______________________________________________
> > 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
>
>
>
>
>
> 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 contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
More information about the Agda
mailing list