bjz_

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:

    use stuff::Pair;

    fn weird(pair: Pair<i32, String>) {
        dbg!(stuff::foo(pair))  // Rust checks: Pair<i32, String> == Id<(i32, String)>
    }

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.

Hey, funny to see this old thing pop up here!

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.

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.

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!

I'm sad it's not!

Yeah, it's not an uncommon to feel this way, especially if you've not learned the humanities formally. Pretty much the first thing I learned in art theory at university was how much art depends on influence and appropriation, and that it's important to accept and embrace this. It was a hard lesson to learn as a young person striving to be original, but it's served me really well.

Even as I now move into programming, computer science, and industrial programming language research, I'm still grateful for that small amount of art theory I did at university. You don't need to try to be original - rather it's important to seek wide and varied influences, develop your sense of taste, and from that will flow seemingly unique and varied insights.

I think he was the one to ask Phil Wadler to help out on the Featherweight Go formalization work.