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.

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! :)

[1]: https://github.com/metaocaml/metaocaml-bibliography

[2]: https://granule-project.github.io/

[3]: https://github.com/AndrasKovacs/staged

[4]: https://github.com/AndrasKovacs/elaboration-zoo/

Thanks for reminding people!

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

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!

Glamorous Toolkit[0] is pretty neat! More of something designed for making software on top of, but it's a pretty cool example of what's possible.

[0]: https://gtoolkit.com/

Relevant wikipedia article: https://en.wikipedia.org/wiki/Dimensionless_quantity

Radians and degrees are both ratios where the units cancel out - ie. m/m. The point that is made is that adding degrees to radians without any conversions is technically fine from a dimensional analysis perspective, but it's often a bug in programming that we might want to prevent.

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.

I don't think these kinds of long term, far-seeing projects would survive in the life-and-death contest of startups and the private sector either.

I dunno what the alternative is, other than political activism, pushing parties to support progressive tax policies, and educating our peers and family members. It's not only research on the line here.

Ahh cool - had some similar questions here: https://news.ycombinator.com/item?id=23460980 - mainly, how much manual switching do you have to do? Or is it seamless, depending on what project directory your in? I think I tried the local switches in the past and got really confused when switching projects and everything broke, thinking 'wasn't all this meant to prevent this?'.

Oh that's nice to hear! Some questions:

Do you have to run this command manually, and does it mutate the shell state? That's one thing that frustrated me with opam in the past as well. I couldn't just jump into a directory and build a thing, then switch to another project directory - there was a lot of manual switching and unswitching of packages if I recall correct?

Is it possible to install multiple tools globally using opam that use disjoint library versions? Like, I might want to install Abella and Coq side-by-side, but they might have conflicting version requirements. I think I was super excited about opam 2, then tried installing one thing, only to have it break again when I installed something else.

Is it possible to have multiple versions of the same libray in the same project, or does the constraint solver need to find a single solution for each library? [1]

[1] https://news.ycombinator.com/item?id=23454917

Yeah, it's really great to see the progress there. However, afaik, it still doesn't freeze packages by default, or let you have multiple packages of the same version in a dependency tree[1]. The former can be worked around, but it's annoying that it's not the default. The latter is more frustrating however!

[1] https://news.ycombinator.com/item?id=23454711

> OCaml's is also excellent but not immediately obvious (their docs have improved a lot)

Interesting! The last time I tried OPAM, it actually seemed more frustrating than Cabal! Maybe it's improved? Last time I tried OPAM it would install packages globally by default, and avoiding that was a confusing process, when that should be the default behavior.

Cargo (while not perfect) has really nice defaults out of the box - ie. it generates a lockfile by default, scopes packages locally to individual projects, and lets you use more than one package of the same version in the same project.

Really hoping OCaml and Haskell can improve their package management story - they are getting there, but it still holds me back from really using them on a daily basis.

What happens if you are building a library that is published to Hackage?

I think Rust gives the symbols unique hashes for each crate version to avoid this. See this answer on Stack Overflow for more information: https://stackoverflow.com/a/51722134 - not sure if there is a better reference document though.

You sometimes get weird errors like expected `A` but found `A` in the unusual event that you actually run into this, but this is probably something that could be fixed.

The new improvements to Cabal have been super nice of late, but one thing I _really_ wish Cabal would do is allow for multiple versions of a library to be used in the same project. Having to satisfy a single library version is incredibly frustrating, and the solver errors are incredibly confusing. This is especially confusing when it complains about a library deep in your dependency graph being in conflict.

Ultimately the failure mode means that you can't build your package and are blocked until a fix is made upstream, where as with a package manager like Cargo you can still build your project. The downside is that you have a duplicate in your dependency graph - but this can be fixed upstream in an asynchronous fashion.

Also Mozilla Research

Then why not charge people to do those kinds of jobs more? Or encourage companies to make the jobs less unpleasant and more fulfilling? A UBI means that workers have more power to be picky about where they work, which puts pressure on companies to improve conditions.

I've been trying to learn enough about this problem to be of use in implementing this (playing around with my own language implementations). It seems like a real challenge might be around ensuring that your programs have extraneous 'type stuff' removed in the compiled program. Part of this could be helped with a nice way of doing proof irrelevance (eg. something like Quantitative Type Theory) and another could be multistage programming (eg. something like MetaML or MetaOCaml). The latter would make it much easier to do a more general form of Rust's monomorphisation of type parameters. You'd then may also want some sort of uniqueness typing and borrowing, but I have no idea where to get started on that! And you also don't want to drown in a mountain of annotations!

As an Australian who has privacy concerns their government's COVIDSafe app (see https://github.com/vteague/contactTracing), and hence not installing it, I'm really thankful that Apple and Google are pushing this model of contact tracing. We still don't know if digital contact tracing is effective in practice, but it's still important to try, but we can do this in a way that avoids giving governments with worrying authoritarian tendencies another tool.

Same on Firefox!

I've definitely found Elm worth playing around with - it's a really beautifully designed language with some really cool library design thrown in that I wish more people would learn from. That said I'd _really_ recommend steering clear of it for important stuff due to the issues described in this article.

This was a really great video that goes into lots of what most of the crowd sourced ventilators miss in their designs. Worth the watch if you want to know what's important in ventilator design when it comes to not doing injuries to patients.