Those languages that choose to use options or results with ?. instead of null or exceptions are already choosing to avoid impure functions and use static typing.
An impure "function" is any procedure which may have side-effects or produce different results for the same formal arguments depending on the runtime environment or evaluation order. Most languages with option or result types (e.g. Rust) still make extensive use of impure procedures. Haskell and its close relatives are pretty much the only well-known exceptions with first-class pure functions enforced through the type system.
Purity is always a spectrum - Haskell allows non-terminating "functions", for example. Choosing to treat certain kinds of failures as valid function evaluations that can be reasoned about under the normal rules of the language is a step in the direction of purity. More to the point, it's the aspect of purity that's salient when we're talking about whether it makes sense to regard these particular constructs as monads.
Haskell allows non-terminating "functions", for example.
Non-terminating functions are still pure functions in the mathematical sense. While it does somewhat complicate the use of programs as proofs, a pure function doesn't need to have a defined value for every possible input. A better example might have been unsafePerformIO which, like "unsafe" in Rust, is meant to be used to construct a pure interface to impure code but depends on the programmer to handle it properly. The difference is that Rust doesn't require "unsafe" around all side-effects, just those that may impact memory safety.
I would agree that Option and Result types represent "a step in the direction of purity", but even a little bit of impurity nullifies referential transparency and inhibits equational reasoning.
... it's the aspect of purity that's salient when we're talking about whether it makes sense to regard these particular constructs as monads.
A construct is a monad if it obeys the monad laws for all well-typed inputs. In languages like Rust or JS which lack any type-level enforcement of purity the constructs are only monads under the condition that the inputs happen to be pure, not in the general case. For example, for any functor (which includes all monads) we have the law "map f . map g == map (f . g)". However, if f and g may have side effects then substituting one side for the other will interleave the effects in a different order and potentially change the result, so the monad laws are not satisfied.
Non-terminating functions are still pure functions in the mathematical sense.
No they're not. Mathematically a function must evaluate to a value.
I would agree that Option and Result types represent "a step in the direction of purity", but even a little bit of impurity nullifies referential transparency and inhibits equational reasoning.
It doesn't nullify anything; the "Fast and Loose Reasoning is Morally Correct" result applies just as well to a language with, say, nulls, as it does to the impure parts of Haskell that it was originally addressed at. The more relevant these aspects of your language are to practical programs, the less useful reasoning one can do, but it's very much a spectrum rather than a binary.
In languages like Rust or JS which lack any type-level enforcement of purity the constructs are only monads under the condition that the inputs happen to be pure, not in the general case. For example, for any functor (which includes all monads) we have the law "map f . map g == map (f . g)". However, if f and g may have side effects then substituting one side for the other will interleave the effects in a different order and potentially change the result, so the monad laws are not satisfied.
Pure is not a binary; rather the law holds to the extent that the functions are pure (that is, the two sides of the law are equivalent to each other in the same sense that the function is equivalent to its evaluation). Even in Haskell you have cases of the same kind of law violation where two expressions should be equivalent (according to the monad laws) but one terminates and the other doesn't.
Mathematically a function must evaluate to a value.
For every input within its domain, yes. Whether this is a problem for partial functions will depend on how you define the domain: either exactly the set permitted by the function's type, or the subset of well-typed inputs with an associated value. As far as I can tell the most common definition of the domain for a relation or function is the set of inputs which have at least one associated result; on the other hand, those definitions are not concerned with the function's type. I would say that the input type is only an approximation (superset) of the function's domain, with better type systems permitting closer approximations. (For perspective, I've never known anyone to argue that the result type must perfectly capture the function's range, which is defined much the same way as the set of results associated with at least one input.)
The more relevant these aspects of your language are to practical programs, the less useful reasoning one can do...
There is indeed a spectrum of varying degrees of impurity among impure languages, depending on both language design and custom among its users. However, there is one key area where the classification is binary, and that is in the answer to the question: Does the language assume referential integrity or not? In Haskell the answer is "yes". The compiler will make substitutions under the assumption that evaluation does not have side effects; if you break that expectation, via unsafePerformIO or other means, the result is undefined. In Rust or Javascript the answer is "no", and various optimizations are prevented because the compiler cannot assume that the evaluation of an unknown function will not have side effects.
Even in Haskell you have cases of the same kind of law violation where two expressions should be equivalent (according to the monad laws) but one terminates and the other doesn't.
If one side doesn't terminate then you can never get to the point of observing that they have different results. The point of "fast and loose reasoning" is that you only need to prove that the laws are never broken within the program. The condition "map f . map g == map (f . g)" cannot evaluate to False... but that doesn't mean it must evaluate to True. In Rust or JS, however, that condition could evaluate to false in the presence of side effects.
Comments
An impure "function" is any procedure which may have side-effects or produce different results for the same formal arguments depending on the runtime environment or evaluation order. Most languages with option or result types (e.g. Rust) still make extensive use of impure procedures. Haskell and its close relatives are pretty much the only well-known exceptions with first-class pure functions enforced through the type system.
Purity is always a spectrum - Haskell allows non-terminating "functions", for example. Choosing to treat certain kinds of failures as valid function evaluations that can be reasoned about under the normal rules of the language is a step in the direction of purity. More to the point, it's the aspect of purity that's salient when we're talking about whether it makes sense to regard these particular constructs as monads.
Non-terminating functions are still pure functions in the mathematical sense. While it does somewhat complicate the use of programs as proofs, a pure function doesn't need to have a defined value for every possible input. A better example might have been unsafePerformIO which, like "unsafe" in Rust, is meant to be used to construct a pure interface to impure code but depends on the programmer to handle it properly. The difference is that Rust doesn't require "unsafe" around all side-effects, just those that may impact memory safety.
I would agree that Option and Result types represent "a step in the direction of purity", but even a little bit of impurity nullifies referential transparency and inhibits equational reasoning.
A construct is a monad if it obeys the monad laws for all well-typed inputs. In languages like Rust or JS which lack any type-level enforcement of purity the constructs are only monads under the condition that the inputs happen to be pure, not in the general case. For example, for any functor (which includes all monads) we have the law "map f . map g == map (f . g)". However, if f and g may have side effects then substituting one side for the other will interleave the effects in a different order and potentially change the result, so the monad laws are not satisfied.
No they're not. Mathematically a function must evaluate to a value.
It doesn't nullify anything; the "Fast and Loose Reasoning is Morally Correct" result applies just as well to a language with, say, nulls, as it does to the impure parts of Haskell that it was originally addressed at. The more relevant these aspects of your language are to practical programs, the less useful reasoning one can do, but it's very much a spectrum rather than a binary.
Pure is not a binary; rather the law holds to the extent that the functions are pure (that is, the two sides of the law are equivalent to each other in the same sense that the function is equivalent to its evaluation). Even in Haskell you have cases of the same kind of law violation where two expressions should be equivalent (according to the monad laws) but one terminates and the other doesn't.
For every input within its domain, yes. Whether this is a problem for partial functions will depend on how you define the domain: either exactly the set permitted by the function's type, or the subset of well-typed inputs with an associated value. As far as I can tell the most common definition of the domain for a relation or function is the set of inputs which have at least one associated result; on the other hand, those definitions are not concerned with the function's type. I would say that the input type is only an approximation (superset) of the function's domain, with better type systems permitting closer approximations. (For perspective, I've never known anyone to argue that the result type must perfectly capture the function's range, which is defined much the same way as the set of results associated with at least one input.)
There is indeed a spectrum of varying degrees of impurity among impure languages, depending on both language design and custom among its users. However, there is one key area where the classification is binary, and that is in the answer to the question: Does the language assume referential integrity or not? In Haskell the answer is "yes". The compiler will make substitutions under the assumption that evaluation does not have side effects; if you break that expectation, via unsafePerformIO or other means, the result is undefined. In Rust or Javascript the answer is "no", and various optimizations are prevented because the compiler cannot assume that the evaluation of an unknown function will not have side effects.
If one side doesn't terminate then you can never get to the point of observing that they have different results. The point of "fast and loose reasoning" is that you only need to prove that the laws are never broken within the program. The condition "map f . map g == map (f . g)" cannot evaluate to False... but that doesn't mean it must evaluate to True. In Rust or JS, however, that condition could evaluate to false in the presence of side effects.