[Agda] implicit level arguments

[Nils Anders Danielsson]

On 2013-01-28 12:44, Serge D. Mechveliani wrote:
> People,
> can you, please, explain about the  level arguments  style?
>
> The Standard library lib-0.6 declares, for example,
>
>    record _=>_ {c} (CБ┌│ CБ┌┌ : Container c) : Set c where ...      -- I
>
>    record Semigroup c l : Set (suc (max c l)) where ...         -- II
>    Group, RingWithOne ...  are in the same style of  II
>
>    record Container (l : Level) : Set (suc l) where ...         -- III
>
>    data Eq {a l} {A : Set a} (_~~_ : Rel A l) : ...             -- IV
>
> (for this letter, I replace some math symbols).
>
> My impression is that the level arguments should be implicit.
> Because
> a) I suspect that levels are needed to differ between such collections
>     as sets and proper classes, and the like (right?),
> b) in practical computation, one usually does not think of whether the
>     data is of a set or of a proper class,
>     (this is kind of a second class information).
>
> Now, (I) hides the level,  II uses explicit levels,
> III uses an explicit level, and even adds  `: Level'
> and  `data Eq'  hides its two levels.
>
> Is this put at random or by some systematic approach?

I try to make the Level arguments explicit only if they usually need to
be given explicitly.

-- 
/NAD