[Agda] Coinductive families

[Andreas Abel]

Thorsten, I mostly agree with your exposition.

But we also need to distinguish:

1) Internal representation. (sum, products, (co)induction)
2) External syntax. (data and record)

In particular, I do not think that Agda's record syntax is a very good  
idea and think that Haskell's syntax is better. In my practical  
experience, it is not an uncommon refactoring to turn a "record" into  
a data type by adding a field:

   data D = C1 { f1 :: A1, ..., fn :: An }    -- "record"

later add:

    | C2 ...

In Agda you have to rewrite record syntax into data syntax if you want  
to do this change.

Also, being a record is not necessary tied to having exactly one  
constructor, and you put forward the Vec example, which is an indexed  
record.

In my opinion, a record is more extensionally given as a data types  
whose complete set of projections is definable.  Lists are not records  
because their constructors are overlapping (both produce a List A),  
but Vec's constructor's are not overlapping (one produces a Vec A  
zero, the other a Vec A (suc n), which cannot be confused).

In MiniAgda you can define the Vec record by

   data Vec (A : Set) : Nat -> Set
   { vnil : Vec A zero
   ; vcons : [n : Nat] -> (vhead : A) -> (vtail : Vec A n) -> Vec A  
(suc n)
   } fields vhead, vtail

which creates the two destructors vhead and vtail.

The big question is: which indexed records give rise to modules?

Encoding indexed records in the way you describe below works of  
course, but is it a practical solution?

Cheers,
Andreas




On Oct 4, 2010, at 7:49 PM, Thorsten Altenkirch wrote:

