walker (Feb 12 2022 at 15:19): walker (Feb 12 2022 at 15:19):Not strictly related to coq, but I am learning it in coq context.. Does any one knows good place to learn about coinductive types and coinduction in I am struggling to see the difference between inductive types and co-inductive types in coq.
Karl Palmskog (Feb 12 2022 at 15:41): Alexander Gryzlov (Feb 12 2022 at 15:44):https://plv.mpi-sws.org/paco/ might be also useful
walker (Feb 12 2022 at 15:49):Thanks a lot every, probably I would start by the tutorial, and decide what to do next from there!
Ali Caglayan (Feb 12 2022 at 15:55):Don't forget about the Coq reference manual. There is an important caveat that you should keep in mind. Many of the older sources linked above will treat coinductive types in a "positive" manner, using constructors and pattern matching.
This can be argued to be a historical mistake, and is known to break important properties of Coq. The alternative is the "negative" presentation of coinductive types, which essentially look like records whose fields can reference the record type.
Karl Palmskog (Feb 12 2022 at 15:57):but nobody uses primitive projections to do coinduction currently
Karl Palmskog (Feb 12 2022 at 15:57):and I would strongly advise not to do that, since syntax and semantics is terrible
Karl Palmskog (Feb 12 2022 at 16:04):in contrast, Pierre-Marie's proposal for fixing of "breaking of important properties" looks bearable and will not kill off coinduction in the Coq ecosystem, like mandating primitive projections will: https://github.com/coq/coq/pull/10764
walker (Feb 12 2022 at 16:35):noted thanks everyone!
Yannick Zakowski (Feb 12 2022 at 17:08):Karl Palmskog said:
but nobody uses primitive projections to do coinduction currently
I don't know if that's true. We do in the Interaction Trees library and other experimental projects related: https://github.com/DeepSpec/InteractionTrees/
And fwiw so does paco in its internals, though it's not visible from the user side.
Yannick Zakowski (Feb 12 2022 at 17:10):And more generally on the topic of coinduction in Coq, I strongly recommend Pous's library as a potential alternative to paco: https://github.com/damien-pous/coinduction
I tend to find it more accessible as it builds on a cleaner foundation.
Arpan Agrawal (Feb 14 2022 at 10:10):According to http://flint.cs.yale.edu/cs428/coq/doc/faq.html, Eduardo Gimenez' thesis (Reference number 8 on the page) is a good resource
Ali Caglayan (Feb 28 2022 at 17:35):Karl Palmskog said:
and I would strongly advise not to do that, since syntax and semantics is terrible
What did you mean by this?
Ali Caglayan (Feb 28 2022 at 17:36):I am very confused since I was under the impression that negative coinductive types had a semantics that made sense, whereas for positive coinductive types that is not the case.
Ali Caglayan (Feb 28 2022 at 17:37):Have you got any information on the semantics of positive coinductive types?
Karl Palmskog (Feb 28 2022 at 17:56):@Ali Caglayan please see the Q&A I had with PMP here: https://proofassistants.stackexchange.com/questions/583/what-is-the-state-of-coinductive-types-and-reasoning-in-coq
There is a reason that primitive projections are unpopular. In my view, the connection between records and coinductive types should be nonexistent. PMP's positive types would at least make sense.
Ali Caglayan (Feb 28 2022 at 18:01):Can you expand on why there should be no connection between records and coinductive types?
Karl Palmskog (Feb 28 2022 at 18:02):I want to express a coinductive datatype or relation, I don't want to declare some weird record that can't be accessed. This is not hard
Ali Caglayan (Feb 28 2022 at 18:03):Have you got some examples of datatypes in mind?
Karl Palmskog (Feb 28 2022 at 18:04):streams, infinite trees?
Ali Caglayan (Feb 28 2022 at 18:05):For streams you have a one constructor coinductive type, isn't a record precisely what having one constructor means (in the non-indexed case)?
Ali Caglayan (Feb 28 2022 at 18:07):And could you elaborate on "weird record that can't be accessed"?
Karl Palmskog (Feb 28 2022 at 18:08):Paulin introduced inductive datatype declarations into Coq, and Gimenez mirrored her syntax for coinductive types. Why would I want to use anything else? The burden is basically on you to show convincingly why switching to primitive projections everywhere only for coinductive declarations is a good idea.
Karl Palmskog (Feb 28 2022 at 18:10):you can see similar reasoning here: https://github.com/coq/coq/pull/10764#issuecomment-532771463
Ali Caglayan (Feb 28 2022 at 18:12):I'm trying to understand why people are using positive coinductive types in Coq, and so far the only convincing reason I've found is that "negative coinductive types weren't around then". I'm looking to understand what people expect when they do coinduction.
Gimenez "mirroring syntax" doesn't seem quite correct to me. Inductive datatypes are typically thought of as the least fixed point of something. Being the least, they have to somehow map into every other fixed point hence you get an elimination principle. Coinductive datatypes are typically thought of as the greatest fixed point of something. Being the greatest you have to map other fixed into them. This is why I don't expect to see (multiple) constructors when talking about coinductive types.
Ali Caglayan (Feb 28 2022 at 18:14):Karl Palmskog said:
you can see similar reasoning here: https://github.com/coq/coq/pull/10764#issuecomment-532771463
This thread is also very confusing, but it seems that the quarrel is rather with PMP's "complicated" syntactic criterion rather than anything concrete about negative coinductive types.
Karl Palmskog (Feb 28 2022 at 18:18):What exactly is confusing about this quote from Xavier:
Coq's positive coinduction leads to awkward proofs (manual unrollings, nothing computes, etc) but the specifications are quite nice. You can take Capretta's PhD thesis, or the Leroy-Grall paper on coinductive natural semantics, and transcribe the mathematical descriptions as coinductive types and predicates that look like the maths.
Paolo Giarrusso (Feb 28 2022 at 18:18):Paulin introduced inductive datatype declarations into Coq, and Gimenez mirrored her syntax for coinductive types. Why would I want to use anything else?
Because codata is _dual_ to data. Coinduction with negative types works in Agda and makes lots of sense (at least ignoring sized types).
Karl Palmskog (Feb 28 2022 at 18:19):the negative declarations look like garbage
Paolo Giarrusso (Feb 28 2022 at 18:22):apologies for mistaking this for a discussion, but I don't care enough for coinduction to deal with this much emotion.
Karl Palmskog (Feb 28 2022 at 18:27):but what exactly is your argument then? Rewrite tens of thousands of lines of Coq proofs because it makes sense in Agda?
Karl Palmskog (Feb 28 2022 at 18:29):I'm fine with primitive projections being available, but if the only argument is: it works in Agda and the previous syntax seems incorrect - why would anyone want to port code? The best solution is probably just to get https://github.com/coq/coq/pull/10764 merged
Ali Caglayan (Feb 28 2022 at 18:33):Let's remove Agda from the discussion, since that should have zero weight here. What I'm simply trying to understand is are there any semantics for positive coinductive types? The semantic picture which gets discussed when talking about coinduction which I outlined above seems to indicate that we expect to see negative coinductive types.
Karl Palmskog (Feb 28 2022 at 18:36):have you read Gimenez's thesis and papers? I already link to https://link.springer.com/chapter/10.1007/3-540-60579-7_3 in the StackExchange post
Karl Palmskog (Feb 28 2022 at 18:56):if the defining feature of negative types are a single constructor, does this mean you have to use option to get anything close to possibly-infinite/lazy lists? For example:
CoInductive trace : Type :=
| Tnil : A -> trace
| Tcons : A -> B -> trace -> trace.
You can convert any positive coinductive into a negative by first breaking the recursion into a non-recursive functor and then wrap it in a single-field coinductive. And I agree it looks silly.
Li-yao (Feb 28 2022 at 19:02):Inductive traceF (X : Type) : Type := Tnil : A -> traceF X | Tcons : A -> B -> X -> traceF X.
CoInductive trace := { untrace : traceF trace }.
oh gods.. the only way I can see this being used [the positive version] is by compilation akin to Equations. That is, one would write everything as positive types first and then convert them to negative.
Ali Caglayan (Feb 28 2022 at 19:06):Right, but the semantics of that thing are well understood, so if Coq compiled "positive" coinductive definitions in the background, would anybody care?
Karl Palmskog (Feb 28 2022 at 19:07):as also discussed on the StackExchange, you have to also introduce axioms
Ali Caglayan (Feb 28 2022 at 19:08):Right, but also discussed is the fact that funext is a thing, and few people seem to mind.
Karl Palmskog (Feb 28 2022 at 19:09):also, most don't care about SR breakage
Karl Palmskog (Feb 28 2022 at 19:09):so I think we are still at an impasse
Li-yao (Feb 28 2022 at 19:12):Wouldn't people who don't care about SR be just as happy with adding the eta rule as an axiom?
Ali Caglayan (Feb 28 2022 at 19:15):I don't really care that people like to write their coinductive types in a positive way, Li-yao already demonstrated how that can be overcome using a "compilation". SR breakage isn't a deal breaker for me but rather a symptom of a bigger problem which is that there are no good semantics for positive coinductive types AFAICT. If there are, please tell me!
Karl Palmskog (Feb 28 2022 at 19:15):OK, define first what you mean by "good semantics"
Karl Palmskog (Feb 28 2022 at 19:16):then the next step might be to demonstrate why Gimenez's semantics / the current positive types implementation is not "good" according to the definition and why the proposal in PR 10764 is not "good" either. In the second case, it may be better to take the discussion to the PR.
Karl Palmskog (Feb 28 2022 at 19:23):I at least read PMP's answer on the StackExchange as that SR is the basic issue, which in my view makes it boil down to: "nice definitions + SR breakage" or "non-nice definitions + axioms + no SR breakage"
Li-yao (Feb 28 2022 at 19:30):Just as a comment, IIRC Gimenez does not really address the SR problem, instead he moves the goalposts by proving a weaker SR-like theorem (thesis p48 (p60 of the PDF): http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.9849&rep=rep1&type=pdf )
Karl Palmskog (Feb 28 2022 at 19:33):yeah, from what I know Gimenez was aware of the SR breakage, but Ali said the SR breakage itself wasn't the deal breaker.
Paolo Giarrusso (Feb 28 2022 at 19:39):FWIW, "backwards compatibility" is one concern (and a valid one), "negative records are bad" is a different one.
Paolo Giarrusso (Feb 28 2022 at 19:40):And looking from here, I'm not sure why you're blaming negative coinductives when people mix inductives and coinductives without realizing.
Paolo Giarrusso (Feb 28 2022 at 19:43):The traceF-trace decomposition just tells you that the observations on your coinductive type have inductive structure.
Paolo Giarrusso (Feb 28 2022 at 19:44):Having said that, I don't know if negative coinductives are "the right" concept, but they certainly have a claim to that position.
Paolo Giarrusso (Feb 28 2022 at 19:45):The resulting maths looks certainly different; but constructive maths looks unusual to a classical mathematician, and I don't think we'd appreciate if they talked about "garbage" for those definitions.
Karl Palmskog (Feb 28 2022 at 19:57):how exactly are negative types more constructive than positive ones?
Paolo Giarrusso (Feb 28 2022 at 19:58):I didn't say "more constructive", I made an analogy: Some would argue they're "more principled" since they support SR more elegantly — which of course is subjective!
Paolo Giarrusso (Feb 28 2022 at 19:59):Either way, Coq supports both classical logic and definitional proof irrelevance (and nobody plans to drop either), so it could just as well keep supporting positive inductives (either as-is, or with PMP's restriction). If people want SR by default, you could just restrict positive inductives by default.
Paolo Giarrusso (Feb 28 2022 at 20:00):But I'm anyway a pluralist who doesn't see Lean's choices as sinful.
Last updated: Oct 13 2024 at 01:02 UTC