Zulip Chat Archive

Alternatively define an inductive type that includes the extra values (say $-\infty$ and $\infty$ in some algorithmic problems), and derive instances for those.

Kyle Miller (Jun 22 2023 at 15:50):

A version of Option Nat with special notation is WithBot Nat. You can use it, but it seems to be more useful when you expect to actually make use of this additional "bot" value. When you expect to have true Nats, (1) it should be said that you can't expect to know what a Nat expression means unless you know the definitions of the operations, and (2) when there's subtraction, it's on you to do a followup proof that you're not in the truncation regime. It's easy to check here that we are truncating:

example : 12^3 < (10^3 + 9^3) := by decide

Of course, if you're dealing with subtraction you can immediately move to Int with no loss of representation while also being able to do subtraction freely. That's much better than whatever algebraic structure WithBot Nat happens to be.

And yes, there are types with infinities tacked on. For example, docs4#EReal is WithBot (WithTop ℝ), to model the extended real numbers.

Oliver Nash (Jun 22 2023 at 15:54):

IMHO the superiority of the junk value design pattern over partial (or monadic) functions is an empircal observation.

The best justification I have is that junk values allow you to defer the duty of proving the input was good, whereas a partial function requires you to immediately discharge this duty because the obligation exists at the type level (rather than the term level).

Maybe one day some fancy new foundational idea will allow us the benefit of this deferral without having to nominate junk values.

Johan Commelin (Jun 22 2023 at 15:58):

There is of course the chance/hope/wish/dream that proving that the input was good immediately and recording it in the type, will mean that at many other places the obligation can be discharged automatically by unification or other automation.

Riccardo Brasca (Jun 22 2023 at 15:58):

We want to write a ≤ b → b - a + a = b, not a ≤ b → some bizarre stuff with subtypes.

Kyle Miller (Jun 22 2023 at 15:58):

I think the way junk values are handled can be discomforting to those who have a programming background.

On one hand, (functional) programmers like having type systems that can tell them during compilation whether they have programming defects. You never want to construct a junk value (that's a defect), and so they accept having proofs (via type compatibility) that everything is within bounds scattered throughout the program code.
On the other, mathematicians write definitions ("programs") and then prove many things about them separately. There's less of a need to make sure the types in definitions are compatible because, if they weren't, then the expected proofs wouldn't carry through.

Trebor Huang (Jun 22 2023 at 15:59):

Garden variety programmers are more used to junk values I think

Thomas Browning (Jun 22 2023 at 16:02):

There is at least one case where I would consider the junk value to be not actually junk. When doing group theory, many cardinality results are stated with nat.card which uses 0 as a junk value when the type is infinite. But most cardinality results in group theory involve only multiplication and divisibility, in which case 0 is the perfect junk value.

Shreyas Srinivas (Jun 22 2023 at 16:20):

Thomas Browning said:

There is at least one case where I would consider the junk value to be not actually junk. When doing group theory, many cardinality results are stated with nat.card which uses 0 as a junk value when the type is infinite. But most cardinality results in group theory involve only multiplication and divisibility, in which case 0 is the perfect junk value.

I don't have an example right away (I am inside a bus that is hot as an oven), but the issue with picking a junk value for an operation like this is that one might need different junk values for the same type in different circumstances

Shreyas Srinivas (Jun 22 2023 at 16:22):

Also, from a programming perspective it would be awesome if subtypes worked nicely, considering that something like that is often the sales pitch for dependent types.

Kevin Buzzard (Jun 22 2023 at 16:22):

One should never rely on the specific value of a junk value (at least in mathematics) -- the whole point is that mathematicians shouldn't ever be calling those functions with values outside the "mathematical region". Maybe in programming it's different though.

Shreyas Srinivas (Jun 22 2023 at 16:24):

Kevin Buzzard said:

One should never rely on the specific value of a junk value (at least in mathematics) -- the whole point is that mathematicians shouldn't ever be calling those functions with values outside the "mathematical region". Maybe in programming it's different though.

In programming, we eventually want to run programs. So ideally we are forced to prove that we aren't giving functions the wrong values, when we call a function

Martin Dvořák (Jun 22 2023 at 16:26):

However, also in programming, there is a rule "trash in, trash out".

Shreyas Srinivas (Jun 22 2023 at 16:27):

Dependently typed programming is supposed to improve static type checking to help exclude junk values.

Kyle Miller (Jun 22 2023 at 16:37):

@Shreyas Srinivas This is what I was trying to get at when I mentioned how junk values are discomforting to programmers. Said another way, is the person who writes the definition obligated to prove as they go that everything is perfectly compatible? Or is the obligation that you need to write follow-up theorems that the definition behaves exactly as expected?

Dependent types are necessary in both cases. Sometimes though it's easier to write a program/definition with as simple typing as possible and then reserve dependent types for the proof object itself (dependent types are necessary for Lean-as-a-theorem-prover).

Kyle Miller (Jun 22 2023 at 16:41):

@Kevin Buzzard I think this Nat.card = 0 junk value is one that you can actually rely on, since it's mathematically meaningful: given an element g : G of a group G, then you get the exponentiation map Int -> G, and Nat.card of the image of this map is exactly the non-negative generator of the kernel. 0 is the "generic" value for Int after all...

This is just a counter to how you should "never" rely on a specific junk value. On the other hand, perhaps you're right and setting Nat.card to 0 for infinite types isn't junk, but a specification.

Shreyas Srinivas (Jun 22 2023 at 16:58):

Kyle Miller said:

Shreyas Srinivas This is what I was trying to get at when I mentioned how junk values are discomforting to programmers. Said another way, is the person who writes the definition obligated to prove as they go that everything is perfectly compatible? Or is the obligation that you need to write follow-up theorems that the definition behaves exactly as expected?

Dependent types are necessary in both cases. Sometimes though it's easier to write a program/definition with as simple typing as possible and then reserve dependent types for the proof object itself (dependent types are necessary for Lean-as-a-theorem-prover).

Agreed. But it kind of negates the whole promise that dependent types force programmers to prove things. After all, who is checking if the programmer writes the theorems.

I was wondering if we couldn't automate the proof checking for subtypes like liquid types. In lean, since there is no (at least widely known) inbuilt support for refinement types, I would assume this would be written as a meta program (with syntactic sugar) that takes in the program code, and spits a proof obligation as a goal state from which the proof can be completed if it hasn't already been (could they be called semi-liquid types? ;) )

