[Agda] using literals and the standard library

Thu Dec 6 10:39:30 CET 2018

In favor of having instance arguments in agda-stdlib, in separate files. In
favor of merging agda-prelude into stdlib.
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>
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 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
>>
> _______________________________________________
> 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/a5f1bb9b/attachment.html>