[Agda] using literals and the standard library
Apostolis Xekoukoulotakis
apostolis.xekoukoulotakis at gmail.com
Thu Dec 6 11:31:17 CET 2018
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.
1.
https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary.agda#L26
2.
https://github.com/UlfNorell/agda-prelude/blob/master/src/Prelude/Decidable.agda#L6
> What exactly would that amount to? Will that force me to use the
> standard library?
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.
On Thu, Dec 6, 2018 at 11:51 AM Martin Escardo <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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181206/094ab821/attachment.html>
More information about the Agda
mailing list