Kyle Miller (Jun 22 2023 at 17:18):

I don't think there's any promise being negated -- these are two ends of a spectrum, and in math-land, where theorems are the point, it seems to be fine to use junk values and avoid dependent types in definitions (and one of the things we try to avoid is "dependent type hell", which is when dependent types make it difficult to prove things).

Dependent types are great and all, but I think what subtypes do in practice is make sure you're maintaining some local invariants -- this can help detect defects, but it does little for the bigger picture. After all, who is checking if a programmer writes a program that matches the specification? :smile:

Patrick Stevens (Jun 22 2023 at 17:40):

Personally I suspect one reason functional programmers find "discharge the obligation up front" so much more natural is because we all grew up with weaker type systems that didn't allow us to save proofs til the end. We have to "parse, not validate" at the very start to get any type safety at all, because our usual type systems don't let us unfold function definitions in our proofs of properties, so if you don't do your proof right away, you've missed your chance.

Shreyas Srinivas (Jun 22 2023 at 18:41):

Patrick Stevens said:

Personally I suspect one reason functional programmers find "discharge the obligation up front" so much more natural is because we all grew up with weaker type systems that didn't allow us to save proofs til the end. We have to "parse, not validate" at the very start to get any type safety at all, because our usual type systems don't let us unfold function definitions in our proofs of properties, so if you don't do your proof right away, you've missed your chance.

Maybe. But I think there is more to it, as I have already mentioned (and Kyle addressed):

Functional programmers want to run the code they write. The role of static type checking is to identify malformed programs before running them. They dont want to just prove that a function is well behaved as long as they dont make a mistake. They want the compiler to scream at them when they try to divide by zero, or violate a bound check on a collection. Even in Lean's Std, a lot of functions on the collection data structures are implemented with two or more alternatives, one of which requires proof obligation, another which has an Option type output, and sometimes a third that panics on bad arguments.
The problem with putting a proof obligation in a separate theorem is, as I said before, the issue that the obligation to write the theorem doesn't exist. This then goes back to point 1.

Johan Commelin (Jun 22 2023 at 20:23):

In mathlib the obligation to write the theorem does exist, because mathlibs existence depends on the existence of theorems that depend on theorems that depend on theorems that are such "spec api coherence lemmas for definitions with junk values".

Shreyas Srinivas (Jun 22 2023 at 20:40):

By obligation, I mean something enforced by a compiler, specifically through compiler errors or warnings.

Shreyas Srinivas (Jun 22 2023 at 20:45):

To clarify, I am not complaining about the approach for math. I am sure that it works very well if proving theorems is the end goal, mathlib being good evidence for that.

Tyler Josephson ⚛️ (Jun 22 2023 at 21:06):

Johan Commelin said:

That's stuff for a new thread. But see https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

