[Agda] using literals and the standard library

[Matthew Daggitt]

'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 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> 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
>>
> _______________________________________________
> 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/d5c46709/attachment.html>