[Agda] Coinductive families

[Dan Licata]

Hi everyone,

I agree with Andreas that distinguishing different kinds of conjunctions
is important.  In fact, the distinction between * and & is not exclusive
to linear logic.  You can tease these two apart in regular old
intuitionistic logic by polarizing the types---dividing them up into
positive (intro-oriented) and negative (elimination-oriented).  See
e.g. Noam Zeilberger's thesis.
https://www.pps.jussieu.fr/~noam/thesis.pdf 
When there are effects around, you can tell * and & apart: a value of A
& B can have suspended effects, but a value of A * B cannot.

But an interesting question which I don't know the answer to is: what is
the role of these different conjunctions, and polarity in general, when
everything is pure?  If we separate out the induction/coinduction
aspect, then is there any semantic difference between a record type
defined by destructors, and the notion of pairing implicit in a datatype
with a single constructor?

For example, & (defined as a record) and * (defined as a datatype) are
isomorphic (propositionally).  So the difference must be in definitional
equality.  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?  I think Coq does this, but without making
eta definitional.

Regarding Andreas's question about the theory of all of this, I wonder
whether you could sort it out by actually having both conjunctions in
the core language, and then providing a source notation that lets
programmers be sloppy about which one they mean.  Elaboration would try
to guess the most convenient one, and insert the mediating isomorphisms
when necessary.  Certain code would force one decision or the other:
Pattern matching on record constructors would force it to be *, not
&. Needing eta would force it to be & (assuming you can't build in eta
for * definitionally, like I asked about above).

-Dan

PS: By analogy with coproducts, the full eta rule for * should be
  C t = split t as (x,y) in C (x,y) 
  for any C : A * B -> ...
That is, you get unique maps out of *, but unique maps into &.
However I wouldn't expect to get this one definitionally.  

On Oct05, Andreas Abel wrote:
> Maybe intutionistic linear logic can shed some light here.  We need to  
> distinguish between strict product (tensor, *) and lazy product  
> (conjunction, &).
> 
> A record should be understood in terms of &.  It is lazy and defined  
> by its projections.  Eta is natural for &:
> 
>   p = (fst p, snd p) : A & B
> 
> A data type with one constructor is a unary sum of a strict product.   
> It is eliminated by pattern matching.
> Eta for the strict product only exists in the clumsy form,
> 
>   t = split t as (x,y) in (x,y) : A * B
> 
> which does not help you much in terms of solving metas and checking  
> equality.
> 
> Currently records are hybrids, because we have record patterns.  If  
> all record patterns could be translated away, we could understand  
> records in terms of &.  But currently we allow record patterns that  
> cannot be translated away, such as where record patterns are mixed  
> with data constructor patterns.
> 
> There is no clear theory on this, or is there?
> But it works well in practice, or doesn't it?  All subject reduction  
> problems banned?
>