We submitted a paper and cited this blog post to explain why Lean defines 1/0=0. A peer reviewer (like us) found this blog post extremely helpful, saying “I was "upset" (in a scientific way) about an undefined derivative being assigned as zero. After the blog post, I had made my peace with it, particularly after the last paragraph. …” They then suggested that we don’t rely on a blog post in the “volatile internet” to make such a critical point in our paper, and that we cite something more permanent. Does anyone have suggestions for papers or other citable works that illustrate the points of this blog post?

Kevin Buzzard (Jun 22 2023 at 21:14):

Anyone is welcome to do anything they like with the information on that blog post: I'll agree to any reuse of it, with or without citation, if that helps

Shreyas Srinivas (Jun 22 2023 at 23:33):

@Tyler Josephson ⚛️ : If they want something "permanent" maybe you could put the blog link in the wayback machine and get the archive link for use as citation URL. As a bonus you also get the date on which it was archived, in case something changes in the future, and people want to know when you the page was in the state you describe in your citation.

Shreyas Srinivas (Jun 22 2023 at 23:35):

(deleted)

Niels Voss (Jun 23 2023 at 00:02):

For programming specifically, there is a divp (notated by /ₚ) which requires you to prove that division is valid before you use it. I think if you are using integers, it also requires you to prove that the dividend is divisible by the divisor. I've never used it, but it might make sense to use a different operator in math and in programming. Something like 3 - 5 = 0 might be arguably worse than division by zero in terms of programming, though I suppose you could use integers instead of natural numbers. However, I do agree with everyone else here that the 1 / 0 = 0 convention makes more sense for mathematics at the present moment.

Eric Wieser (Jun 23 2023 at 01:12):

docs#divp doesn't do anything useful on integers besides division by 1 and -1

Niels Voss (Jun 23 2023 at 04:08):

Oh right it requires the value to have an inverse. Maybe I was thinking of something else in mathlib

Shreyas Srinivas (Jun 23 2023 at 10:05):

I guess what I am looking for is something like Program in Coq : https://coq.inria.fr/refman/addendum/program.html#coq:flag.Program-Mode

Shreyas Srinivas (Jun 23 2023 at 10:21):

In lean, something like the following works :

def incr (x : ℕ) : {y : ℕ // y ≥ 1} := ⟨x + 1,prop⟩
  where
    prop := by
      linarith

unless the where clause is put inside a match arm. Then the goal becomes some metavariable. For example see the goal for proof in

def sub (x : ℕ) (y : {a : ℕ //a ≤ x}) : ℕ :=
  match x with
  | 0 => 0
  | x + 1 =>
      sub x ⟨y.val - 1, proof⟩
      where
        proof := by
              sorry --    .... ⊢ ?m.9036 x y

and of course this leads to an error on proof also. I am guessing that where is always parsed as if it were outside the entire match expression

Shreyas Srinivas (Jun 23 2023 at 10:23):

In Coq's program mode, I get a message that there are so many unfulfilled obligations, then (in a similar fashion to conv here), I can access each obligation and write a proof for it. This is in addition to Coq trying to automatically prove the goals first.

Shreyas Srinivas (Jun 23 2023 at 10:27):

EDIT: Corrected example:
In the second example, using have or let solves the issue a little bit (not metavars), but the somehow the goal is still yval ≤ m + 1

def sub (x : ℕ) (y : {a : ℕ //a ≤ x}) : ℕ :=
  match y.val with
  | 0 => x
  | m + 1 =>
      have proof := by
        cases' y with yval yprop
        simp_all
        done -- Error
      sub m ⟨y.val - 1, proof⟩

Mac Malone (Jul 08 2023 at 04:37):

Shreyas Srinivas said:

Even in Lean's Std, a lot of functions on the collection data structures are implemented with two or more alternatives, one of which requires proof obligation, another which has an Option type output, and sometimes a third that panics on bad arguments.

To me, this suggests that proof obligation, option, and panics are all useful ways to programmatically handle partial functions. In my experience in CS, junk values are often quite useful. Panics (which use junk values) are useful when you want to ignore a particular edge case even if that edge case is not provably avoidable -- some failures are so fatal that handling them is irrelevant because everything else will fail (this is particularly common in impure code). There are also many algorithms which work better with certain junk values e.g. 1/0=0 because that is the special case they want anyway. Similarly, the ability to preserve type homogeneity that junk values provide is sometimes more valuable than special casing(because doing otherwise may e.g. induce large performance costs or complicate the model too severely).

Mac Malone (Jul 08 2023 at 04:39):

An good example of where Nat.sub in particular is useful is for values which deplete but can never go below zero (e.g., resource counters or health counters in video games).

Last updated: Dec 20 2023 at 11:08 UTC