Please, don’t conflate “functional” (e.g. Clojure) with “typeful” (e.g. Rust). They are different, though not incompatible: Functional style simplifies structure, typeful style makes structure explicit.
Firstly “Typeful” is more ML than rust. While it’s unfortunate that “functional style” must have different meanings in different contexts, it’s the unfortunate reality we live in. Statically typed languages manifest functional style differently than dynamically typed languages, and they should.
ML is both typeful and functional. I wanted to give examples of a language that is functional but not typeful (Clojure) and another that is typeful but not functional (Rust), to emphasize that both qualities needn’t come hand in hand in a language design.
Just to be clear: By “typeful”, I don’t mean “statically typed”, but rather “statically typed and the types tell you a significant part of what’s going on in the program”. It happens to be the case that statically typed functional languages are typeful, because it happens to be the case that the type structure of functional programming is well understood: the Brouwer-Heyting-Kolmogorov and Curry-Howard correspondences predate computers and programming languages themselves! What makes Rust an interesting case is that it’s one of the first attempts at capturing the type structure of imperative programming (mutation, aliasing, concurrency control).
I see, I had misinterpreted your intent. I agree in the case of Rust it has aspects of ADT but isn’t functional first, wheras clojure is functional first but is missing ADT, but in the context of the language they’re talking about I’d definitely say the type system is intertwined with its functional style. So I don’t think there’s any conflation, but I can see now why you felt it was important to point that out.
The type systems of Scala, Haskell, ML, etc. happen not to have any means to accurately describe the structure of imperative programs beyond I/O segregation and reference cells, as a way to say “here be dragons!” That’s why typeful programming in those languages exerts pressure towards using a functional style. This is a limitation of those particular languages, not typeful style, though.
Weird claim, the monad bind operation is a perfect way to model imperative operations. Also, ML and Scala don’t enforce that segregation at all.
Monads allow you to embed an effectful object language inside a pure metalanguage, but they don’t let you actually tame the effects that happen in the effectful language. For instance, Haskell’s IO is actually unsafe in the presence of concurrency: you can mutate the same IORef from two different threads at the same time, and the results will be just as disastrous as if you did the same thing in Java or C++ or whatever.
The type systems of Scala, Haskell, ML, etc. happen not to have any means to accurately describe the structure of imperative programs beyond I/O segregation and reference cells, as a way to say “here be dragons!”
It sounds like people’s use of the free monad over algebras representing their chosen effects is one of many solutions to this problem. Do you mean something else?
Can you use monads to statically enforce correct concurrency control? Or to prevent use-after-free for resources that need manual cleanup?
As far as I can tell, the only effects that can be adequately managed using monads alone are those that can be “desugared” back to purely functional programs: exceptions (EitherT), nondeterminism (ListT), etc. For “intrinsically imperative” stuff, you need something else.
I believe you can use indexed monads to model substructural types, but nobody, as far as I can see, actually does this in real code. Nobody even understands what indexed monads are from a mathematical perspective! In any case, Rust definitely makes it much more practical to write safe imperative code that handles resources concurrenty and efficiently. I’d still prefer the Haskell way though, since it’s better at everything else :) when efficiency is a concern, I drop down to C++ and be really really careful.
I don’t think it’s fundamentally impossible to design a single language that’s good at both what ML and Haskell do well (manipulate “eternal” values) and what Rust does well (manipulate “ephemeral” resources). This is a very rough sketch of what I think such a language could look like:
Use call-by-value evaluation.
Distinguish destruction (which is deterministic and controlled by the programmer, as in Rust) from deallocation (which is performed by a garbage collector, as in ML and Haskell).
Distinguish a special class of types, let’s call them cptypes, that are guaranteed to have trivial destructors. This works in a similar fashion to Standard ML’s eqtypes, which are guaranteed to have decidable equality. See here and here for details.
The basic type formers are sum, tuple, function and object types.
Sum and tuple types are cptypes iff their type parameters and constructor payloads are cptypes. This mirrors the rule for eqtypes in Standard ML.
Function types come in two flavors: functions (-o) and cpfunctions (->). foo -> bar is always a cptype, and foo -o bar never is (regardless of what foo and bar are), and the former is a subtype of the latter.
foo -> bar
foo -o bar
Object types are never cptypes, since objects (and only objects!) can have programmer-defined destructors.
A value can be used more than once iff its type is a cptype.
Of course, this glosses over many details, and figuring out those details is precisely why it took Rust so many years to go from 0.x to 1.x. But a new language has the benefit of hindsight, and, in any case, when exploring the design space, “do as Rust does” is a sensible starting point.
As for indexed monads, I object to the name, unless someone can show that they are actual monads. In any case, they don’t seem to be elegant.
Haskell’s ST data type is a way to prevent leaking of state. It’s possible to use ST to ensure resources stay within a scope and are cleaned up.
I’m not completely sure about concurrency control. You mean something like Haskell’s acid-state?
ST is effectively a single monadic region: all resources are deallocated all-at-once at the end of the ST action that you pass to runST. But, even considering nested monadic regions in their full generality, you couldn’t possibly express the following pattern:
This pattern arises, for example, in the implementation of concurrent B+ tree variants internally used by DBMSs.
I mean the ability to:
But, even considering nested monadic regions in their full generality, you couldn’t possibly express the following pattern:
You can’t? Can’t you use free coproduct style to express that kind of chain with ST-style regions? (Or indeed just an ST-like monad that uses a type-level list of the currently open regions). A/B/… would each be indexed by their own type.
The fundamental problem is that monadic regions are monad transformers, and monad transformers impose a stack discipline. Every step of the pattern I described, other than the first and last ones, requires the ability to deallocate the second topmost element of the stack while retaining the topmost one. You need substructural types.
Monad transformers are one possible way to encode monadic regions, and have the nesting limitation you describe. But they’re not the only way to write them, and other encodings do not have that limitation (e.g. on http://okmij.org/ftp/Haskell/regions.html I believe the “heavy-weight implementation” allows your interleaved A/B/C/… scenario - the nesting restriction is explicitly noted as a limitation of the lightweight implementation only).
Why should I trust that the type system used in the “heavy-weight implementation” is sound?
Why do you trust that the Rust borrow checker is sound? Or any other means of enforcing this kind of constraint?
The comments at the top sketch an argument that the use of OverlappingInstances is safe and explain that IncoherentInstances is only for compatibility with older versions (though I would certainly understand confirming that oneself). AIUI UndecidableIstances does not present soundness issues, in the sense that anything that compiles successfully with that extension is sound (just that compilation may not terminate, or in practical terms compilation of some sound programs may time out)
I trust substructural types because they tackle the problem of resource management directly, rather than by means of hacky workarounds. Using rank-2 types (ST) to get local mutation is completely ridiculous.
I trust the borrow checker because I’ve read the ATTAPL chapter on region-based memory management, as well as the papers by Tofte and Talpin on region-based memory management. In this regard, Rust’s improvements are primarily a matter of ergonomics (elision), but the fundamental system is the same. That covers immutable borrows.
As for mutable borrows, I trust them because they’re effectively syntactic sugar for a pattern where a caller transfers ownership to a callee, with a promise that the callee will transfer ownership back to the caller when it’s done. Since I already trust both substructural types and regions, it’s not hard to trust mutable borrows as well.
I trust a complex implementation written as a library more than I trust a simple implementation that’s only available as a language-level builtin, just based on past experience. Using rank-2 types doesn’t particularly bother me because I’m already used to them and would want them in my programming language for other reasons, so the implementation of other features may as well use them. I would prefer direct support for affine or linear types (I’m not familiar with substructural types), sure, but I see that as an implementation detail. It’s a hack in the sense of being an ugly workaround, but not in a sense that impairs correctness.
Monadic regions are also an implementation of regions so I don’t see the academic backing for Rust’s borrow checker as being any stronger or weaker than that for monadic region libraries?
Monadic regions only account for immutable borrows. Most interesting types that can be nicely implemented in Rust but not in Haskell have operations that require mutable borrows.
As far as I can tell, the only effects that can be adequately managed using monads alone are those that can be “desugared” back to purely functional programs
They have precisely the same power as delimited continuations in a call-by-value language
Right. And, if I recall correctly, delimited continuations are just particular higher-order functions, which can be no more effectful than the host language is.