[Agda] Coinductive families
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Oct 4 10:04:19 CEST 2010
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/
More information about the Agda
mailing list