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…
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…
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…
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…
> 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…
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…
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…
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…
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…
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,…
> 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…
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…
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…
> given that there isn’t even any clean way to specify interface expected by C++ template, all you have is type traits Concepts?
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…
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…
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…
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…
> 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…
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…
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…
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…
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…
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,…
> 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…
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…
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…
> given that there isn’t even any clean way to specify interface expected by C++ template, all you have is type traits Concepts?