[Agda] Coinductive families

[Andreas Abel]

On Oct 5, 2010, at 5:25 PM, Nils Anders Danielsson wrote:

> On 2010-10-05 15:59, Dan Licata wrote:
>> Perhaps someone could review for me why you want to treat
>> them differently for definitional equality, like Agda currently does.
>> For example: does something go wrong if you identify records with
>> one-branch datatypes.  I.e. for every one-branch datatype, you
>> automatically generate all of the projections and make eta (p =  
>> (fst p,
>> snd p)) hold definitionally?
>
> Some reasons:
>
> * Using different kinds of definitional equality for one- and
>  two-constructor data types (or recursive and non-recursive
>  one-constructor data types) may be confusing. By using "record" you
>  explicitly ask for η-equality.

But this would not require a completely different syntax.

> * If Agda generated projections automatically, what would they be
>  called? All record fields have names.

data Sigma ++(A : Set) ++(B : A -> Set) : Set
{ pair : (fst : A) -> (snd : B fst) -> Sigma A B
}
fields fst, snd


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/