3 ms·

What do you mean by, "Languages like Haskell are built to do mathematics in first-and-foremost"? It's hard for me to find a reasonable interpretation of this s

What do you mean by, "Languages like Haskell are built to do mathematics in first-and-foremost"? 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.

goatinaboat 6y ago
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. 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!
- gowld 6y ago
  Everything in computers is math. Floating point numbers are math. Java generics with inheritance are math. It's not a point of distinction.
- spekcular 6y ago
  So let me ask again: in what sense do people "do mathematics" in Haskell? They don't really "do" category theory, for example; simply noting that something forms a category is mathematics only in the most trivial sense.
- BeetleB 6y ago
  > All that stuff about types and categories and monads and so on is maths too. 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?
- throwaway518365 6y ago
  Not much afaict. For mathematics, it's usually Coq, maybe Lean or Agda. For scientific computing it's Python or Julia.
  - ghostwriter 6y ago
    You can use HaskellR (https://tweag.github.io/HaskellR/ https://tweag.github.io/HaskellR/) for everything scientific that is being written in Python and Julia.
  - danielscrubs 6y ago
    To be fair, Agda is a fusion of Martin-Löf type theory and Haskell if my memory serves me.
danielscrubs 6y ago
He probably mean a heavy focus on type theory. It has been used in formal verification as a prototype tool [1]. [1]: https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...

goatinaboat 6y ago

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. 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!

gowld 6y ago
Everything in computers is math. Floating point numbers are math. Java generics with inheritance are math. It's not a point of distinction.
spekcular 6y ago
So let me ask again: in what sense do people "do mathematics" in Haskell? They don't really "do" category theory, for example; simply noting that something forms a category is mathematics only in the most trivial sense.
BeetleB 6y ago
> All that stuff about types and categories and monads and so on is maths too. 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?
throwaway518365 6y ago
Not much afaict. For mathematics, it's usually Coq, maybe Lean or Agda. For scientific computing it's Python or Julia.
- ghostwriter 6y ago
  You can use HaskellR (https://tweag.github.io/HaskellR/ https://tweag.github.io/HaskellR/) for everything scientific that is being written in Python and Julia.
- danielscrubs 6y ago
  To be fair, Agda is a fusion of Martin-Löf type theory and Haskell if my memory serves me.

danielscrubs 6y ago

He probably mean a heavy focus on type theory. It has been used in formal verification as a prototype tool [1]. [1]: https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...