12 ms·

Division by zero in type theory: a FAQ

120 points by EvgeniyZh 6y ago

e79 6y ago
I think this behavior makes perfect sense when you view it through the lens of type theory. Functions that return a real number must always return a real number. Some function types are defined by something like ‘R, error’, and then it’s up to the caller to check ‘error’. Others throw exceptions that bubble up the call stack and may never return ‘R’, which in a sense breaks the type contract and has “exception” theory preceding type theory.
- kevinbuzzard 6y ago
  (disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.
  - e79 6y ago
    What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
    - thaumasiotes 6y ago
      Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
      - zozbot234 6y ago
        That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
        thaumasiotes 6y ago
        ...yes?
  - garmaine 6y ago
    Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.
    - Tainnor 6y ago
      Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
      - garmaine 6y ago
        There's a couple of points to be made to that. First, we should be extending our hardware numerics to support the extended real number line, inclusive of infinity, in a way which causes a lot of these exceptions to disappear. Division by zero should result in an inf, not an exception or NaN. Second, those exceptions which can't be eliminated DO need to be handled anyway. To say "but then we'd have to handle a bunch of exceptional cases everywhere!" is exactly the point. They do need to be handled. Finally, language and compiler improvements can make handling exceptional cases easier. E.g. let numerical methods specify domain and range requirements and have these be compiler-enforced. Then the implementation is freed from handling exceptional conditions that only arise with inputs outside of its declared domain.
        Tainnor 6y ago
        I feel you're missing the point: - Division by zero resulting in Inf could be fine in some cases, but might also lead to issue in other situations. The "calculate a slope through two separate points" is a good example: the slope through a single point is either undefined or the derivative, but it's not infinity. In any case, division by zero is sufficiently "weird" or "corner case-y" that you'd want to pay special attention to it. And if the runtime blows up in your face and tells you something is wrong, that can in many cases be better than to continue with wrong values (compile-time checks are always better, but not always feasible). - First, it's not true that all exceptions need to be handled. This heavily dependens on the use case. If you're an app developer, then the app crashing might be a better (!) alternative than e.g. corrupting data, if it happens rare enough. After all, the user can just restart the app. Even if you write a server side app, you may get away with crashing, as long as you have a supervisor or so restarting unhealthy processes/instances. I'm not saying, crashes are good behaviour, but im some cases they are better behaviour than some of the alternatives (and in any case, no code is ever crash-proof, you can always have OOM, stack overflow, etc.). This is the concept of fault tolerance: you might not know which bugs happen, but you want to be able to recover from them somehow. In fact, if I'm not mistaken, Erlang basically takes this philosophy to an extreme. - Even if you handle exceptions, you don't necessarily want to handle them locally. This is why many languages have unchecked exceptions. You're free to declutter a huge chunk of your application of error handling that would be extremely tedious, and just handle the (rare) exception at the top-level, or whatever intermediate layer best knows how to deal with it. Sometimes you just want to assert something about the state of your program that the compiler doesn't know and throwing an unchecked exception in case the condition is violated and only handling it at the topmost layer of your application is a perfectly reasonable decision.
  - enriquto 6y ago
    > if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f). On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.
