> And before you say "why not just break the runtime model", by e.g. having special debug functions that can do IO while presenting to the runtime as pure functions—well, it's not impossible, in theory, but it's a Hard Problem.
import Debug.Trace
square x =
trace "I'm a Hard Problem" (x * x)
main =
print (square 3)It's hard for me to find a reasonable interpretation of this sentence that is true. I'm not sure much serious mathematics is done is Haskell, beyond the usual arithmetic operations present in most programs, especially relative to other programming languages. It hasn't taken off in the numerical computating market, for example.
Historically, it also seems like Haskell was built as a research language.
[1]: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
All that stuff about types and categories and monads and so on is maths too. Arithmetic or numerical work is only a subset of that field. Lots of maths doesn’t even involve numbers!
They don't really "do" category theory, for example; simply noting that something forms a category is mathematics only in the most trivial sense.
I think the question he's asking is: What papers have been published in math journals where the work was done in Haskell? Which mathematicians use Haskell to do mathematics work?
foo :: IO X
0: Which is a completely resonable thing to do, and the basis of any language's standard library, the ability to recapitulate which in normal code separates good languages from Go-like special-cases-for-me-but-not-for-thee languages.
> We are just trying to build things here.
Some languages are built to do engineering first-and-foremost. Languages like Haskell are built to do mathematics in first-and-foremost. This doesn't mean that such languages aren't also well-engineered, or that they aren't also tuned to do engineering in; but the engineering concerns must be subordinated to not breaking the model that mathematicians rely upon to do math in the language. So you can't just e.g. change whether a particular kind of function can emit IO or not; or change what values exist as part of the lattice of a type; or any number of other things visible within the language's abstraction; because those very properties/constraints are also syllogisms which are relied upon in mathematics done in the language.
And before you say "why not just break the runtime model", by e.g. having special debug functions that can do IO while presenting to the runtime as pure functions—well, it's not impossible, in theory, but it's a Hard Problem, because those properties that a function presents to the runtime are also used by the compiler to optimize (or memoize, or fuse, or eliminate) code. You can't really declare something as a pure function without the runtime thinking it can do all sorts of things that result in the function being called less.
In theory, Haskell could have something like a "volatile" qualifier for functions, sort of like C's volatile qualifier for data, to tell the runtime that while the function has type X, all optimization opportunities that would normally apply to type X are off the table. Then you could have special debug functions of type X. It's just that getting this working would require a lot of re-work throughout the compiler, since the compiler mostly deduces optimization opportunities from the type (and marks something as having more optimization opportunities by proving that it has an extra applicable type), rather than just tracking some separate metadata that can be arbitrarily written to.