3 ms·

My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you'r

My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." Yes, you can embed those semantics inside functional semantics, and even use the functional language to add more static verification at the type level via things like F-Star's Hoare logic. But you're still mostly going to shoving bits in specific places based on the result of a shallow pure function applied to bits you yanked from a specific place. On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation (and which are hard to avoid categorically), so you'll need to work within an especially restrictive DSL. Definitely no lambdas or partial application. So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Where in this do you see any functional-ness, outside of the fact that you'll probably call your procedures functions? > Many useful & powerful functional abstractions can be written to use constant space, even in Haskell. Yes, but not to the degree that Atom's use cases require (where the program must allocate all memory ahead of time and therefore know a specific upper bound). This necessitates deviation from usual practices of any kind, including Haskell's.

KirinDave 10y ago
> My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." The difference being that this "very fine imperative language" has much stronger type safety guarantees. Maybe we can stop having ring0 buffer overflows some day when C programmer pride is sufficiently assuaged. I doubt it though... My experience with the linux kernel community is that it is a limitless void of insecurity and infighting. > On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation OCaml does much better here (in fact, really quite amazingly well here, on part with some of the greatest common lisp distribution compilers which were stunningly good at it). But yeah, Haskell has a very poor focus on the needs of the "industry" when said industry is focused around extremely tight optimizations. That said, I refuse to confuse a specific example of FP with a traditionally academic and research focus with the discipline as a whole. That's a dodge. > So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Honest question: what's the problem with this if it offers additional safety and promotes the use of stateless functions? If it all compiles down to similar code, then it's fine. People act like monadic code is not functional, when it is in fact extremely functional code. That's what's funny about all this: imperative programming is expressible succinctly and easily in functional languages.
- johncolanduoni 10y ago
  It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these cases. Your proofs will be full of the typical halmarks of functional programing, and for the stuff that is executed at runtime you'll definitely want some pattern matching, but there will be no closures or higher-order functions and limited opportunities for monads, functors, etc. Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.
- AnimalMuppet 10y ago
  > The difference being that this "very fine imperative language" has much stronger type safety guarantees. Is that a result of the specific language, rather than FP? That is: One could think about building a procedural language that had... well, I'm not sure it could have Hindley-Milner types, because I'm not sure it could have higher-kinded types, but it could come close, couldn't it? And from the other side: Does FP require very strong types? Or can it be done with something equivalent to C/C++'s type system? Or Python's?

KirinDave 10y ago

> My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." The difference being that this "very fine imperative language" has much stronger type safety guarantees. Maybe we can stop having ring0 buffer overflows some day when C programmer pride is sufficiently assuaged. I doubt it though... My experience with the linux kernel community is that it is a limitless void of insecurity and infighting. > On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation OCaml does much better here (in fact, really quite amazingly well here, on part with some of the greatest common lisp distribution compilers which were stunningly good at it). But yeah, Haskell has a very poor focus on the needs of the "industry" when said industry is focused around extremely tight optimizations. That said, I refuse to confuse a specific example of FP with a traditionally academic and research focus with the discipline as a whole. That's a dodge. > So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Honest question: what's the problem with this if it offers additional safety and promotes the use of stateless functions? If it all compiles down to similar code, then it's fine. People act like monadic code is not functional, when it is in fact extremely functional code. That's what's funny about all this: imperative programming is expressible succinctly and easily in functional languages.

johncolanduoni 10y ago
It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these cases. Your proofs will be full of the typical halmarks of functional programing, and for the stuff that is executed at runtime you'll definitely want some pattern matching, but there will be no closures or higher-order functions and limited opportunities for monads, functors, etc. Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.
AnimalMuppet 10y ago
> The difference being that this "very fine imperative language" has much stronger type safety guarantees. Is that a result of the specific language, rather than FP? That is: One could think about building a procedural language that had... well, I'm not sure it could have Hindley-Milner types, because I'm not sure it could have higher-kinded types, but it could come close, couldn't it? And from the other side: Does FP require very strong types? Or can it be done with something equivalent to C/C++'s type system? Or Python's?