[Agda] using literals and the standard library
Martin Escardo
m.escardo at cs.bham.ac.uk
Thu Dec 6 10:50:52 CET 2018
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
More information about the Agda
mailing list