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

[Serge D. Mechveliani]

On Tue, Nov 06, 2012 at 11:52:20AM +0100, Andreas Abel wrote:
> 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. 


I think, this will be good -- for the _language_. 
Is the Agda owner going to add this to the next Agda _language_ version 
and release?


> 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.

In this particular example any constructor coarity for D must be  D.
Do I understand this correct?
Changing to  f : D  presents the ambiguity you are talking of.
Right?

Also consider   data D ...
                where
                open Foo {{...}} 
                f : ...

(2) It is desirable to allow `open' here.

Suggestion 3 for the language. Current domain denotation
---------------------------------------------------------

To locally denote  `this' (`this defined type') the domain (constructor)
being defined by  `data',  
and to put it as a synonym
(choose and reserve an appropriate word:  this, it, $$, @@, ...).  

Consider an example:

  data MbDivideLeft {c l : Level} (H : Semigroup c l)
             (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) :  Set _
    where
    quot       : Nat -> MbDivideLeft H a b                         -- (1)
    quot2      : Nat -> MbDivideLeft H a (a * b)                   -- (2)
    unsolvable :
      let open Semigroup {{...}}
      in
      (x : Carrier H) -> \neg ((x * b) ~~ a) -> MbDivideLeft H a b  -- (3)

In such examples a large expression  `MbDivideLeft H a b'  tends to 
repeat several times. So, let `this' be a local synonym:
    ...
    quot       : Nat -> this
    quot2      : Nat -> this H a (a * b)      --
    unsolvable : let open Semigroup {{...}}
                 in  (x : Carrier H) -> \neg ((x * b) ~~ a) -> this

Regards,
Sergei