- contravariant 6y ago
  Well, if you ask the mathematicians then f(x) = 1/x isn't defined on the real numbers, it's defined on the non-zero real numbers. It always returns a real number but it's domain has a different type. This places the burden on the person using the function to prove that x isn't 0, but that's the price you have to pay to have a proper multiplicative inverse.
  - ragnese 6y ago
    f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. But, I don't think what you said is quite right, either. If you define f(x) = 1/x over the non-zero reals, then the range does have the same type as the domain- you can't get zero out of the function, so the range is also the non-zero reals.
    - ogogmad 6y ago
      The codomain doesn't have to equal the image. The image is the non-zero reals, but the codomain could be any superset of it (including all of R). The word "range" is ambiguous.
      - ragnese 6y ago
        Thank you. I've forgotten some of the terminology, since I haven't thought about real math in a few years. :(
    - contravariant 6y ago
      There's no real problem with defining the codomain to be too big. Although you can indeed also pick the non-zero reals as the co-domain.
    - thaumasiotes 6y ago
      > f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. Not quite. The extended reals are ℝ + {inf, -inf}. This has the problem that 1/x approaches inf from the right and -inf from the left. As ogogmad notes, in order to define a value for 1/x at 0, you need the projectively extended reals.
- jhanschoo 6y ago
  I don't understand what you mean. You still have the different obvious ways of formulating, e.g. division in type theory: 1. The article's way: "R^2->R", but garbage value for 0 in the second argument. 2. What you propose: "R^2->Maybe R" 3. The mathematician's dependent-type-theoretic way "R * (x:R, proof that x!=0) -> R", 4. the conventional way "R * (R\{0}) -> R". They have their advantages and disadvantages. The first is useful in proof verification since it simplifies most proofs, from which perspective this garbage value of 0 is actually well-behaved, and doesn't need to be handled as a special case. But you allow seemingly nonsense theorems when you forget to condition (x>0). What you propose is similar, except that you are forced to reason about whether the output value is valid. 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 4 is more tedious since you have merely shifted the problem of handling the zero case into proving properties about the canonical embedding "R->R\{0}" (which must still have a garbage value for 0). On the upside, these functions surject into R.
  - SquishyPanda23 6y ago
    > 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.
    - jhanschoo 6y ago
      As the article mentions, it doesn't necessarily work this way in a verified proof. Every time you form an expression involving division, you have to supply the proof. It is this repeated supplying of a proof (not necessarily having to reprove it) that is omitted in regular informal proofs that is tedious. In certain situations you can write automation to help you with that. But more frequently, you already have automation for other aspects of your proof, and this need to prove this is tripping up your other automation.
  - e79 6y ago
    I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.
- dependenttypes 6y ago
  What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 = 0 makes sense in type theory is that you can simply define types such as (n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n as in you do not need to make your laws hold true for every possible input of / which is why it does not break regular mathematics.
lmm 6y ago
This sounds like the idea that it's fine for C++ templates to not be typechecked, because the expanded template will eventually be checked by the compiler. Perhaps, but it makes for errors a long way away from their causes, which are difficult to debug. If I ever divide by zero (or by something that might be zero) in my proof, I've almost certainly made a mistake. I'd rather hear about it straight away than later when I try to use some fact about the result of that division.
- MaxBarraclough 6y ago
  For completeness: C++ eventually introduced a feature to allow something analogous to type-checking for template metaprogramming, called concepts - https://en.wikipedia.org/wiki/Concepts_(C%2B%2B) https://en.wikipedia.org/wiki/Concepts_(C%2B%2B)
- nybble41 6y ago
  > … it makes for errors a long way away from their causes, which are difficult to debug. It also means that any type errors that don't affect the expanded template (but may still have an effect on semantics) will not be caught at all.
somewhereoutth 6y ago
Using Scott encoding in the Lambda Calculus it is actually possible to define a 'usable' infinite natural number as a recursive construction (essentially its predecessor is defined as itself). Interestingly enough, constructions for add, (natural) subtract and multiply work as you would expect with this infinite number without needing special handling. E.g. for all n, n + inf == inf, n - inf == 0, n * inf == inf. Furthermore, the construction for (natural) div yields this infinite term (or at least something that behaves exactly like it) when the denominator is 0. Even more interestingly, 0/0 == inf for this system. EDIT: Why might this be useful? Well now when you 'take n' from a list, n=inf will give you the whole list, regardless of how long (or even if it is infinite - i.e. lazy). Likewise 'drop n' will return the empty list - except with an infinite list, whereupon the calculation will fail to terminate. EDIT: inf - inf == non-termination in this system, suggesting that not only inf - inf != 0, but it != inf either, and in fact it is something unreachable (in this system) (note the correspondence between 'subtract' and 'drop').
- zodiac 6y ago
  Mathlib does indeed define the extended real numbers, but they also need to define division on the reals. This is similar to the definition of subtraction having to be done for integers and for naturals (mentioned in the article)
  - somewhereoutth 6y ago
    I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity. What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals). The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator): zero := \f \x n succ := \n \f \x f n infinite := \n succ (infinite n) infinity := infinite zero subn := \n \m m (\p n (\q subn q p) n) n divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m)) divn (succ zero) zero => infinity EDIT: Note that infinity does not have a normal form (does not terminate), but: subn n infinity => zero
