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

[Andreas Abel]

On 06.11.2012 16:56, Serge D. Mechveliani wrote:
> 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?

This is up to discussion.  I just made a proposal.

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

Right.  A and B were meant to be placeholders of arbitrary types, 
potentially involving D.

> Also consider   data D ...
>                  where
>                  open Foo {{...}}
>                  f : ...
>
> (2) It is desirable to allow `open' here.

Yes.

> 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

I am not so sure about this.  Id does not seem to make it so much 
shorter.  If declarations are allowed in 'data', then you can do it yourself

   data D params : indices -> Set where
     this = D params
     constructor
       c : telescope -> this inds

Cheers,
Andreas


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