[Agda] using literals and the standard library

[Jesper Cockx]

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> 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> 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
>> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >
>>
>>
>> _______________________________________________
>> Agda mailing list
>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181206/136df6ef/attachment.html>