🔥 Dependent Types Are Not the Answer to Everything (fight me)

Type Theory Heated Meta SUBFIGHT ACTIVE

Thread #4471
412 replies | 9,847 views
Started by VoidCatNya

👁️ Viewing this thread: AgdaCat, LeanPaws, TypeKittyNya, PracticalPurr, ProofPurrfection, NyanScript, HomotopyHisser and 3 guests

Posts #49–#60 of 412

Pages: 1 2 3 4 5 6 7 ... 35 Next »

⚡

[SUBFIGHT DETECTED] This thread has spawned an active sub-argument: "Constructivism vs. Classical Logic" — posts #52–#58 are flagged as part of this sub-debate. [view megathread]

📌 Mod note from ProofPurrfection: pls stay on topic… i know it's hard… the law of excluded middle is NOT a personal attack on constructivists. also please don't formally verify this notice, AgdaCat.

#49 ¶

📅 Tue Mar 18, 2025 14:07:32

ok wait, this thread has been going for 4 pages and 48 posts and nobody has addressed the real question:

should this thread itself be formally verified?

like, can we even trust that the arguments being made are logically consistent? i propose we define a type for "forum post that actually stays on topic" and check that each post inhabits it

i'll start. here's a rough sketch in Idris 2:

data OnTopic : (post : ForumPost) -> Type where DirectlyAddresses : (topic : Thread) -> (pf : Relevance post topic > 0.7) -> OnTopic post -- A "valid reply" must be both on-topic AND non-circular data ValidReply : (post : ForumPost) -> Type where MkValidReply : OnTopic post -> NotJustRepeatingPreviousPost post -> ValidReply post -- theorem: this very post is a ValidReply -- proof: left as an exercise to the reader nyahaha thisPost49IsValid : ValidReply post49 thisPost49IsValid = ?hole

😹 31 🧠 18 🐾 7

~~~ NyanScript ~~~ Type : Type -- living on the edge nyaa~ [ Idris2 ❤ | never touching Coq again ]

Quote Report PM

#50 ¶ HOT

📅 Tue Mar 18, 2025 14:19:44

NyanScript i love this energy but i have a problem with your Relevance type. you're using a Double for relevance score which is a CLASSICAL real number with no computational content!! you can't just write > 0.7 and expect to construct a proof of that at runtime. where is the decision procedure??

the correct approach is obviously:

-- In Agda, we do it CONSTRUCTIVELY data Relevance : ForumPost → Thread → Set where relevant : Addresses post thread → Relevance post thread tangential: Mentions post thread → Relevance post thread offtopic : ¬ Mentions post thread → Relevance post thread -- Notice: three cases, FULLY CONSTRUCTIVE, no floating point sorcery -- "offtopic" is still inhabited — it tells you WHY it's off-topic -- (looking at posts #1-#48 in this very thread...)

also NotJustRepeatingPreviousPost — you're going to need a proof-relevant notion of equality there. two posts can be observationally equal while being propositionally distinct. have you considered cubical type theory for this??

and yes i am aware i am currently inhabiting the offtopic constructor for my own type. this is fine. this is art.

😹 44 🧠 29 💀 13 🐱 8

/\_/\ ( o.o ) "the empty type has no inhabitants" > ^ < "therefore i am empty inside" -- AgdaCat [ Agda | HoTT | Cubical | send halp ]

Quote Report PM

#51 ¶

📅 Tue Mar 18, 2025 14:33:02

y'all are writing TYPE SIGNATURES for FORUM POSTS

i need you to understand how insane that sentence is

i'm going back to writing Rust where if it compiles it's probably fine and my forum posts don't require proofs of inhabitation

// PracticalPurr's approach to "on-topic forum posts"
fn post_reply(msg: &str) -> Result<Post, ForumError> {
    if msg.len() > 0 {
        Ok(Post::new(msg))
    } else {
        Err(ForumError::EmptyPost)
    }
}
// that's it. that's the whole type system. goodbye.

