[Agda] Coinductive families
Thorsten Altenkirch
txa at Cs.Nott.AC.UK
Tue Oct 5 12:35:50 CEST 2010
On 4 Oct 2010, at 22:26, Andreas Abel wrote:
> 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),
Just to state the obvious, Lists can be represented as records namely:
record List (A : Set) : Set where
constructor list
field
isCons : Bool
hd : T isCons → A
tl : T isCons → List A
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?
> 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?
No, I guess we want the destructor syntax. But it least it is clear what it means.
Cheers,
Thorste
> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101005/95c3ac3e/attachment-0001.html
More information about the Agda
mailing list