4 ms·

> Surely it would be better to use a Maybe type for this instead? > > 0 / 1 = Just 0 > 0 / 0 = Nothing This would make it impossible to compose mathemati

by lgas 3y ago

> Surely it would be better to use a Maybe type for this instead? > > 0 / 1 = Just 0 > 0 / 0 = Nothing This would make it impossible to compose mathematical expressions of more than one operation without discharging the Maybe which would get ugly fast.

munchler 3y ago
But that's the true nature of division. Unless one can prove that the denominator is non-zero, then the computation is not well defined. Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.
- trealira 3y ago
  It seems like it would be more practical to create non-zero integer/other number types, and only those can be used as denominators. But it would also be nice to not have to make a custom subtype every time you needed something with a specific property.
  - munchler 3y ago
    Agreed. I think this is where dependent types become useful, but that is a whole can of worms.
- nyrikki 3y ago
  Division isn't closed on the natural numbers. Total functions have to return either true or false explicitly, failure as negation doesn't work. That is where you get Gödel's 'this statement is false' from. This is the law of the excluded middle that broke the Mathmatica Principia. Plato, Aristotle, and Russell's use of the law of the excluded middle is what Gödel, Church, and Turning leverages. For problems in P this distinction is harder to see because P=co-P but we think NP!=co-NP. As NP are by definition decision problems this is important. NP being the provable yes-instances and co-NP being the no-instances, even proving a function is total is hard. If you accept failure as negation you may be able to build a sun-Turing machine that always halts but you won't be able to show it is complete and consistent. That is why ZF disallows statements like 'this statement is false'.
  - mrkeen 3y ago
    > even proving a function is total is hard. It's best left to the compiler. But if you're considering doing it, don't imagine yourself taking an existing function like qsort and trying to prove it's total. Instead try building up a new function and only build it out of other total functions.
    - nyrikki 3y ago
      If your language is TC and thus supports general recursion, no algorithm can possibly exist for deciding whether a function is in fact total in the general case. As all primitive recursive functions are provably total, that is a place a compiler can work. But just using for loops gets you there too. Total functions that are also pure functions are a pretty small set so there may be other reductions like the above. But don't depend on the compiler. But I agree writing total functions from the start is the ideal if possible.
- madmax96 3y ago
  Dependently typed languages make it even better. For example, in Lean4: def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat := if denominator > numerator then 0 else 1 + myDiv (numerator - denominator) denominatorNotZero -- Example usage. example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl You have to submit a proof that the denominator is non-zero in order to use `myDiv`. No monad required ;).
- jimbokun 3y ago
  Can Haskell enforce a type of “any integer other than zero”? I feel like you would just end up with the equivalent of Maybe, but not sure.
  - Iceland_jack 3y ago
    With https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/, but as a separate checker. I think there are talks of integrating it into the compiler
mrkeen 3y ago
It was ugly. And then do-notation arrived in around 1999 (I think - I'd be super happy if someone can find a precise year for me) and it became a solved problem. Just in time for people to ignore it and start complaining about the ugliness of flatMap from 2015 onwards.

by lgas 3y ago

munchler 3y ago

But that's the true nature of division. Unless one can prove that the denominator is non-zero, then the computation is not well defined. Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.

trealira 3y ago
It seems like it would be more practical to create non-zero integer/other number types, and only those can be used as denominators. But it would also be nice to not have to make a custom subtype every time you needed something with a specific property.
- munchler 3y ago
  Agreed. I think this is where dependent types become useful, but that is a whole can of worms.
nyrikki 3y ago
Division isn't closed on the natural numbers. Total functions have to return either true or false explicitly, failure as negation doesn't work. That is where you get Gödel's 'this statement is false' from. This is the law of the excluded middle that broke the Mathmatica Principia. Plato, Aristotle, and Russell's use of the law of the excluded middle is what Gödel, Church, and Turning leverages. For problems in P this distinction is harder to see because P=co-P but we think NP!=co-NP. As NP are by definition decision problems this is important. NP being the provable yes-instances and co-NP being the no-instances, even proving a function is total is hard. If you accept failure as negation you may be able to build a sun-Turing machine that always halts but you won't be able to show it is complete and consistent. That is why ZF disallows statements like 'this statement is false'.
- mrkeen 3y ago
  > even proving a function is total is hard. It's best left to the compiler. But if you're considering doing it, don't imagine yourself taking an existing function like qsort and trying to prove it's total. Instead try building up a new function and only build it out of other total functions.
  - nyrikki 3y ago
    If your language is TC and thus supports general recursion, no algorithm can possibly exist for deciding whether a function is in fact total in the general case. As all primitive recursive functions are provably total, that is a place a compiler can work. But just using for loops gets you there too. Total functions that are also pure functions are a pretty small set so there may be other reductions like the above. But don't depend on the compiler. But I agree writing total functions from the start is the ideal if possible.
madmax96 3y ago
Dependently typed languages make it even better. For example, in Lean4: def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat := if denominator > numerator then 0 else 1 + myDiv (numerator - denominator) denominatorNotZero -- Example usage. example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl You have to submit a proof that the denominator is non-zero in order to use `myDiv`. No monad required ;).
jimbokun 3y ago
Can Haskell enforce a type of “any integer other than zero”? I feel like you would just end up with the equivalent of Maybe, but not sure.
- Iceland_jack 3y ago
  With https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/, but as a separate checker. I think there are talks of integrating it into the compiler

mrkeen 3y ago

It was ugly. And then do-notation arrived in around 1999 (I think - I'd be super happy if someone can find a precise year for me) and it became a solved problem. Just in time for people to ignore it and start complaining about the ugliness of flatMap from 2015 onwards.