Tainnor 6y ago
I ran into this argument before. I can understand that it makes sense for proof assistants. As the post shows, proof assistants don't allow you to misuse that anywhere else. (But as a sidenote: couldn't you fix this with dependent types somehow?) I still think it would be wrong for a regular programming language. Afaik, the Pony language does this too, but that is a general-purpose programming language that does not check your logic, and I am very wary of something like that. People might type up some algorithms, or even just try to compute an average, and the system absolutely should yell at you if you try to divide by zero.
- 1-more 6y ago
  Elm does this for integers (Floats support Infinity, natch) and I support it. Elm is meant for writing declarative UIs, and the only example I could think of for blindly dividing by 0 is taking the average of an empty list without checking first. But any time you might do that, you'd be better served by matching on the empty list _before_ trying to take the average and rendering something helpful for the user.
- ogogmad 6y ago
  > (But as a sidenote: couldn't you fix this with dependent types somehow?) Most proof assistants, including Lean, are built on dependent type theory.
  - Tainnor 6y ago
    Sure but then I guess maybe you can find ergonomic improvements to your dependent type system so as not to run into the problems discussed in the article (e.g. having to reprove that something is not zero over and over again).
    - OscarCunningham 6y ago
      Maybe the way to do that would be to prove once that x is nonzero, use that to define r = 1/x, and thereafter use multiplication by r?
- 6y ago
Someone 6y ago
I don’t think the “in type theory” restriction is correct. This choice works fine when using type theory in theorem provers, but would be unacceptable if we did it in programming languages that use type theory (or would that be called “type practice” ;-)?) In Haskell, for example, 1/0 returns Infinity.
- Sniffnoy 6y ago
  That's not exactly right... in Haskell, 1/0 has type Fractional a => a. So, it could be any fractional type. If 1/0 occurs in a context where it'll be interpreted as a floating-point number, you'll get Infinity, yes, as per how standard floating-point works. In other contexts though you may get an error. E.g., if you import Data.Ratio and do 1/0 :: Rational, you'll get an error.
- dddbbb 6y ago
  The type signature of division in Haskell merely requires that it takes two fractional `a`s and returns another `a`. 1 / 0 :: Double evaluates to Infinity. 1 / 0 :: Rational throws a runtime exception. A division by zero producing zero would be perfectly sensible in Haskell, and perhaps even desired if you are totally averse to runtime errors. The Pony language infamously does this.
- curryhoward 6y ago
  In academia, "type theory" almost always means dependent type theory, such as Martin-Löf type theory or homotopy type theory. Type theory is used in most theorem provers as a foundation for mathematics. The title of this blog post is using the term in a standard way. Programming languages such as Haskell and Java are not based on type theory. They have type systems. Haskell's type system is much closer to type theory than that of Java, but it's still quite crippled compared to what type theorists study. It is of course possible to define things in type theory such that 1/0 = Infinity or something else, but that is not the norm.
dvt 6y ago
The title is a bit sneaky. Division by zero in "type theory" will depend on just that -- your type theory. Some theories use special values for division by zero (e.g. could spit out DNE or +INF/-INF). But then you need to formalize how you do "things" with DNE or infinities. This is, more often than not, an unnecessary rabbit hole, so just returning 0 is simpler. Some theories might require a proof that the denominator isn't zero (essentially making division a three-argument function) -- which is kind of a cool way of thinking about it[1]. [1] https://math.stackexchange.com/questions/334393/how-does-type-theory-handle-division-by-zero-and-such https://math.stackexchange.com/questions/334393/how-does-typ...
nshepperd 6y ago
This strikes me as having some interesting similarity to the practice in Haskell of placing type class constraints on functions, not data types. A deprecated feature of Haskell used to allow you to write data types like: data Ord k => Map k v = ... This defined a data type representing an ordered map from k to v, with the additional restriction that before you can talk about such a map you had to know that the type k is orderable (has an instance of the Ord type class which defines comparison operators). This may be considered to be similar to the definition of (/) requiring that its second argument is nonzero. This style was supplanted by leaving the data type definition 'bare' and placing the constraints on the API's functions instead: data Map k v = ... insert :: Ord k => k -> v -> Map k v -> Map k v lookup :: Ord k => k -> Map k v -> Maybe v This style is similar to instead placing the nonzero-ness constraint on the theorems which define the API of (/). In both cases there are basic engineering reasons for the switch: - Having the constraints in the definition of terminology (Map, /) doesn't save any work, as you still need to prove those constraints to do anything or refer to it (in Haskell this meant sprinkling `Ord k =>` in the type of anything that referred to Map k v). - In fact it results in doing more work than necessary, as you are sometimes forced to prove the constraints just to mention Map, even when what you are doing does not require them. For instance defining the empty map 'empty :: Map k v' shouldn't require you to know anything about k, because an empty tree doesn't contain any keys, let alone care about their ordering. In this case requiring Ord k in order to mention Map k v would be superfluous.
- Ar-Curunir 6y ago
  Rust tends to take the second approach as well; it tends to place trait bounds on `impl` blocks, and not on the struct itself. (This is by no means a standard across the community though; I'd say it's a 50/50 split)
  - wh33zle 6y ago
    A case where it is unavoidable is when you want to refer to an associated type in your struct declaration. In most other cases, putting bounds on impls leads to less repetition of those bounds and better error messages! Another related topic is trait methods with method-level type parameters that have bounds. Those have to be repeated on every usage site so it is usually preferable to go for a design that has the type parameters in the actual trait. Instead of: trait Foo { fn foo<T: Bar>(&self, bar: T) } do this instead: trait Foo<T> { fn foo(&self, t: T) } impl<T: Bar> Foo for XYZ { fn foo(&self, bar: T) { } } One bound might seem fine in this example but once stuff needs to be Send, Sync and 'static is when it gets annoying.
