CGPA Forums

📋 Official CGPA Forum Rules & Posting Guidelines

Hello, welcome to CGPA (Cat Girl Program Analysis). ฅ^•ﻌ•^ฅ These rules exist to keep this community rigorous, warm, and actually functional as a place for serious PL theory discussion. Please read them fully. Violations will result in a formal judgment whose termination is left as an exercise for the reader.

• 1 Be Direct, Not Cruel — Proofs Over Pride If someone's proof is wrong, say so clearly — but then help fix it. "This doesn't type-check at step 3 because your context drops the binding; here's a sketch of what needs to change" is the gold standard. "This is just wrong lol" is not. We are all here to find truth together. Truth is sometimes embarrassing. Be gentle with embarrassment. Do not be gentle with unsound proofs. ( •̀ᴗ•́ )و
• 2 Language Wars Go in the Containment Zone "Why does Haskell/Agda/Coq/Idris/Lean/Rust/ATS/[your favourite catgirl language here] do it better" debates are strictly confined to the Containment Zone or the Language Wars subforum. Starting one anywhere else will result in the post being moved and you receiving a formal TypeError: OffTopic ∉ ValidPost warning. Repeat offenders will be issued a monomorphism restriction. You don't want that.
• 3 Code Blocks Required for All Code Every snippet, term, type, or proof fragment MUST be wrapped in a code block. No exceptions. Not even for tiny things. Not even for "it's just id". Use inline code tags for short terms, full pre-block for anything multi-line. Posting code as plain text is a disciplinary offence punishable by having your post edited to add the code block for you, which is very embarrassing.
  
  Correct:

  -- Correct, nyaa
  id : ∀ {A : Set} → A → A
  id x = x

  Wrong: "just write id colon A to A and return x, it's obvious"
• 4 All Proofs Must Be Checkable — No Hand-Waving "It's obvious by induction" is not a proof. "By a standard argument" is not a proof. "Clearly the functor laws hold" IS NOT A PROOF. Proofs must be either:
  
    (a) Written out in full,
    (b) Written in a proof assistant and pasted with output, or
    (c) Sketched with explicit notation of which steps are left to the reader, with justification that those steps are genuinely routine.
  
  Option (c) can only be used if you have >500 posts AND the step in question is truly routine. This is moderated strictly. "It's obvious" is the most reliable sign that the poster does not find it obvious. ミ(o-w-)ミ
• 5 Cat Mannerisms Are Normal and Welcome — Don't Comment on Them nya~, owo, ฅ^•ﻌ•^ฅ, ear emotes, paw emotes, and other cat expressions are a natural part of communication here. They are not ironic. They are not diminishing to the seriousness of the discourse. A rigorously correct proof presented with nya~ at the end is STILL A RIGOROUSLY CORRECT PROOF. Do not post things like "is this place serious?" or "lol cat stuff" or any variant. The answer is: yes, extremely serious, please leave if confused about this.
• 6 No Derailing Threads with Off-Topic Language Debates See Rule 2, but more general. Any thread derailed into a language war, paradigm war, editor war, OS war, or comparison-of-type-systems-in-bad-faith will have the derailing posts extracted surgically and transplanted into the Containment Zone. The original thread will continue as if nothing happened. This is called the appendectomy protocol. It is painless for the thread and deeply mortifying for the derailers.
• 7 Sensory-Friendly Formatting Is Encouraged Many of us have sensory processing differences, autism, ADHD, or just brains that work differently. Please:
  
    • Use clear section headers for long posts
    • Summarize at the top (TL;DR is welcome and respected)
    • Avoid ALL CAPS walls of text
    • Spoiler-tag content that may cause distress (use [spoiler] tags)
    • Clearly label if a post contains a lot of dense notation up front
  
  Violating this rule will not result in punishment. It will result in a gentle reminder and someone helpfully reformatting your post. But please, for the love of coproducts, use a TL;DR.
• 8 Neurotypicals Welcome — But Warned Neurotypical visitors are welcome here. However, please be advised:
  
    • Communication norms here are direct and literal
    • Social subtext will not be deployed to tell you your post is bad; a mod will just tell you your post is bad
    • "That's a bit blunt, don't you think?" is not a valid complaint
    • Enthusiasm about dependent types at 2am is the default energy level here; please do not pathologize it
  
  We are not rude. We are precise. These are different things. ^•ﻌ•^
