[Agda] [ANNOUNCE] Agda 2.5.1

[Bradley Hardy]

Hi Andy,

I believe it’s the actual definitions of the primitive types and functions that are loaded automatically. The names are a separate matter. The automatic inference of types whose names aren’t in scope happens elsewhere too. If we have modules and definitions like so:

-- A.agda
module A where
  data A : Set where

-- B.agda
module B where
  open import A

  data B : A -> Set where
    fromA : (x : A) -> B x

-- C.agda
module C where
  open import B

  fromA' : forall x -> B x
  fromA' = fromA

Agda is able to infer that the first argument to `fromA’` has type `A`, even though the actual name for that type is not in scope.

The same thing is going on with your example. That module essentially re-exports the names of the primitive definitions (by defining them as dummy postulates and binding them to the real definitions using the BUILTIN pragma), but those definitions exist regardless of whether their names are in scope.

Brad

> On 18 Apr 2016, at 17:27, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
> 
> I quote from Release notes for Agda version 2.5.1:
> 
> "The Agda.Builtin modules are installed in the same way as
> Agda.Primitive, but unlike Agda.Primitive they are not loaded
> automatically.”
> 
> This prompts me to ask a question that has bugged me for some time,
> but not sufficiently to be bothered to ask this list, until now.
> 
> In what sense, exactly, is Agda.Primitive  “loaded automatically” ?
> Naively, I would think the answer should be that the declarations in
> Agda.Primitive are always available without having to say
> 
> open import Agda.Primitive
> 
> However, whereas
> 
> data foo  {ℓ }(A : Set ℓ) : Set ℓ where
> 
> typechecks OK,
> 
> data foo  {ℓ : Level}(A : Set ℓ) : Set ℓ where
> 
> does not (Agda complains that Level is not is scope), whereas
> 
> open import Agda.Primitive
> data foo  {ℓ : Level}(A : Set ℓ) : Set ℓ where
> 
> does typecheck.
> 
> What am I mis-understanding here?
> 
> Andy
> 
> 
> Andrew M. Pitts,
> Professor of Theoretical Computer Science,
> University of Cambridge Computer Laboratory,
> William Gates Building, 15 JJ Thomson Ave,
> Cambridge CB3 0FD, UK.
> 
> Tel +44 1223 334629,
> Fax +44 1223 334678,
> Email <Andrew.Pitts at cl.cam.ac.uk>,
> Web   <www.cl.cam.ac.uk/users/amp12>.
> 
> 
> On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
>> Dear all,
>> 
>> The Agda Team is very pleased to announce the release of Agda 2.5.1.
>> 
>> GHC supported versions
>> ======================
>> 
>> Agda 2.5.1 has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.
>> 
>> 
>> Installation
>> ============
>> 
>>  cabal update && cabal install Agda
>> 
>> 
>> Standard library
>> ================
>> 
>> The version of Agda standard library compatible with Agda 2.5.1 is
>> available at
>> 
>>  https://github.com/agda/agda-stdlib/releases/tag/v0.12
>> 
>> (The release of the Agda standard library 0.12 will be announced
>> later).
>> 
>> What is new?
>> ============
>> 
>> In addition to the new features, changes, incompatibilities, fixed
>> issues and enhancements announced on the release candidates 1 and 2
>> 
>>  http://thread.gmane.org/gmane.comp.lang.agda/8378
>> 
>>  http://thread.gmane.org/gmane.comp.lang.agda/8529
>> 
>> the following issues were fixed:
>> 
>> * https://github.com/agda/agda/issues/1796
>> 
>> * https://github.com/agda/agda/issues/1821
>> 
>> More information about the changes included in Agda 2.5.1 can be found
>> in
>> 
>>  http://hackage.haskell.org/package/Agda-2.5.1/changelog
>> 
>> 
>> Enjoy Agda 2.5.1.
>> 
>> --
>> Andrés, on behalf of the Agda Team
>> _______________________________________________
>> 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