semantically unjustified coinduction

[mikeshulman]

semantically unjustified coinduction

[pigworker]

We didn't have coinduction in Epigram 1, but we were certainly on that case in Epigram 2. We did not get as far as mixing Mu and Nu. (Co-)datatypes in Epigram 2 were given by defining descriptions of polynomial functors: we had type constructors Mu and Nu which took least and greatest fixpoints, respectively. Data in Nu were introduced by coiteration, but we also allowed the constructor. Definitional equality expanded coiteration only on demand but would proceed structurally under the constructor. We were briefly tempted to treat "being compared to a constructor term" as a demand, but that either leaves definitional equality intransitive or solves the Halting Problem. Propositional equality was bisimulation, and that is sufficient to make dependent case analysis definable.

If i had known then what I know now, I would have made Mu and Nu internal to the datatype of functor descriptions. That would descriptions a syntax with binding, which seemed too scary at the time, but today would be less so if we were to teach definitional equality the equational theory of substitution. It's important, in general, to allow arbitrarily deep interleavings of Mu and Nu. E.g., if one is modelling session types, it could be that the client is allowed to ask the server for as many strings as it wants: the client is inductive and the server is coinductive, so the client must eventually stop asking, but it is the server who is responsible for the finiteness of each string.

(Co)programming with (co)recursors is good sport, but going beyond single step (co)recursion often requires some sort of explicit buffering construction. Sized types are neater, and better suited to higher-order programming. One thing data descriptions might let you do is compute, for a given description, its size-indexed counterpart. (Co)recursors could then say "if you can justify your (co)recursion on sized data, I'm happy to run it on unsized data". Not only can we overload constructors (never ask the type of a constructor; ask rather how it's admitted by a type), we can make local refinements to the types (plural) of data in order to explain the validity of computations.

[andreasabel]

@jonsterling Are you referring to this:

For example, we would like to use the cons constructor for sized lists at type
A → Listₛ A ∞ → Listₛ A ∞
but this is impossible with ∞ ≮ ∞. As a workaround, we can define a consing operation for lists at ∞ that is extensionally equal to cons, but this requires a pattern match on the input list – an inefficiency that should not be necessary.

Well, you can type cons as A → Listₛ A ∞ → Listₛ A (∞ + 1) and then use the fact that these two list types are the same because the fixpoint has been reached at ∞. See for instance the type of the constructors on page 15.
Maybe what is written in the introduction (2.2) isn't all accurate.

The idea to extend the considered ordinals to ∞ + n is from:

Andreas Abel, Brigitte Pientka:
Well-founded recursion with copatterns and sized types. J. Funct. Program. 26: e2 (2016)

[mikeshulman]

When I say categorical semantics, I mean that it should have semantics in every category of a particular class, such as Grothendieck toposes. Semantics in one particular category like reflexive graphs is something, but not sufficient to be able to use the type theory as an internal language for general categories.

[mikeshulman]

Usually, semantics does not happen in general categories, but you always need to place extra conditions, like cartesian-closed etc.

Yes, in the previous sentence I said

I mean that it should have semantics in every category of a particular class.

[mikeshulman]

So disregarding sizes, if you want parametricity, how do you do this in your favorite categories? How do you ensure that e.g. (A : Set) -> List A -> List A is parametric in A.

What do you mean by "parametric" in categorical semantics?

[mikeshulman]

If you mean things like does it satisfy free theorems, the answer is that it doesn't usually.

[dolio]

I don't recall the exact details but Henning Basold's thesis also tries to give a better account of mixed induction and coinduction, and it might have more general categorical semantics.

In particular, I believe it is structured along the lines of what Conor mentions, where the language for specifying polynomial functors is closed under least/greatest fixed points (and I think it proves that that works semantically). It seems (to me) like that is the sort of thing you need for (co)data types to be properly composable in the desired way.

[andreasabel]

Coinduction by guardedness is broken when inductive and coinductive types are mixed because it always assumes that the coinductive type (Stream) is the outer one even when in your definition it is clearly inside the inductive type (Ord).
This is a known problem:

Thorsten Altenkirch, Nils Anders Danielsson:
Termination Checking in the Presence of Nested Inductive and Coinductive Types. PAR@ITP 2010: 101-106

My solution here is sized types. With sized types you can faithfully express what you mean in this situation.
However, sized types are expert only as well, because Agda will just believe your size assignments and you can prove False with it.
I am afraid we only have expert only approaches to coinduction at this point.

Personally, I still think that sized types are less broken as, contrary to guardedness, they do not pervert the definitions you have written into something you clearly did not mean.

Prior art:

• #5273

[mikeshulman]

Thanks! Sorry that I missed the earlier issue (I was only searching for "coinduction" not "guardedness"). But it looks like 3 years have passed without any progress. If the theoretical problem is too hard to solve right now, would it be possible to just check for potentially-problematic nestings and reject them? It seems a bad situation for Agda to continue accepting definitions like this without even a warning. The stackexchange answer I linked to makes it sound as though this is even the intended behavior.

[andreasabel]

I checked and the OP is correctly rejected by the new type-based termination checker contributed by @knisht :

• #7152

So maybe in the long run we can discontinue the --guardedness termination method in favour of --type-based-termination, and need not invest more work into --guardedness.

[mikeshulman]

That sounds promising, I guess.

Is anything known about whether a function accepted by any of these termination checkers is in principle expressible using the standard recursors?

[andreasabel]

Is anything known about whether a function accepted by any of these termination checkers is in principle expressible using the standard recursors?

If you code well-founded recursion with standard recursors, you get extra function arguments (accessibility proofs) that are matched on, so you get at least different definitional equality (for open terms). Closed terms of ground type should still reduce to the same value, though.
So, extensionally, yes, but intensionally, no, I'd say. And we usually care about the latter when developing proofs.

[nad]

If you code well-founded recursion with standard recursors, you get extra function arguments (accessibility proofs) that are matched on, so you get at least different definitional equality (for open terms). Closed terms of ground type should still reduce to the same value, though. So, extensionally, yes, but intensionally, no, I'd say. And we usually care about the latter when developing proofs.

It might also be the case that it is impossible to prove accessibility in certain cases.

Didn't you use some kind of impredicativity to verify the soundness of sized types? Perhaps the proof-theoretic strength sometimes goes up when sized types are added to a type theory.

[mikeshulman]

That's too bad. Is there any known termination-checker that doesn't alter the definitional equalities vis-a-vis the standard recursors?

(I don't have a philosophical attachment to recursors, but as far as I know, recursors are all that we know how to model directly in categorical semantics. But I suppose one might try to improve that situation too.)

[jonsterling]

That's too bad. Is there any known termination-checker that doesn't alter the definitional equalities vis-a-vis the standard recursors?

(I don't have a philosophical attachment to recursors, but as far as I know, recursors are all that we know how to model directly in categorical semantics. But I suppose one might try to improve that situation too.)

Not sure if this helps, but my recollection is that this was one of the main goals that Conor McBride had when designing his account of elaborating recursive pattern-matching definitions to actual recursors (in his thesis with OLEG, and later with Epigram): if you write something that looks like an equation, it better be something you can realise by an equation with recursors. So I believe that Epigram's elaboration had the property you want, and it may even be the case that Lean's elaboration, which I believe is based on those ideas, has this property too (but don't quote me).

[mikeshulman]

Thanks! Do Epigram or Lean include coinduction?

[jonsterling]

@mikeshulman I can't remember how far they got with coinduction in Epigram. There was a lot of work done by Conor at the time of Epigram 2 in that direction, at least on the theoretical end: for instance, in this paper http://strictlypositive.org/ObsCoin.pdf he talks about his intention to implement a certain treatment of coinduction in Epigram, but I am not sure what happened after that.

In Lean, there is to my knowledge no built-in support for coinduction. On the other hand, there has been some preliminary work on adding coinductive datatypes using Lean 4's elaborator reflection support; this MSc thesis by Alex Keizer looks relevant: https://eprints.illc.uva.nl/id/eprint/2239/1/MoL-2023-03.text.pdf. But I don't think this work contains a treatment of corecursive functions, etc.

[mikeshulman]

Thanks! As with recursors, I believe that corecursors are all we know how to model in categorical semantics (terminal coalgebras). So if sized types can be (in theory) reduced to corecursors preserving definitional equalities, or if someone can prove that they have categorical semantics, then I'm happy to use them; but otherwise I would want to stick to something with known semantics.

[pigworker]

There are several things worth doing here, many of which I'm too busy for, so have some free ideas on me. As I said, I'd like to look at localising the notion of size, so that it's in play for the construction of a computation but not in the faces of that computation's clients. I'd like to consider not absolute size, but relative size, with a sort of Noetherian intuition that while some things are really very big indeed, you can't keep on picking substructures forever. And I would indeed like to show that the resulting formulation can be expressed as a buffering construction on top of standard (co)recursors at the expense of (1) a combinatorial explosion, and (2) a great deal of tedious inlining (typically of recursive calls lifted functorially).

[andreasabel]

@mikeshulman wrote:

if someone can prove that they have categorical semantics,

Would this semantics be categorical enough: https://limperg.de/paper/msc-thesis/thesis.pdf ?

[jonsterling]

@andreasabel This looks indeed like proper semantics, but isn't the discussion in Section 2.2 a nail in the coffin? Or is there another proposal for how to deal with sizes consistently without requiring these spurious pattern matches?

[jonsterling]

Thanks for this further info @andreasabel !

Quick question: when you say that the two list types are the same, do you expect them to be definitionally equal, or is this up to isomorphism?

[andreasabel]

@mikeshulman wrote:

Semantics in one particular category like reflexive graphs is something, but not sufficient to be able to use the type theory as an internal language for general categories.

Well, you can drop the reflexive graphs, but then you lose size-parametricity. Maybe it is possible to replace reflexive graphs by some universal property?
Frankly, I don't know what is allowed and what not. Usually, semantics does not happen in general categories, but you always need to place extra conditions, like cartesian-closed etc.

So disregarding sizes, if you want parametricity, how do you do this in your favorite categories? How do you ensure that e.g. (A : Set) -> List A -> List A is parametric in A. Can you do this with some universal property? Maybe this technique could be transferred then.

(Also, I usually think of sizes as external to the category which interprets types and terms.)

[mikeshulman]

Thanks for that reference! It does give a good general categorical account of mixed induction and coinduction, with signatures that are closed under both least and greatest fixed points. But it looks to me like the only means of defining functions on these types that he ends up with, in the dependently typed and categorically general case, is with the recursors and corecursors. So it doesn't solve the problem of finding categorical semantics for a more general (co)pattern-matching syntax with some kind of termination/productivity checker. (He does discuss (co)pattern matching in the simply typed case, but I don't think he gives a termination/productivity checker.)