[Agda] using literals and the standard library
Thorsten Altenkirch
Thorsten.Altenkirch at nottingham.ac.uk
Thu Dec 6 11:37:03 CET 2018
Why are you not using the standard library?
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.
More information about the Agda
mailing list