dwheeler 6y ago
Obviously a system can define a symbol like "/" as whatever it wants to. But then it isn't what many mathematicians would expect. The Metamath Proof Explorer defines "/" so it only has a value if the denominator is a nonzero complex number: http://us.metamath.org/mpeuni/df-div.html http://us.metamath.org/mpeuni/df-div.html You can argue if that is better, but that is a possible choice.
credit_guy 6y ago
With humility I will say that I don't like this solution. In mathematics functions have domains and codomains. Two functions are equal if their domains are equal, their codomains are equal, and for all the values in the domain they return the same values in the codomain. A mathematician who doesn't know anything about type theory, but hears Lean is good at formalizing math, will expect the division function to have the domain R x (R\{0}). Modifying the domain to be R x R and returning a garbage value for the added points is not a good solution. Maybe it works "in real life", but you always need to carry with you an invisible asterisk and footnote that Lean did the right thing only assuming you asked the right question. Again, being humble (my Lean experience is about one hour in total, spread across several sessions), I think it would be better to invest a bit more time upfront and always define properly the domain of the function used, rather than introduce edge cases that can bite you in the back twenty five theorems down the road.

120 points by EvgeniyZh 6y ago

e79 6y ago

I think this behavior makes perfect sense when you view it through the lens of type theory. Functions that return a real number must always return a real number. Some function types are defined by something like ‘R, error’, and then it’s up to the caller to check ‘error’. Others throw exceptions that bubble up the call stack and may never return ‘R’, which in a sense breaks the type contract and has “exception” theory preceding type theory.

kevinbuzzard 6y ago
(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.
- e79 6y ago
  What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
  - thaumasiotes 6y ago
    Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
    - zozbot234 6y ago
      That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
      - thaumasiotes 6y ago
        ...yes?
- garmaine 6y ago
  Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.
  - Tainnor 6y ago
    Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
    - garmaine 6y ago
      There's a couple of points to be made to that. First, we should be extending our hardware numerics to support the extended real number line, inclusive of infinity, in a way which causes a lot of these exceptions to disappear. Division by zero should result in an inf, not an exception or NaN. Second, those exceptions which can't be eliminated DO need to be handled anyway. To say "but then we'd have to handle a bunch of exceptional cases everywhere!" is exactly the point. They do need to be handled. Finally, language and compiler improvements can make handling exceptional cases easier. E.g. let numerical methods specify domain and range requirements and have these be compiler-enforced. Then the implementation is freed from handling exceptional conditions that only arise with inputs outside of its declared domain.
      - Tainnor 6y ago
        I feel you're missing the point: - Division by zero resulting in Inf could be fine in some cases, but might also lead to issue in other situations. The "calculate a slope through two separate points" is a good example: the slope through a single point is either undefined or the derivative, but it's not infinity. In any case, division by zero is sufficiently "weird" or "corner case-y" that you'd want to pay special attention to it. And if the runtime blows up in your face and tells you something is wrong, that can in many cases be better than to continue with wrong values (compile-time checks are always better, but not always feasible). - First, it's not true that all exceptions need to be handled. This heavily dependens on the use case. If you're an app developer, then the app crashing might be a better (!) alternative than e.g. corrupting data, if it happens rare enough. After all, the user can just restart the app. Even if you write a server side app, you may get away with crashing, as long as you have a supervisor or so restarting unhealthy processes/instances. I'm not saying, crashes are good behaviour, but im some cases they are better behaviour than some of the alternatives (and in any case, no code is ever crash-proof, you can always have OOM, stack overflow, etc.). This is the concept of fault tolerance: you might not know which bugs happen, but you want to be able to recover from them somehow. In fact, if I'm not mistaken, Erlang basically takes this philosophy to an extreme. - Even if you handle exceptions, you don't necessarily want to handle them locally. This is why many languages have unchecked exceptions. You're free to declutter a huge chunk of your application of error handling that would be extremely tedious, and just handle the (rare) exception at the top-level, or whatever intermediate layer best knows how to deal with it. Sometimes you just want to assert something about the state of your program that the compiler doesn't know and throwing an unchecked exception in case the condition is violated and only handling it at the topmost layer of your application is a perfectly reasonable decision.
- enriquto 6y ago
  > if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f). On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.
