[Agda] Coinductive families

[Andreas Abel]

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

> On 2010-10-05 14:14, Andreas Abel wrote:
>> 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.
>
> I'm fairly certain that we can translate away these patterns, but  
> there
> is no immediate need to do so, because the translation would be
> observationally indistinguishable from what we generate now (modulo  
> any
> bugs).


How would you translate away the patterns in Thorsten's example?

record List (A : Set) : Set where
   constructor list
   field
     isCons : Bool
     hd : T isCons → A
     tl : T isCons → 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

Here are some prototypical translations:

With "if":

append l bs = if (isCons l)
   then list true (hd l _) (\ _ -> append (tl t _) bs)
   else bs

(This is only type correct with "smart if", i.e., with the constraint  
isCons l = true in the then-branch.)

With "with":

append l bs = append' l bs (isCons l)
append' l bs true = list true (hd l _) (\ _ -> append (tl t _) bs)
append' l bs false = bs

(This version is not type-correct, needs to be refined by the inspect- 
pattern.)

In the first case, append l bs loops. In the second case it terminates  
(but more by accident) because matching on (isCons l) blocks unfolding.

Thus, depending on the translation there is an observable difference!

Anyway, for now the termination checker rejects all versions of append  
given here,  shout if you disagree!

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/