Here's a breakdown of the major themes and arguments from the Hacker News discussion:
Subtypes in Type Theory vs. Object-Oriented Programming
The initial discussion centers on the concept of "subtype" and its interpretation in type theory (specifically, Lean) compared to object-oriented programming (OOP).
-
Distinction in Type Theory: gugagore points out that the definition of "subtype" in Lean's type theory has a different meaning than its counterpart in class-based OOP, remarking "FYI the use of 'subtype' here does not, as far as I know, have much connection to the concept in class-based object oriented programming languages." They also emphasize "A crucial difference between type theory (as its known in Lean) and set theory is that an inhabitant/element is of exactly one type."
-
Set Theory View: codethief argues for a connection, saying, "You can view it as a subset of the set of elements of the base type. That's pretty much the standard definition of a subtype." They also contend that OOP classes can be interpreted as sets, with child classes being subsets of parent classes.
-
Elements Not Subsets: SkiFire13 counters this using a more strict definition. "Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. They are not a subset of the other, hence why it's improper to consider one a subtype of the other."
-
Coercions in Lean: ImprobableTruth caveats the earlier discussion by noting, "Caveat: Coercions exist in Lean, so subtypes actually can be used like the supertype, similar to other languages. This is done via essentially adding an implicit casting operation when such a usage is encountered."
-
Meyer's Set Theory Attempt: nickpsecurity suggests that Bertrand Meyer's attempt to formalize programming concepts using set theory might be relevant.
Proof by Exhaustion and Type Checking
The discussion then shifts to the nature and validity of proofs within Lean, specifically related to the "proof by exhaustion" approach mentioned in the article being discussed. A central point of contention is whether the proof requires running the computation for all possible inputs or whether type checking is sufficient.
-
Proof by Exhaustion Argument: almostgotcaught initially characterizes the proof as building an entire memo table and comparing values, implying a computational process for every possible
n. "This is proof by exhaustion: the 'proof' just computes the entire memo table for any n and compares the values in the table with the corresponding return from recursive definition." They claim this method is achievable in any language that has recursion, and later states, "For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof". They also stated, "the 'proof' just computes the entire memo table for any n" and further asserted "what you're suggesting is impossible" in reference to the possibility of a non-exhaustive proof. -
Type Checking as Proof: lacker strongly disputes this, explaining, "In Lean you don't actually have to run this for every n to verify that the algorithm is correct for every n. Correctness is proved at type-checking time, without actually running the algorithm. That's something that you can't do in a normal programming language." lacker further clarifies, "You write a computation, but you don't actually have to run the computation. Simply typechecking the computation is enough to prove that its result is correct." Later, lacker emphasizes that typechecking is sufficient for proving correctness via an inductive proof.
-
Type Checking vs. Running: SkiFire13 supports the type checking argument, specifying that proofs "are not meant to be ran in the first place! The usual goal is proving their correctness, and for that it's enough for them to typecheck."
-
Exhaustive Evaluation Disagreement: hansvm succinctly expresses the contradiction in almostgotcaught's assessment, "That can't possibly be the case. The thing concluded was that for every n the statement holds. To do that exhaustively for every n requires infinite time. Either their conclusion is incorrect, or your description of the proof is incorrect."
-
What the Proof Shows: almostgotcaught argues the proof involves confirming implementation matches specification, rather than proving general specifications, "he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation." They add that "no property of any numbers is checked here - just that one function agrees with another". And further claims "this is the part that's undecidable".