> I think it is a good idea if we distinguish two issues:
>
> 1) The definitions of datatypes by constructors or destructors
>     corresponding to labelled sums (data) and labelled products  
> (codata)
> 2) The definition of recursive datatypes as either inductive or  
> coinductive
>     corresponding to initial algebras or terminal coalgebras.
>
> E.g. sometimes it is more natural to represent coinductive datatypes  
> in their constructor representations, eg. for colists. Also  
> decoupling the two allows a flexible syntax for mixed inductive /  
> coinductive datatypes (see Nisse's and main recent papers on this).
>
> In any case, I think it is a good idea to dualize our current way to  
> define indexed datatypes by indexed constructors to indexed records  
> defined by destructors as Dan and Andreas suggest. To add another  
> example, we can define Vec using destructors:
>
> record Vec (A : Set) : ℕ → Set where
>  destructor
>    hd : ∀ {n} → Vec A (suc n) → A
>    tl : ∀ {n} → Vec A (suc n) → Vec A n
>
> Dually to the fact that we can encode indexed datatypes using  
> equality and sigma-types, we can can encode these indexed records  
> using eqaulity and pi-types, namely
>
> record Vec (A : Set)(n : ℕ) : Set where
>  field
>    hd : ∀ {m} → n ≡ suc m → A
>    tl : ∀ {m} → n ≡ suc m → Vec A m
>
> And we can recover the constructors:
>
> nil : ∀ {A} → Vec A 0
> nil = record {hd = λ () ; tl = λ ()}
>
> cons : ∀ {A n} → A → Vec A n → Vec A (suc n)
> cons {A}{n} a as = record {hd = λ _ → a;
>                    tl = λ eq → tl' eq}
>  where
>  tl' : ∀ {m} → suc n ≡ suc m → Vec A m
>  tl' refl = as
>
> Cheers,
> Thorsten
>
>
>
> On 4 Oct 2010, at 09:04, Andreas Abel wrote:
>
>> Hi Dan,
>>
>> thanks for your post.  It's a pity you were not at the last Agda  
>> meeting in Nottingham where Anton Setzer gave a talk on this.  We  
>> have been discussing coinduction for two years on the Agda meetings  
>> now, an the conclusions we reached were quite similar to what you  
>> present here.
>>
>> This is my own digest of the discussion. Basically, when you write  
>> (in fantasy Agda)
>>
>> codata Stream (A : Set) : Set where
>>   cons : (head : A) -> (tail : Stream A) -> Stream A
>>
>> this means that you are defining a corecursive record
>>
>> record Stream (A : Set) : Set where
>>   destructor
>>     head : Stream A -> A
>>     tail : Stream A -> Stream A
>>
>> I am using a keyword "destructor" here instead of "field", because  
>> field does not allow you to mention the record you are destructing  
>> in the type.  But this is important for coinductive families, as  
>> you also point out, or, we could also call them "indexed records".
>>
>> It comes natural then to extend pattern matching to destructor  
>> patterns, so the constructor is creating an object defined by its  
>> observations.
>>
>> cons : .{A : Set} -> A -> Stream A -> Stream A
>> head (cons a as) = a
>> tail (cons a as) = as
>>
>> Of course, cons and the destructors could be created automatically  
>> from the above "codata" definition. If you go on and define map you  
>> get
>>
>> map : .{A B : Set} -> (A -> B) -> Stream A -> Stream B
>> head (map f s)  = f (head s)
>> tail (map f s) = map f (tail s)
>>
>> map does not reduce by itself, only if its head or tail is  
>> demanded.  Thus, there is no special care needed to prevent looping  
>> of the type checker in the presence of corecursion anymore.  Also,  
>> the subject reduction problem discussed on the Coq and Agda lists  
>> (posted by Nicolas Oury) is gone.
>>
>> The above definition of map could be generated from the constructor- 
>> based one automatically, I suppose, and should be the internal  
>> representation (part of the deal has been realized by Nisse and me  
>> already as "record pattern translation").
>>
>> An interesting special case is the Unit type (empty record)
>>
>> codata Unit : Set
>>    destructors
>>
>> We get
>>
>> unit : Unit
>> ()   -- no destructors
>>
>> and this makes, as you observed below, Unit the terminal type
>>
>> terminal : .{A : Set} -> A -> Unit
>> ()
>>
>> (We probably need a better syntax for "no destructors", maybe
>>
>> terminal a = ()
>>
>> to indicate that "terminal a" is of a type which has no destructors.)
>>
>> Then we can go on and have indexed records, as you also observe.
>>
>>> data Fin : ℕ → Set where
>>>  mk    : ∀{n} → Maybe (Fin n) → Fin (suc n)
>>>  empty : ⊥ → Fin 0
>>
>> This could be represented as
>>
>> record Fin : Nat -> Set where
>>   destructors
>>     fromSuc : .{n : Nat} -> Fin (suc n) -> Maybe (Fin n)
>>     fromZero : Fin 0 -> Bot
>>
>> and then we get the constructors
>>
>> mk : .{n : Nat} -> Maybe (Fin n) -> Fin (suc n)
>> fromFin (mk m) = m
>> -- fromZero does not match
>>
>> empty : Bot -> Fin 0
>> empty ()
>>
>> or
>>
>> fromZero (empty a) = a
>>
>> Cheers,
>> Andreas
>>
>> On Oct 4, 2010, at 4:47 AM, Dan Doel wrote:
>>
>>> On Sunday 03 October 2010 6:10:34 pm Nils Anders Danielsson wrote:
>>>> On 2010-10-01 15:09, Iain Lane wrote:
>>>>> record Tailspin : Set where
>>>>>
>>>>> field
>>>>>
>>>>>  Kaboom : Tailspin
>>>>>
>>>>> test : Tailspin
>>>>> test = ?
>>>>
>>>> I think the problem here is that you are using a recursive record  
>>>> type.
>>>> Such types are not really supported, but for some reason they are  
>>>> not
>>>> disallowed, maybe to allow experiments with coinductive records:
>>>>
>>>> record Stream (A : Set) : Set where
>>>>   constructor _∷_
>>>>   field
>>>>     head : A
>>>>     tail : ∞ (Stream A)
>>>
>>> I posted this in response to an issue on the bug tracker* (so  
>>> sorry if you're
>>> seeing this twice), but there may be some eyes here that it  
>>> wouldn't reach
>>> otherwise, and it's related to the above.
>>>
>>> I was thinking not long ago about notations for defining codata.  
>>> One nice
>>> special case is when the functor in question is a product. Since the
>>> observation is then T -> FT*GT*..., you can write it like:
>>>
>>> codata Stream A = Head :: A & Tail :: Stream A
>>>
>>> But, I was thinking about a more GADT/inductive family-like  
>>> syntax, and the
>>> obvious choice is:
>>>
>>> codata Stream (A : Set) : Set where
>>>  head :: Stream A -> A
>>>  tail :: Stream A -> Stream A
>>>
>>> where the list specifies the destructors, and the type being  
>>> defined is a
>>> product thereof, instead of a sum as in the inductive case (and  
>>> this is
>>> probably not surprising; inductives and sums are colimits, and  
>>> coinductives
>>> and products are limits). Charity handles type definitions in this  
>>> way.
>>>
>>> But, in the ordinary coinductive case, the first argument is  
>>> always the same,
>>> so we could think about eliding it, which of course produces the  
>>> suggestive:
>>>
>>> codata Stream (A : Set) : Set where
>>>  head :: A
>>>  tail :: Stream A
>>>
>>> and this looks exactly like records. And, in fact, it doesn't just  
>>> look like
>>> records, it *behaves* a lot like (Agda) records in several ways.
>>>
>>> 1) Both records and codata are defined by the observations that  
>>> can be
>>> performed on them, rather than how they're constructed, as  
>>> inductives are.
>>>
>>> 2) The eta rule for records is very much like proper extensional  
>>> equality for
>>> coinductive types: two values are equal if all observations/ 
>>> projections of the
>>> two are equal. For instance, for the empty record:
>>>
>>> record ⊤ : Set where
>>>
>>> with no projections, as a codata, we'd expect to, for any type not  
>>> needing to
>>> support any observations, there to be a canonical injection into  
>>> the empty
>>> record:
>>>
>>> ana : ∀{A : Set} → A → ⊤
>>> ana _ = _
>>>
>>> term : ∀{A} → (f : A → ⊤) → f ≡ ana
>>> term f = refl
>>>
>>> And lo and behold, there is. Not that this isn't equally justified  
>>> by
>>> induction for non-recursive records (inductive and coinductive  
>>> records should
>>> coincide when non-recursive), but the focus on equality of
>>> projections/observations seems like a coinductive take.
>>>
>>> 3) In the bug in question, there was a problem with the  
>>> termination checker
>>> not accepting code involving something like:
>>>
>>> foo ... (x , y) = ... (foo ... x) ... (foo ... y) ...
>>>
>>> because the match on (x , y) is translated to projections from the  
>>> record.
>>> However, Nils also pointed out that the following code should not  
>>> check:
>>>
>>> record R : Set where
>>>  constructor c
>>>  field
>>>    p : R
>>>
>>> foo : R -> R
>>> foo (c r) = foo r
>>>
>>> because it translates into:
>>>
>>> foo : R -> R
>>> foo r = foo (p r)
>>>
>>> which will not normalize (foo r => foo (p r) => foo (p (p r))  
>>> => ...). The
>>> solution found was to make 'p r <= r', so that the checker is  
>>> aware that the
>>> argument isn't getting *bigger*, but it isn't necessarily getting  
>>> smaller,
>>> either (the latter part invalidates foo). However, is this  
>>> situation not
>>> rather strange?
>>>
>>> If R were indeed inductive, we'd expect it to be empty. For  
>>> instance:
>>>
>>> data R : Set where
>>>  c : R -> R
>>>
>>> ¬R : R → ⊥
>>> ¬R (c r) = ¬R r
>>>
>>> but this is exactly the function we've just ruled out, because it  
>>> won't
>>> normalize with records. And in the inductive case, p r must be  
>>> smaller than r,
>>> but we are treating it as if it isn't.
>>>
>>> However, if records are coinductive, the above makes perfect sense:
>>>
>>> a) p r <= r, because coinductive types admit circular definitions,  
>>> and so
>>>   projecting out of one may yield something of equal size, but not  
>>> greater.
>>> b) foo is obviously not a productive corecursive definition, so  
>>> it's natural
>>>   to rule it out. There's no longer a strange situation where we  
>>> must rule
>>>   out an ostensibly inductively justified definition because it  
>>> would fail
>>>   to normalize.
>>> c) It's okay that we can't prove that R is uninhabited, because it  
>>> *is*
>>>   inhabited by c (c (c (c ...))).
>>>
>>> 4) I haven't bothered to think this through much yet, but:  
>>> coinductives had
>>> problems (and still do in Coq, I think) with subject reduction  
>>> when they were
>>> initially conceived of as being built out of constructors. Taking  
>>> the view
>>> that values of coinductive type are opaque things with observation  
>>> functions
>>> seems important to a well-working theory.
>>>
>>> When constructors and matching thereon were added for records, I  
>>> believe there
>>> were similar issues with subject reduction, which is why the  
>>> matches are now
>>> translated to projections.
>>>
>>> I suspect these two situations are related.
>>>
>>> So, how about it? Is it possible that Agda has had non-recursive  
>>> coinductive
>>> types all along, and that codata would have been better added by  
>>> fixing the
>>> way that recursive records work?
>>>
>>> On the topic specified in the subject line, I've been thinking  
>>> about what
>>> coinductive families might look like. Inductive families are  
>>> initial algebras
>>> in a slice category (which makes them a way of specifying how an  
>>> entire family
>>> T i is constructed at once), so a coinductive family should be a  
>>> final
>>> coalgebra in the same. I'm not sure I have the chops to specify  
>>> what that is,
>>> exactly, *but*, I can speculate wildly.
>>>
>>> We allow the specification of inductive families by allowing  
>>> constructors to
>>> target arbitrary values of the index:
>>>
>>> data Fin : ℕ → Set where
>>>  zero : ∀{n} → Fin (suc n)
>>>  suc  : ∀{n} → Fin n → Fin (suc n)
>>>
>>> So, it stands to reason that we should be able to specify  
>>> coinductive families
>>> by allowing projections to specify arbitrary starting indices:
>>>
>>> codata CoFin : ℕ → Set where
>>>  pred  : Fin (suc n) → Maybe (Fin n)
>>>  empty : Fin 0 → ⊥
>>>
>>> Of course, where the 'n' comes from in the pred destructor is  
>>> something I
>>> haven't figured out yet. :) Perhaps the presence of the n at all  
>>> is an
>>> illusion in both cases. Edwin Brady et al. tell us that inductive  
>>> families
>>> need not store their indices**. Perhaps this is not merely an  
>>> optimization,
>>> but a recognition that quantification over indices is part of a  
>>> schema for
>>> defining many constructors, not actually a field of the  
>>> constructor, and:
>>>
>>> pred  : ∀{n} → Fin (suc n) → Maybe (Fin n)
>>>
>>> is a similarly sensible schema (apologies if the paper actually  
>>> makes this
>>> observation; it's been a while since I read it).
>>>
>>> If this definition is a little surprising, note that we could also  
>>> write Fin
>>> as:
>>>
>>> data Fin : ℕ → Set where
>>>  mk    : ∀{n} → Maybe (Fin n) → Fin (suc n)
>>>  empty : ⊥ → Fin 0
>>>
>>> which makes it a little clearer that we're dealing with the same  
>>> functors
>>> here.
>>>
>>> Thoughts?
>>>
>>> -- Dan
>>>
>>> [*] http://code.google.com/p/agda/issues/detail?id=334
>>>
>>>
>>> [**] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.3849
>>>
>>> Also, here's a fancier proof than the top one: the anamorphism  
>>> into the
>>> product record is unique. Of course, I don't expect eta rules to  
>>> extend nicely
>>> into providing extensional equality of recursive records-as-codata.
>>>
>>> module Prod where
>>> record _×_ (A B : Set) : Set where
>>>  field
>>>    fst : A
>>>    snd : B
>>>
>>> open _×_
>>>
>>> ana : ∀{A B C : Set} → (C → A) → (C → B) → C → A × B
>>> ana f g x = record { fst = f x ; snd = g x }
>>>
>>> comm₁ : ∀{A B C} → (f : C → A) (g : C → B) → (fst ∘  
>>> ana f g) ≡ f
>>> comm₁ f g = refl
>>>
>>> comm₂ : ∀{A B C} → (f : C → A) (g : C → B) → (snd ∘  
>>> ana f g) ≡ g
>>> comm₂ f g = refl
>>>
>>> open ≡-Reasoning
>>>
>>> univ : ∀{A B C : Set} → (f : C → A) (g : C → B)
>>>     → (h : C → A × B)
>>>     → (fst ∘ h) ≡ f
>>>     → (snd ∘ h) ≡ g
>>>     → h ≡ ana f g
>>> univ f g h eq₁ eq₂ = begin
>>>                       (λ x → h x)
>>>                     ≡⟨ refl ⟩
>>>                       (λ x → record { fst = (fst ∘ h) x
>>>                                     ; snd = (snd ∘ h) x })
>>>                     ≡⟨ cong (λ k →
>>>                              λ x → record { fst = k x
>>>                                           ; snd = (snd ∘ h) x })
>>>                         eq₁ ⟩
>>>                       (λ x → record { fst = f x
>>>                                     ; snd = (snd ∘ h) x })
>>>                     ≡⟨ cong (λ k → λ x → record { fst = f  
>>> x
>>>                                                 ; snd = k x })
>>>                         eq₂ ⟩
>>>                       (λ x → record { fst = f x ; snd = g x })
>>>                     ≡⟨ refl ⟩
>>>                       (λ x → ana f g x)
>>>                     ∎
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>> 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/
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>

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/