siknad

Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.

IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.

The computation code becomes effectful, but the effects are visible in types and are limited by them, and effects can be implemented both with pure and impure code (e.g. using another effect).

The effect can also be abstract, making the processing code kinda pure.

In a language with unrestricted side effects you can do the same by passing a Writer object to the function. In pure languages the difference is that the object can't be changed observably. So instead its operations return a new one. Conceptually IO is the same with the object being "world", so computation of type "IO Int" is "World -> (World, Int)". Obviously, the actual IO type is opaque to prevent non-linear use of the world (or you can make the world cloneable). In an impure language you can also perform side-effects, it is similar to having a global singleton effect. A pure language doesn't have that, and requires explicit passing.

But many statically typed languages allow throwing exceptions of any type. Contexts can be similar: "try catch" becomes "with value", "throw" becomes "get".

What's underwhelming about Rust's enums and pattern matching? Lacking indexed types/GADTs?

> I even wonder if it's necessarily a better choice than modern C++ for someone starting a new project.

The same enums, matching and other language features that aren't related to safety and yet allow the developer to write less boilerplate, alleviate the need to remember implementation details of the code used. And as someone said here, safety is not only about security vulnerabilities.

Not once I had problems with the borrow checker. Maybe it depends on the domain, requirements or project size. While I haven't finished any game in Rust, I am writing one (as a hobby/learning) and I try to avoid unnecessary and noticeable performance hits. Though I am working under the assumption that some runtime checks that are present in safe Rust and not in C++ are a net positive due to easier debugging. I'm not convinced that "unsafe" code and asm are necessary in modern gamedev.

Isn't CFFI enough for that?

CL is expression based (like Rust, unlike other mainstream languages I've seen), has a concise macro system (more convenient than Rust's imo), has a GC (simpler to use than languages with manual memory management or RC-only), has a better developed ecosystem then some new languages (ex. automatic ffi generation; while buggy, tremendously helpful compared to writing bindings manually). And it's not pure as in Haskell. And it has type annotations that may be checked at runtime or improve performance. An implementation like SICL could make it viable to use it as a scripting language.

Any similar modern languages with better tooling/ecosystem? Perhaps Julia, haven't seen it yet.

There are features in Agda/Idris (and probably Coq, about which I sadly know almost nothing) that are absent from Lean and are useful when programming (coinduction, set omega, more powerful `mutual`, explicit multiplicity, cubical? etc), but I'd say the need for them is less common.

Now it has a RC GC and boxes everything >= 64 bits (including struct fields and IO/ST results), and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago).

[1] https://github.com/kmill/lean4-raytracer

* tactics (proof scripts are a lot easier than manual proving)

* syntax extensibility (Racket-like, supports custom elaboration/delaboration)

* mathlib (library of formalized math)

* tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code)

Small things I can remember:

* do-notation with early return and imperative loops

* easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)

So, `(a -> b) -> (b -> c) -> (c -> d) -> ... -> a -> z`.

Dependent types, allow a lot more type safety (ex. shader program type parametrized by description of its uniform variables, getting rid of `INVALID_OPERATION` on wrong uniform location/type).

> you can incorporate those features in imperative languages like Rust and Swift

Incorporating dependent types into imperative languages with unrestricted effects is hard (impossible?).

With full dependent types one can write generic types like std::array and use them with runtime parameters. In dependently-typed languages there are two main types: Sigma (dependent pair) and Pi (dependent function). Example of Sigma type in pseudo C#:

  (uint n, Array<int, n> a); // array of any size

  Array<T, (n + 1)> push(Type T, uint n, Array<T, n> a, T x) { ... }
  Array<int, 3> x = push(int, 2, [1, 2], 3); // [1, 2, 3]

A bit larger example:

  void Console.WriteLine(string format, params object[] args);

  WriteLine("{%int} {%bool}", ?); // ?'s type is an array with an int value and a boolean value.

  template<typename T>
  concept has_foo = requires(T x){
  { x.foo } -> std::same_as<int>;
  };

  template<has_foo T>
  int get_foo(T x){...}

  // or

  template<typename T>
  requires has_foo<T>
  void f(T x){...}

  // or even

  void f(has_foo auto x) {...}

Concepts?

As monad is just an interface, it doesn't necessary cause runtime costs. Identity is a monad too. Effects may not always require sacrificing performance, but as they can be used to implement exceptions they are not just free compile time annotations. Also the differences discussed there: https://www.reddit.com/r/haskell/comments/3nkv2a/why_dont_we...