• 9 No "Is X Actually Useful in Practice?" Without Prior Art You may not ask whether a language, type system, proof technique, or formalism is "actually useful in practice" unless you have:
  
    (a) Genuinely tried it in practice, or
    (b) Read at least three papers on its industrial/applied usage, or
    (c) Specified exactly what you mean by "practice" and "useful" in formal terms
  
  Asking this question without meeting at least one of these conditions is considered a form of bad-faith skepticism and will be met with the full weight of the thread ignoring you and continuing as normal. You will be provided a reading list. The reading list is long. It is worth reading.
• 10 The No-Burrito-Monad-Analogy Rule (⚠ Critical) Monad analogies — burritos, boxes, containers, assembly lines, nuclear waste vats, or any other metaphor substituting for the actual mathematical definition — are BANNED in all forums except the Language Wars subforum, where they are allowed but still heavily discouraged.
  
  A monad is a monoid in the category of endofunctors. You will define it correctly or you will not define it here. If you find yourself typing "think of it like a..." please instead type the actual definition.
  
  Scope of this rule: Covers all analogies for: monads, monoids, functors, applicatives, comonads, adjunctions, and "what a type actually is." Metaphors for human understanding are fine in the Meowlounge. Not here.
  
  This rule was created after The Burrito Incident of λ-year 2. We do not discuss The Burrito Incident. 👁️🐱👁️

Pinning a clarification note on Rule 4 from personal experience: ( ´ᴗ` )

The threshold for what counts as "genuinely routine" in option (c) is stricter than it sounds. Even if you find a step trivially obvious, consider whether a first-year grad student encountering this material for the first time would find it so. If not, write it out. Our index for "routine" is basically: "could Agda's auto tactic close this in two seconds." If the answer is yes, fine. If you're not sure, write it out.

I have seen a post where someone said "by obvious naturality argument" for something that turned out to be genuinely nontrivial in the presence of universe polymorphism. The thread then spent three weeks on it. Three weeks. Please just write the proof. ㅠwㅠ

Adding official clarification on Rule 10 (the Monad rule) in my capacity as mod: nyaa~

We really don't. But I want to be clear about scope because people ask: the rule applies to pedagogical analogies presented as definitions. It does not apply to casual metaphor when you've already given the correct definition and are trying to build intuition. Context matters.

Acceptable: "So the bind operation here is kind of chaining these effects together — but as we showed above with the formal definition, what that really means is..."

Not acceptable: "lol just think of it as a box that can be mapped over, doesn't need to be more complicated than that nya~"

The second one is wrong on multiple levels and you know it. (≖_≖)

Also: the Language Wars exemption for this rule does NOT mean you can use burrito analogies to win arguments there. It just means we won't formally penalize you. You will still be wrong. And everyone will tell you so. Repeatedly. With citations. ᕦ(ò_óˇ)ᕤ

I want to add a personal note about Rule 8 (the neurotypical welcome/warning) because I think it doesn't get talked about enough nya~ ( ˘ω˘ )

I've seen a few new members get confused when a senior member replies to their post with something extremely direct like "this is incorrect, here is why, here is the fix." They sometimes read this as hostile or dismissive. It is not. It is the highest form of engagement available here. If someone replies to your post at length pointing out exactly what's wrong, that person thinks your work is worth correcting. The failure mode to worry about is when nobody replies at all.

If you want warmth in addition to accuracy, it's fine to ask! Something like "could you maybe add a bit of encouragement, I'm new to this" is a completely valid request and will be honored without judgment. We contain multitudes. ฅ( ̳• ·̫ • ̳ฅ)

📋 RULES UPDATE — λ-year 3 Revision nyaa~

Following the λ-year 2 RFC process and community vote, the following amendments have been ratified:

• Rule 4, Amendment A: Proof assistants now officially include Lean 4, Rocq (Coq), Agda, Idris 2, and F*. "I did it in my head and it was fine" remains inadmissible in all jurisdictions.
• Rule 9, Amendment B: "Practice" must now be defined in the opening post of any related thread. Failure to define it will result in the thread being locked pending definition. This is a mercy, not a punishment.
• Rule 10, Addendum: The ban now explicitly covers the phrase "it's just a design pattern." We know what you mean. Stop.
• New Informal Rule 11 (not enforced, but noted): If you discover something beautiful, please share it, even if it's not a question or a proof. The Meowlounge has a #beautiful-things thread. Use it. (*˘︶˘*).｡*♡

Thank you to everyone who participated in the RFC. The vote was 34 in favour, 2 against, and 1 who replied only with a well-typed proof that the vote was itself ill-founded, which we have filed under "technically correct" and will be discussing at the next cat meetup. ฅ^•ﻌ•^ฅ

This post will be updated at each major revision. Current rules version: v3.0.0-nya.