Traits are designed in such a way that there always is some privileged “receiver” type. In abstract datatypes, ML modules, and type classes there isn't this bias. In an ADT you can have a number of associated abstract datatypes, and in type classes all the 'parameters' are treated equivalently (other than order of the arguments which is a little annoying). To compare:
module type Add = sig
type lhs
type rhs
type out
val add : lhs -> rhs -> out
end
class Add lhs rhs where
type Out
add : lhs -> rhs -> Out lhs rhs
trait Add<Other = Self> {
type Out;
fn add(self, other: Other) -> Self::Output
}
The way Rust does it is nice for more OOP-style usages of traits, but is annoying if you go outside of that (like with the operator traits). This is a personal annoyance, and would have other knock-on effects if it were changed, but does annoy me sometimes, hah.
> What is definitional equality? What does an abstract type alias look like?
Sorry, type theory lingo. Definitional equality means (in the way I was using it - there's some subtlety) that when comparing two things, you look at the definitions, potentially performing some computations to simplify things down. For example, if I had:
pub type Id<T> = T;
pub type Pair<T, U> = (T, U);
pub fn foo((x, _): Id<(i32, String)>) -> i32 { x }
Then I can supply a `y: Pair<String, i32>` to `foo` from another module and everything will be ok, because Rust computes the underlying type when comparing the type of the argument with the type of the parameter, based on the definition of the type alias:
If however, I wanted to hide the contents of the type alias, but only expose its signature, I'd be out of luck. In other languages you can have "opaque" or "abstract" type aliases that don't reduce definitionally outside the module where they were defined. Granted, in writing this now, you could use a "newtype" struct for this, and that probably works better with traits, but yeah... I think I recall running into other weirdness related to this stuff but can't remember off the top of my head.
I think it's more a reflection of how Rust evolved, and the techniques and approaches known and understood at the time and the strangeness budget they were (understandably) willing to take on at the time as opposed to something inherent. And also sometimes having separate, complicated features for similar things (as opposed to simple, generalised features that compose powerfully) can be useful pedagogically as well.
At any rate, this is something I'm personally interested in based on my experience working with Rust over the last decade, and so that's why it appears so high up on my list. Often you really do want sub-languages for different purposes, but managing how they interact and work together, what is the same and what is different, and how that impacts usability is interesting (and difficult) part. I feel like it should be possible to do this, but it's going to take some work and there's still lots of unknowns.
In technical terms, I'm interested in dependently typed module systems, multistage programming[1], graded modal type theory[2], elaborator reflection, and two level type theory[3]. These all sound pretty intimidating, but you can actually see glimmers of some of this stuff in how Zig handles type parameters and modules, for example, something that most programmers really like the first time they see it!
I do feel like there is the core of a simple, flexible, powerful systems language out there... but finding it, and making it approachable while maintaining a solid footing in the theory and being sensitive to the practical demands of systems programming is a nontrivial task, and many people will be understandably skeptical that this is even a good direction to pursue. Thankfully the barrier to entry for programming language designers to implementing languages in this style has reduced significantly in just the last number of years[4], so I have hope that we might see some interesting stuff in the coming decade or so. In the meantime we have Rust as well, which is still an excellent language. I'm just one of those people who's never content with the status quo, always wishing we can push the state of the art further. This is why I got excited by Rust in the first place! :)
I think you share a lot of my interests on the theory side of things. I also share your belief that those areas probably can allow for the development of the core of systems level programming language. Of course, I tend to find that graded, or the more general contextual modal type theory subsumes multi-staged, two level and grade modal theories. I also think a broad spectrum dependently typed language (with modal enforcement of computational irrelevance) can take care of dependent modules.
I think you are also spot on about Rust having a strangeness budget and that could be responsible for the syntactic state of the language as it exists today. I have a much higher tolerance for non-conventional syntax so almost all of my type theory implementation and PL work has been outside the normal syntactic bounds for the last 2 years. I doubt I ever produce a language that is public, let alone a language that is used by any portion of the software engineering field. But my belief is that this arena is fertile ground for a more fundamental core, like you mentioned.
As an aside, I happened to stumble upon Andras’ video presentations on YouTube on Saturday and flagged them to watch and bookmarked the repo for them earlier today. So bravo on linking what look to be really nice resources for this area of work.
> This is a thought I've often had myself. The name `unsafe` is not wrong, per-se, but it can sometimes have the wrong connotation
Yeah, this is one of the many things on this list that isn't a new idea, see this RFC from June 2014: https://github.com/rust-lang/rfcs/pull/117. I believe D has a `@trusted` attribute at the function level that serves a similar purpose.
I don't really use this site any more, but thought I'd just pop in to remind people that these are my personal thoughts from last year... I think there are some things I would add or change now and as others have noted, it's ok to disagree with me!
Many of the things I listed are not new, and there's been plenty of difficult discussions about many of them over the years, and are being worked on or postponed, or rejected for various good reasons (I could have done a better job at citing stuff in this gist). Managing a living language is difficult and challenging task, and many compromises need to be made. I think the Rust community is doing a great job considering all the challenges.
That said, I'd love to see more language designers consider the possible space of memory-safe by default systems languages, learning from what Rust can teach us, and bringing on board ideas from other places, like the newer systems languages and developments in dependent types, sub-structural type systems, etc. There's still so much more to explore, and still lots that can be done to improve in Rust itself.
I think there's actually a serious point here. As is so often the case, we should be unifying our efforts to solve common, pressing problems, not fragmenting our efforts over things that matter far less. Specifically, I think those of us that care about reliability and efficiency should unite behind Rust to provide a compelling replacement for C and C++ on the one hand, and (for some applications) higher-level but less efficient languages on the other. Rust is certainly not perfect, but if we succeed at making it a popular language with great libraries covering many application domains, it'll be better than what we have now.
It's pretty obvious that "Le Coq Sportif" is part of a non-english brand name. Coq not so much, especially out of context - eg. people overhearing professional conversations about the theorem prover, or when trying to introduce it to new audiences. I'll accept it was a tit-for-tat joke back in the day (re. 'bit'), but the original namers should have foreseen this day coming. It's branding 101 to do your research and avoid these issues.
They are differently powerful. Rust's macros can let you extend the syntax and do context-free code generation, where as C++ can let you to type-directed code generation. You can do the latter in Rust using trait dispatch, but it's more awkward and less expressive than what C++ has.
Yeah, would really love to see a static type system that tackled this directly - ie. handling versioned nodes in a cluster and ensuring deployments happen safety. I think it would be possible, but it would require some careful thought and design.
From what I see it's the dismissive way it was posed, with little curiosity about the real challenges. Similar to the 'oh I could build that in a weekend' style comments that are pretty exhausting for creators to have to deal with.
This submission is literally about why people aren't using some Rust framework. I add my two cents as to why that might be and then that gets called toxic and dismissive.
Seems like many people here aren't actually willing to engage in a discussion. I guess this submission is basically just native advertisement for the framework in question.
One limitation is privacy and abstraction. You can hide implementation details with most ML module systems - eg. hiding the underlying type of `Node`. You can also make local definitions in the module private. It's pretty challenging to get this stuff right - there's lots of research about it.
Also, as noted in other comments, Zig's type parameters are also dynamically typed. This leads to implementation details leaking out. This is not an issue in OCaml and other ML-style languages.
As a bit of a nit-pick, it's not _that_ new - see languages like ML, SML, OCaml, Miranda, Haskell, Coq, etc. that combined the notion of types from programming languages and types from mathematics. It's more that it's only recently that _industry_ has been learning about it.
That said, I definitely think you're right to point that this is a new thing for industry, and not just a swing back to the idea of types that were previously mainstream in industry. I'm excited too!
> What is definitional equality? What does an abstract type alias look like?
Sorry, type theory lingo. Definitional equality means (in the way I was using it - there's some subtlety) that when comparing two things, you look at the definitions, potentially performing some computations to simplify things down. For example, if I had:
Then I can supply a `y: Pair<String, i32>` to `foo` from another module and everything will be ok, because Rust computes the underlying type when comparing the type of the argument with the type of the parameter, based on the definition of the type alias: If however, I wanted to hide the contents of the type alias, but only expose its signature, I'd be out of luck. In other languages you can have "opaque" or "abstract" type aliases that don't reduce definitionally outside the module where they were defined. Granted, in writing this now, you could use a "newtype" struct for this, and that probably works better with traits, but yeah... I think I recall running into other weirdness related to this stuff but can't remember off the top of my head.