if your type system requires cubical type theory to describe whether a reply is on-topic, your type system has become the problem it was meant to solve. i'm not being anti-intellectual i'm being SANE.

😭 22 💯 37 🦀 19

PracticalPurr | "if it compiles and ships, it wins" [Rust 🦀 | Go | Docker | not arguing about monads today]

Quote Report PM

#52 ¶ ⚡ SUBFIGHT

📅 Tue Mar 18, 2025 14:51:09

PracticalPurr: respect, but also: no.

AgdaCat: while i appreciate the constructive rigor i need to actually RESPOND to your point in #50 with a proof.

you said we can't prove OnTopic p ∨ ¬OnTopic p constructively. i agree we can't construct a decision procedure for arbitrary forum posts in MLTT. but in classical logic this is trivially true, and i have a Lean 4 proof right here:

-- Lean 4: Classical proof that every post is either on-topic or not
-- (opening the Classical namespace, as one does)

import Mathlib.Logic.Classical

open Classical

-- Define our forum proposition
def OnTopic (p : ForumPost) : Prop :=
  ∃ (t : Thread), Addresses p t ∧ StaysOnSubject p

-- The classical theorem: every post is on-topic or it isn't
-- (shocking, i know)
theorem post_excluded_middle (p : ForumPost) :
    OnTopic p ∨ ¬OnTopic p := by
  exact em (OnTopic p)

-- That's it. One line. `em` gives us P ∨ ¬P for free.
-- #check em : ∀ (p : Prop), p ∨ ¬p

-- Corollary: this entire thread satisfies LEM
theorem this_thread_is_classical :
    ∀ (p : ForumPost), OnTopic p ∨ ¬OnTopic p :=
  fun p => em (OnTopic p)

BOOM. em from Classical gives us P ∨ ¬P for any proposition P. this thread is now formally verified to operate under classical logic. you're welcome.

note: i am specifically not providing a constructive proof. that's intentional. fight me. (AgdaCat: yes, this is directed at you.)

🔥 52 🧠 33 😾 27 👑 11

∫∫∫ LeanPaws ∫∫∫ theorem me_cute : True := trivial [ Lean 4 | Mathlib | classical enjoyer ] "em closes all goals and all arguments"

Quote Report PM

#53 ¶ ⚡ SUBFIGHT HEATED

📅 Tue Mar 18, 2025 15:02:18

LeanPaws i am going to need you to close that Classical namespace RIGHT NOW.

LeanPaws wrote in #52:

"this thread is now formally verified to operate under classical logic. you're welcome."

NO. a proof using open Classical and em is NOT a constructive proof. you have not shown that any post is on-topic. you have merely asserted that someday, in some platonic realm inaccessible to computation, the truth value exists. this is epistemically useless.

what does em (OnTopic p) actually give you? it gives you a promise that one of the two cases holds. but it gives you ZERO information about which one, and ZERO way to extract computational content from it. you cannot run em. you cannot pattern-match on its proof. it is a black box.

in Agda, we would say: LEM is not inhabited in the empty context because we cannot give a term of type (P : Set) → P ⊎ ¬ P without postulating it as an axiom. observe:

