[Agda] Coinductive families

[Andreas Abel]

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?

Cheers,
Andreas


On Oct 5, 2010, at 2:52 PM, Thorsten Altenkirch wrote:

> On 5 Oct 2010, at 12:42, Dan Doel wrote:
>
>> On Tuesday 05 October 2010 6:35:50 am Thorsten Altenkirch wrote:
>>
>>> Btw, when trying to define append
>>>
>>> append : ∀ {A} → List A → List A → List A
>>> append (list true h t) bs = list true h (λ _ → append (t _) bs)
>>> append (list false _ _) bs = bs
>>>
>>> the termination checker complains. I am not sure why, since (t _) is
>>> smaller than (list true h t), isn't it?
>>
>> This theoretically rewrites to something like:
>>
>> append l bs with isCons l | hd l | tl l
>> ... | true  | h | t = list true h (\_ -> append (t _) bs)
>> ... | false | _ | _ = bs
>>
>> and with the projection rule:
>>
>> t = tl l <= l
>>
>> so, no; it is merely not-bigger (or, possibly, actually bigger if  
>> your version
>> is old enough; not sure).
>
> But if I replace my record with the isomorphic data type, then it is  
> fine.
>
> data List (A : Set) : Set where
>  list : (isCons : Bool)
>       → (hd : T isCons → A)
>       → (tl : T isCons → List A)
>       → List A
>
> append : ∀ {A} → List A → List A → List A
> append (list true h t) bs = list true h (λ _ → append (t _) bs)
> append (list false _ _) bs = bs
>
> Could we not view record types as data types with one constructor?
>
> T.
>
>
>> This is the same rule used to disqualify:
>>
>> record R : Set where
>>   constructor c
>>   field
>>     p : R
>>
>> foo : R -> R
>> foo (c r) = foo r
>>
>> which *actually* translates internally to:
>>
>> foo : R -> R
>> foo r = foo (p r)
>>
>> which won't normalize. append can't be translated, I think, because  
>> the match
>> on isCons blocks translation to projections (the translation I gave  
>> is
>> probably a bit much to expect of the checker), but Andreas changed  
>> the rule
>> for pattern matching on record constructors to make the two  
>> consistent, I
>> think.
>>
>> -- Dan
>
>

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/