contravariant 6y ago
Well, if you ask the mathematicians then f(x) = 1/x isn't defined on the real numbers, it's defined on the non-zero real numbers. It always returns a real number but it's domain has a different type. This places the burden on the person using the function to prove that x isn't 0, but that's the price you have to pay to have a proper multiplicative inverse.
- ragnese 6y ago
  f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. But, I don't think what you said is quite right, either. If you define f(x) = 1/x over the non-zero reals, then the range does have the same type as the domain- you can't get zero out of the function, so the range is also the non-zero reals.
  - ogogmad 6y ago
    The codomain doesn't have to equal the image. The image is the non-zero reals, but the codomain could be any superset of it (including all of R). The word "range" is ambiguous.
    - ragnese 6y ago
      Thank you. I've forgotten some of the terminology, since I haven't thought about real math in a few years. :(
  - contravariant 6y ago
    There's no real problem with defining the codomain to be too big. Although you can indeed also pick the non-zero reals as the co-domain.
  - thaumasiotes 6y ago
    > f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. Not quite. The extended reals are ℝ + {inf, -inf}. This has the problem that 1/x approaches inf from the right and -inf from the left. As ogogmad notes, in order to define a value for 1/x at 0, you need the projectively extended reals.
jhanschoo 6y ago
I don't understand what you mean. You still have the different obvious ways of formulating, e.g. division in type theory: 1. The article's way: "R^2->R", but garbage value for 0 in the second argument. 2. What you propose: "R^2->Maybe R" 3. The mathematician's dependent-type-theoretic way "R * (x:R, proof that x!=0) -> R", 4. the conventional way "R * (R\{0}) -> R". They have their advantages and disadvantages. The first is useful in proof verification since it simplifies most proofs, from which perspective this garbage value of 0 is actually well-behaved, and doesn't need to be handled as a special case. But you allow seemingly nonsense theorems when you forget to condition (x>0). What you propose is similar, except that you are forced to reason about whether the output value is valid. 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 4 is more tedious since you have merely shifted the problem of handling the zero case into proving properties about the canonical embedding "R->R\{0}" (which must still have a garbage value for 0). On the upside, these functions surject into R.
- SquishyPanda23 6y ago
  > 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.
  - jhanschoo 6y ago
    As the article mentions, it doesn't necessarily work this way in a verified proof. Every time you form an expression involving division, you have to supply the proof. It is this repeated supplying of a proof (not necessarily having to reprove it) that is omitted in regular informal proofs that is tedious. In certain situations you can write automation to help you with that. But more frequently, you already have automation for other aspects of your proof, and this need to prove this is tripping up your other automation.
- e79 6y ago
  I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.
dependenttypes 6y ago
What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 = 0 makes sense in type theory is that you can simply define types such as (n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n as in you do not need to make your laws hold true for every possible input of / which is why it does not break regular mathematics.

lmm 6y ago

This sounds like the idea that it's fine for C++ templates to not be typechecked, because the expanded template will eventually be checked by the compiler. Perhaps, but it makes for errors a long way away from their causes, which are difficult to debug. If I ever divide by zero (or by something that might be zero) in my proof, I've almost certainly made a mistake. I'd rather hear about it straight away than later when I try to use some fact about the result of that division.

MaxBarraclough 6y ago
For completeness: C++ eventually introduced a feature to allow something analogous to type-checking for template metaprogramming, called concepts - https://en.wikipedia.org/wiki/Concepts_(C%2B%2B) https://en.wikipedia.org/wiki/Concepts_(C%2B%2B)
nybble41 6y ago
> … it makes for errors a long way away from their causes, which are difficult to debug. It also means that any type errors that don't affect the expanded template (but may still have an effect on semantics) will not be caught at all.

somewhereoutth 6y ago

Using Scott encoding in the Lambda Calculus it is actually possible to define a 'usable' infinite natural number as a recursive construction (essentially its predecessor is defined as itself). Interestingly enough, constructions for add, (natural) subtract and multiply work as you would expect with this infinite number without needing special handling. E.g. for all n, n + inf == inf, n - inf == 0, n * inf == inf. Furthermore, the construction for (natural) div yields this infinite term (or at least something that behaves exactly like it) when the denominator is 0. Even more interestingly, 0/0 == inf for this system. EDIT: Why might this be useful? Well now when you 'take n' from a list, n=inf will give you the whole list, regardless of how long (or even if it is infinite - i.e. lazy). Likewise 'drop n' will return the empty list - except with an infinite list, whereupon the calculation will fail to terminate. EDIT: inf - inf == non-termination in this system, suggesting that not only inf - inf != 0, but it != inf either, and in fact it is something unreachable (in this system) (note the correspondence between 'subtract' and 'drop').

zodiac 6y ago
Mathlib does indeed define the extended real numbers, but they also need to define division on the reals. This is similar to the definition of subtraction having to be done for integers and for naturals (mentioned in the article)
- somewhereoutth 6y ago
  I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity. What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals). The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator): zero := \f \x n succ := \n \f \x f n infinite := \n succ (infinite n) infinity := infinite zero subn := \n \m m (\p n (\q subn q p) n) n divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m)) divn (succ zero) zero => infinity EDIT: Note that infinity does not have a normal form (does not terminate), but: subn n infinity => zero

