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