7 ms·

"Controversial: Flix defines division by zero to equal zero." Wait what. Can I read up on the motivation somewhere?

• deleted 1y ago
  [deleted]
• mkl 1y ago
  The FAQ (https://flix.dev/faq/#:~:text=Dividing%20by%20zero%20yields%20zero https://flix.dev/faq/#:~:text=Dividing%20by%20zero%20yields%...) links to https://www.hillelwayne.com/post/divide-by-zero/ https://www.hillelwayne.com/post/divide-by-zero/, which is more about Pony, but links to https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... which properly explains that it's helpful for proof assistants to define division by zero, with particular reference to Lean. Really it's defining a division-like function (Lean calls it real.div) that disagrees with division in this one way, and then making "/" use it. It's unclear to me if this is sensible in a general purpose programming language that isn't a proof assistant.
  • remon 1y ago
    Ah thanks for the insights and references. And yes I'm still curious why this definition of div/0==0 is needed in the context of Flix
    • remon 1y ago
      Gotta be honest, this isn't very inspiring : "Wait, division by zero is zero, really? Yes. But focusing on this is a bit like focusing on the color of the seats in a spacecraft."