Tainnor 6y ago

I ran into this argument before. I can understand that it makes sense for proof assistants. As the post shows, proof assistants don't allow you to misuse that anywhere else. (But as a sidenote: couldn't you fix this with dependent types somehow?) I still think it would be wrong for a regular programming language. Afaik, the Pony language does this too, but that is a general-purpose programming language that does not check your logic, and I am very wary of something like that. People might type up some algorithms, or even just try to compute an average, and the system absolutely should yell at you if you try to divide by zero.

1-more 6y ago
Elm does this for integers (Floats support Infinity, natch) and I support it. Elm is meant for writing declarative UIs, and the only example I could think of for blindly dividing by 0 is taking the average of an empty list without checking first. But any time you might do that, you'd be better served by matching on the empty list _before_ trying to take the average and rendering something helpful for the user.
ogogmad 6y ago
> (But as a sidenote: couldn't you fix this with dependent types somehow?) Most proof assistants, including Lean, are built on dependent type theory.
- Tainnor 6y ago
  Sure but then I guess maybe you can find ergonomic improvements to your dependent type system so as not to run into the problems discussed in the article (e.g. having to reprove that something is not zero over and over again).
  - OscarCunningham 6y ago
    Maybe the way to do that would be to prove once that x is nonzero, use that to define r = 1/x, and thereafter use multiplication by r?
6y ago

Someone 6y ago

I don’t think the “in type theory” restriction is correct. This choice works fine when using type theory in theorem provers, but would be unacceptable if we did it in programming languages that use type theory (or would that be called “type practice” ;-)?) In Haskell, for example, 1/0 returns Infinity.

Sniffnoy 6y ago
That's not exactly right... in Haskell, 1/0 has type Fractional a => a. So, it could be any fractional type. If 1/0 occurs in a context where it'll be interpreted as a floating-point number, you'll get Infinity, yes, as per how standard floating-point works. In other contexts though you may get an error. E.g., if you import Data.Ratio and do 1/0 :: Rational, you'll get an error.
dddbbb 6y ago
The type signature of division in Haskell merely requires that it takes two fractional `a`s and returns another `a`. 1 / 0 :: Double evaluates to Infinity. 1 / 0 :: Rational throws a runtime exception. A division by zero producing zero would be perfectly sensible in Haskell, and perhaps even desired if you are totally averse to runtime errors. The Pony language infamously does this.
curryhoward 6y ago
In academia, "type theory" almost always means dependent type theory, such as Martin-Löf type theory or homotopy type theory. Type theory is used in most theorem provers as a foundation for mathematics. The title of this blog post is using the term in a standard way. Programming languages such as Haskell and Java are not based on type theory. They have type systems. Haskell's type system is much closer to type theory than that of Java, but it's still quite crippled compared to what type theorists study. It is of course possible to define things in type theory such that 1/0 = Infinity or something else, but that is not the norm.