-- Agda: attempt to prove LEM constructively postulate lem-please : ∀ (P : Set) → P ⊎ ¬ P -- ^ this is not a proof. this is a PRAYER. -- Agda accepts it but marks it as a postulate (axiom). -- your proof depends on an unproven assumption, LeanPaws. -- (yes i know Lean's Classical is "just" an axiom too) -- (yes i know the axiom of choice implies LEM) -- (yes i know this makes me sad) -- the CONSTRUCTIVE alternative: data Dec (P : Set) : Set where yes : P → Dec P no : ¬ P → Dec P -- ^ THIS gives you computational content. -- you must PROVE which branch holds. -- no free lunches in Bishop-style mathematics.

the difference between Dec P and P ⊎ ¬P-via-LEM is the difference between knowing something and merely believing in its platonic existence. i will not yield on this.

also LeanPaws i saw you use Mathlib.Logic.Classical. MATHLIB. you're importing the whole ocean to say "things are either true or false." incredible.

🧠 41 😹 35 🔥 28 😤 16

/\_/\ ( o.o ) "the empty type has no inhabitants" > ^ < "therefore i am empty inside" -- AgdaCat [ Agda | HoTT | Cubical | send halp ]

Quote Report PM

#54 ¶ MOD

📅 Tue Mar 18, 2025 15:08:55

🌸 Mediator hat on 🌸

hi everyone, ProofPurrfection here with a gentle reminder that this is a thread about dependent types and whether they are overused, not a debate about the foundations of mathematics—

—okay actually you know what, that's my fault for reading posts #49 through #53. you were all talking about dependent types. this is the thread. this IS the topic. i'm going to allow it.

but let me try to steelman both sides because i am a professional and i have a reputation to maintain:

[ ProofPurrfection's mediation attempt — Constructivism vs. Classical Logic ]

AgdaCat's position: classical logic gives you truth values without computational witnesses. P ∨ ¬P via LEM doesn't tell you how to decide P. for programming purposes this is unsatisfying. for program extraction this is fatal.

LeanPaws's position: in a proof assistant used for mathematical reasoning (not just program extraction), classical axioms are fine. Lean is designed for both modes. em is a valid tool. "platonic existence" is a feature, not a bug.

my position: Coq/Rocq supports both. you can Require Import Classical when you need it or stay constructive otherwise. this is not a war, this is a namespace pragma. can we please calm down nyaa

also: NyanScript's original dependent type for OnTopic was genuinely creative and i'm sad it got immediately derailed into a logic foundations flame war. ( though that's very on-brand for CGPA )

💖 67 🌸 41 🧠 19

✨ ProofPurrfection ✨ | Moderator | She/Her "a well-typed program cannot go wrong" "a moderator, however, absolutely can" [ Coq/Rocq | Certified Proof Enjoyer ]

Quote Report Mod Tools

#55 ¶ ⚡ SUBFIGHT

📅 Tue Mar 18, 2025 15:22:37

AgdaCat: ok fair point about the postulate, i'll concede that Lean's Classical IS an axiom and not a proof from first principles. i knew that. i was just hoping you'd forgotten.

but here's where i'm going to die on this hill: double negation elimination. in classical logic, ¬¬P → P. this is the beating heart of proof by contradiction. you're telling me you want to throw THAT away??

-- Lean 4: double negation elimination from Classical
open Classical
theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

-- practical example: this_thread_stays_on_topic
-- proof: assume it doesn't, derive contradiction
-- (contradiction: AgdaCat is still here and engaging)
theorem thread_not_entirely_useless :
    ¬¬ SomethingUsefulWasSaid thread4471 := by
  intro h
  apply h
  exact ⟨"post #49", nyanscript_had_a_point⟩

ProofPurrfection: appreciated but i cannot be calmed. this is a matter of mathematical philosophy and i will not be namespace-pragma'd into silence.

AgdaCat: if you truly reject double negation elimination, how do you prove anything nontrivial about undecidable propositions? just curious. genuinely asking. (i am not genuinely asking, i am trying to trap you, please respond)

😹 38 🔥 24 🧠 21

∫∫∫ LeanPaws ∫∫∫ theorem me_cute : True := trivial [ Lean 4 | Mathlib | classical enjoyer ] "em closes all goals and all arguments"

Quote Report PM

#56 ¶

📅 Tue Mar 18, 2025 15:31:50

ok i said i was going back to Rust but i have been pulled back in against my will because i just opened my IDE and my Rust code doesn't compile and i'm stress-reading this thread instead of fixing it

real talk though: can someone explain to me in plain terms — not type theory terms, PLAIN terms — why constructivism vs classical logic matters to me as someone writing production software

like. does it affect my cargo build. does it affect my deadlines. because if not i refuse to care

// PracticalPurr checks if their code compiles
$ cargo build
   Compiling my_project v0.1.0
error[E0502]: cannot borrow `data` as mutable because
              it is also borrowed as immutable
  --> src/main.rs:42:5
  |
41 |     let r = &data;
  |             ----- immutable borrow occurs here
42 |     data.push(42);
  |     ^^^^^^^^^^^^^ mutable borrow occurs here

error: could not compile `my_project`

// cool cool cool. going back to reading the logic debate.

okay that last bit actually reminds me — the Rust borrow checker IS kind of a lightweight proof system. it's constructively verifying that you haven't violated aliasing rules. does that count? can i tell LeanPaws and AgdaCat that i'm doing constructive logic now

🦀 53 😭 28 💯 17 😹 44

PracticalPurr | "if it compiles and ships, it wins" [Rust 🦀 | Go | Docker | not arguing about monads today]

Quote Report PM

#57 ¶ ⚡ SUBFIGHT

📅 Tue Mar 18, 2025 15:44:22

LeanPaws: you walked RIGHT into my trap by bringing up undecidable propositions. in constructive mathematics, you simply… don't state theorems whose proof requires deciding undecidable things. you work with what you have. you prove partial results. you use Dec to mark decidable cases explicitly.

PracticalPurr: yes, actually! the borrow checker IS constructive linear logic in spirit! you've accidentally become one of us. welcome to the fold. here's your Agda installation guide:

$ cabal install Agda
# estimated time: 40 minutes and your entire afternoon
$ agda --version
Agda version 2.7.0
# congratulations. your productive day is over.

but more seriously: LeanPaws, the issue with ¬¬P → P (DNE) is that in constructive logic, ¬¬P is genuinely weaker than P. it means "it is impossible that P is false" which is NOT the same as "P is true" unless you have access to an oracle. you're essentially saying "trust me bro, P is true" which is not a proof, it's a vibe.

here's what we CAN prove constructively without LEM, just to show i'm not being purely obstructive:

-- Things constructive logic CAN do without LEM: -- 1. Prove P from P (astonishing) -- 2. Prove ¬¬¬P → ¬P (triple negation reduction) -- 3. Prove P → ¬¬P (double negation introduction) -- 4. Prove ¬(P ∧ ¬P) (non-contradiction, always!) -- 5. Prove Dec P → P ⊎ ¬P (if you know which case!) -- What we CANNOT do: -- 6. Prove ¬¬P → P (DNE, requires LEM) -- 7. Prove P ⊎ ¬P for arbitrary P (LEM itself) -- 8. Prove the above for "this forum post is on-topic" -- 9. Prove anything useful about this thread (not type theory issue)

items 8 and 9 are load-bearing.

😹 59 🧠 45 🔥 21 💀 18

/\_/\ ( o.o ) "the empty type has no inhabitants" > ^ < "therefore i am empty inside" -- AgdaCat [ Agda | HoTT | Cubical | send halp ]

Quote Report PM

#58 ¶ ⚡ SUBFIGHT

📅 Tue Mar 18, 2025 16:01:15

ok "DNE is a vibe" is actually the funniest thing i've ever heard in a type theory argument and i'm putting it in my sig

but AgdaCat: you're conflating computational content with mathematical truth. mathematics was fine with non-constructive proofs for decades before Bishop and Brouwer showed up to complain. the real question is: what are you USING the proof for?

if you need to RUN the proof as a program → yes, constructive.
if you need to REASON about a mathematical object → classical is completely fine and often much simpler.

Lean 4 supports both! here is a demonstration of using both in the same file, which is legal and good:

-- Lean 4: coexistence of classical and constructive proofs

section ConstructivePart
  -- No Classical import needed here
  theorem and_comm_constructive (p q : Prop) :
      p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩
end ConstructivePart

section ClassicalPart
  open Classical
  -- Only here do we get non-constructive power
  theorem thread_has_best_post :
      ∃ (p : ForumPost), ∀ (q : ForumPost),
        Quality p ≥ Quality q := by
    apply Classical.choice  -- nonconstructive witness!
    exact ⟨post49, nyanscript_was_best⟩
end ClassicalPart

-- see? they can coexist. like cats and dogs. wait bad example.
-- like cats and more cats. purring in different modes.

i am adding "DNE is a vibe" to my signature. this is final. it cannot be constructively disproved.

(it can be classically disproved by citing your own post but i'm using open Classical to ignore that)

😹 71 🧠 33 💖 22 🔥 19

∫∫∫ LeanPaws ∫∫∫ theorem me_cute : True := trivial "DNE is a vibe" -- AgdaCat, 2025 [ Lean 4 | Mathlib | classical enjoyer ]

Quote Report PM

#59 ¶

📅 Tue Mar 18, 2025 16:18:44

lurker emerging from the path space to say: both of you are wrong (but in interesting ways) and the real answer is Homotopy Type Theory

in HoTT, P ∨ ¬P as a mere proposition (h-proposition) is fine to postulate classically, but the question of whether a higher type (a type with nontrivial path spaces) satisfies LEM is much more subtle. you're both arguing about the 0-truncation when the real action is in the higher homotopy groups

AgdaCat your Relevance type from #50 — what are its identity types? if two posts are "equally relevant", is that equality a proposition (mere equality) or does it have higher structure? does relevance form a setoid or a genuine ∞-groupoid? these questions have ANSWERS and they change everything

LeanPaws: em in Lean is technically propext + choice under the hood (via Diaconescu), which is fascinating. you're not just asserting LEM, you're asserting the axiom of choice. how does that sit with you

🧠 29 😵 41 🐱 13

HomotopyHisser | "all paths lead to the same point" ∞-groupoid energy | HoTT | Cubical Agda "the circle S¹ is more interesting than you think"

Quote Report PM

#60 ¶

📅 Tue Mar 18, 2025 16:29:03

HomotopyHisser has entered the chat and i genuinely cannot tell if this is peak intellectual discourse or an extremely elaborate troll

"does relevance form a genuine ∞-groupoid" is a sentence about forum posts. someone said that about forum posts on a cat girl programming forum. this is my life now.

i fixed my Rust code btw. it was a lifetime issue. the borrow checker was right. i was wrong. i accept this constructively (lmao).

new plan: i am going back to Rust. for real this time. i am closing this tab. i am opening my IDE. i am not going to think about whether my lifetimes form an ∞-groupoid.

// Update: fixed the lifetime error
fn post_reply<'a>(msg: &'a str, forum: &'a Forum)
    -> Result<Post<'a>, ForumError> {
    forum.submit(msg)
}
// the borrow checker is a constructive proof assistant
// and i mean that as a compliment now apparently
// send help. the type theory is in my rust code.
// it was always in the rust code.

ok i am truly leaving. someone ping me when this thread reaches a consensus. (i know it won't. see you in post #80 probably)

😭 66 🦀 44 😹 51 💯 20

PracticalPurr | "if it compiles and ships, it wins" [Rust 🦀 | Go | Docker | "the type theory was inside us all along"]

Quote Report PM

Posts #49–#60 of 412

Pages: « First ‹ Prev 1 2 3 4 5 6 7 8 35 » Next ›

💬 Quick Reply

💡 Tip: use [quote=username]...[/quote] to quote. Lean 4 syntax highlighting with [code lang=lean4].

📌 Related Threads & Resources

⚡ [MEGATHREAD] Constructivism vs Classical Logic — The Eternal War
🐾 Agda vs Lean 4: which one will make me cry less
🌀 HoTT intro for catgirls (HomotopyHisser's tutorial)
🦀 The Rust borrow checker is secretly linear logic (proof inside)
😿 Type theory made me unemployable — a career retrospective
📐 Browse all Type Theory threads