Syntax of 'data' declaration [Re: [Agda] boundings in data-where]

[Andreas Abel]

Currently the syntax for data is

   data D pars : type where
     constructor-type-signatures

Thus, open statements and definitions are not supported.  We could think 
of making data declarations more flexible, in a way similar to record 
declarations.  This could be done by adding a 'constructor' keyword 
similar to 'field'.

   data D ... where
     declarations
     constructor
       constructor-type-signatures
     declarations
     constructor
       constructor-type-signatures
     ...

Without 'constructor' keyword, this would be ambiguous.  If you have

   data D : Set where
     f : A
     f = bla
     c : B

then it is not apriori clear if "f : A" should be a constructor 
declaration or the signature of a definition.  Similar, it is not clear 
whether "c : B" should be a constructor declaration or whether the 
definition of c has been forgotten.

There is another reason why we would like to have a constructor keyword. 
  We could switch to telescope-style constructor declarations,

    constructorName (constructorTelescope) [: dataName pars indices]

Example:

   data Nat : Set where
     zero
     suc (n : Nat)

which is short for

   data Nat : Set where
     zero : _
     suc (n : Nat) : _

which in turn can be resolved to

   data Nat : Set where
     zero : Nat
     suc (n : Nat) : Nat

Currently, we cannot write

   data Nat : Set where
     zero : _
     suc  : (n : Nat) -> _

because it is not clear whether the meta variable _ is already the 
target type Nat, or another function type.

Cheers,
Andreas

On 05.11.12 9:07 PM, Serge D. Mechveliani wrote:
> People,
> there is a strange syntax difference between the `record' and `data'
> declarations with respect to bounding and `open' after `where'.
> Consider the example:
>
> ------------------------------------------------------------------------
> record LeftQuotient {c l : Level} (H : Semigroup c l)
>                      (a b : Semigroup.Carrier H) :  Set (max c l)
>    where
>    open Semigroup {{...}}     -- (1)
>    _~_ = Semigroup._\~~_ H    -- (2)
>    field
>      quot : Semigroup.Carrier H
>      ...
>
> data MbDivideLeft {c l : Level} (H : Semigroup c l)
>       (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) : Set (max c l)
>    where
>    open Semigroup {{...}}     -- (1')
>    _~_ = Semigroup._\~~_ H    -- (2')
>    ...
>    unsolvable :
>               (x : Carrier H) -> \neg ((x * b) ~ a) -> MbDivideLeft H a b
>    ...
> ------------------------------------------------------------------------
>
> The lines (1) and (2) do work,  while (1') and (2') do not parse.
> Has it sense to make this feature in `data' similar as in 'record' ?


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/