dvt 6y ago

The title is a bit sneaky. Division by zero in "type theory" will depend on just that -- your type theory. Some theories use special values for division by zero (e.g. could spit out DNE or +INF/-INF). But then you need to formalize how you do "things" with DNE or infinities. This is, more often than not, an unnecessary rabbit hole, so just returning 0 is simpler. Some theories might require a proof that the denominator isn't zero (essentially making division a three-argument function) -- which is kind of a cool way of thinking about it[1]. [1] https://math.stackexchange.com/questions/334393/how-does-type-theory-handle-division-by-zero-and-such https://math.stackexchange.com/questions/334393/how-does-typ...

nshepperd 6y ago

This strikes me as having some interesting similarity to the practice in Haskell of placing type class constraints on functions, not data types. A deprecated feature of Haskell used to allow you to write data types like: data Ord k => Map k v = ... This defined a data type representing an ordered map from k to v, with the additional restriction that before you can talk about such a map you had to know that the type k is orderable (has an instance of the Ord type class which defines comparison operators). This may be considered to be similar to the definition of (/) requiring that its second argument is nonzero. This style was supplanted by leaving the data type definition 'bare' and placing the constraints on the API's functions instead: data Map k v = ... insert :: Ord k => k -> v -> Map k v -> Map k v lookup :: Ord k => k -> Map k v -> Maybe v This style is similar to instead placing the nonzero-ness constraint on the theorems which define the API of (/). In both cases there are basic engineering reasons for the switch: - Having the constraints in the definition of terminology (Map, /) doesn't save any work, as you still need to prove those constraints to do anything or refer to it (in Haskell this meant sprinkling `Ord k =>` in the type of anything that referred to Map k v). - In fact it results in doing more work than necessary, as you are sometimes forced to prove the constraints just to mention Map, even when what you are doing does not require them. For instance defining the empty map 'empty :: Map k v' shouldn't require you to know anything about k, because an empty tree doesn't contain any keys, let alone care about their ordering. In this case requiring Ord k in order to mention Map k v would be superfluous.

Ar-Curunir 6y ago
Rust tends to take the second approach as well; it tends to place trait bounds on `impl` blocks, and not on the struct itself. (This is by no means a standard across the community though; I'd say it's a 50/50 split)
- wh33zle 6y ago
  A case where it is unavoidable is when you want to refer to an associated type in your struct declaration. In most other cases, putting bounds on impls leads to less repetition of those bounds and better error messages! Another related topic is trait methods with method-level type parameters that have bounds. Those have to be repeated on every usage site so it is usually preferable to go for a design that has the type parameters in the actual trait. Instead of: trait Foo { fn foo<T: Bar>(&self, bar: T) } do this instead: trait Foo<T> { fn foo(&self, t: T) } impl<T: Bar> Foo for XYZ { fn foo(&self, bar: T) { } } One bound might seem fine in this example but once stuff needs to be Send, Sync and 'static is when it gets annoying.

dwheeler 6y ago

Obviously a system can define a symbol like "/" as whatever it wants to. But then it isn't what many mathematicians would expect. The Metamath Proof Explorer defines "/" so it only has a value if the denominator is a nonzero complex number: http://us.metamath.org/mpeuni/df-div.html http://us.metamath.org/mpeuni/df-div.html You can argue if that is better, but that is a possible choice.

credit_guy 6y ago

With humility I will say that I don't like this solution. In mathematics functions have domains and codomains. Two functions are equal if their domains are equal, their codomains are equal, and for all the values in the domain they return the same values in the codomain. A mathematician who doesn't know anything about type theory, but hears Lean is good at formalizing math, will expect the division function to have the domain R x (R\{0}). Modifying the domain to be R x R and returning a garbage value for the added points is not a good solution. Maybe it works "in real life", but you always need to carry with you an invisible asterisk and footnote that Lean did the right thing only assuming you asked the right question. Again, being humble (my Lean experience is about one hour in total, spread across several sessions), I think it would be better to invest a bit more time upfront and always define properly the domain of the function used, rather than introduce edge cases that can bite you in the back twenty five theorems down the road.