HN user
Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).
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.
Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example.
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.
Alternatively, the Writer can be replaced with "IO", then the messages would be printed during the processing.
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.
New mainstream languages are rarer than new better (in some way that can be favorable) languages.
Perhaps together with Agda (compiles to Haskell, has FFI to it, is more higher-level), some not-pure ML, and maybe Rust or ATS?
Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.
We could make explicit effect (context, error) declarations for public functions and inferred for private functions. Explicit enumeration of possible exceptions is required for stable APIs anyway.
against the principles behind statically-typed languages, which all hate implicit things
But many statically typed languages allow throwing exceptions of any type. Contexts can be similar: "try catch" becomes "with value", "throw" becomes "get".
VS Code support for Common Lisp is lacking. Alive extension is relatively recent and is a solo effort and thus has significant bugs and is not as feature packed as Vim/Emacs alternatives. For example, it doesn't provide structural editing. It's interaction with sbcl cache seemingly broke my project a few times.
Regarding pattern-matching and enum types, I can see why a C++ programmer is impressed with such constructs, but it's really underwhelming for an OCaml/Haskell programmer.
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.
Bevy has support for dynamically described components and systems. Their main use-case is scripting language support. Can't agree that they insist on single language approach.
Lack of access to the C libraries.
Isn't CFFI enough for that?
There is nothing compelling about the language to people who aren't already Lisp people.
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.
I would recommend trying Lean4 because I think it is better suited to programming. Lean has Rust-like toolchain manager; a build system (cf. `.agda-lib`); much more developed tactics (including `termination_by`/`decreasing_by`); more libraries (mathlib, and some experimental programming-oriented libraries for sockets, web, games, unicode...); common use of typeclasses in stdlib/mathlib; `unsafe` per declaration (cf. per module in Agda); sound opaque functions (which must have a nonempty return type) used for `partial` and ffi; "unchained" do-notation (early `return`, imperative loops with `break`/`continue`, `let mut`); easier (more powerful?) metaprogramming and syntax extensions. And in Agda you can't even use Haskell's type constructors with type classes (ex. monad polymorphic fns, and that makes it more difficult to make bindings to Hs libs, than to C libs in Lean).
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.
How can the audience of a general-purpose programming language not be "programmers"?
Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself.
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).
Big:
* 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)
that can accept any number of functions
So, `(a -> b) -> (b -> c) -> (c -> d) -> ... -> a -> z`.
I've seen an advice to not use equality on floats, and instead use something like |x-y|<e. Probably translates to constructive reals as it needs to compute only some part of the numbers.
Reversing bytes sounds like reversing their bit orders to me.
I kept waiting for more examples for why we need FP
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?).
Small core is easier to verify.
Dependent types are types that depend on values, possibly runtime values. In C# types can only depend on other types when using generics: List<T> depends on T. In C++ there is std::array<T, n> (array with length encoded in type), where n must be known in compile time.
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) {...}given that there isn’t even any clean way to specify interface expected by C++ template, all you have is type traits
Concepts?
I enjoy writing code with Agda. I like writing APIs that can't be used incorrectly and dependent types are so much more powerful that anything I knew before. Also unicode/custom mixfix operators (if_then_else_) are fun to use. Other languages I've seen just can't offer these things. Probably it is not the best choice to create something you want to run as its ecosystem is not quite developed though, but I also like to reinvent the wheel..
which have a runtime costs
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...
an ultimate language that is as expressive as Idris and as efficient as Rust, and is thus essentially perfect.
Are both Idris's expressiveness and Rust's efficiency (given stronger guarantees) perfect? Aren't theese languages really complex both to learn and to write? There are poblems without a solution, perfect and unique to all of them.