Syntax of 'data' declaration [Re: [Agda] boundings in data-where]
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Nov 6 17:41:45 CET 2012
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/
More information about the Agda
mailing list