Viewing profile — siknad

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 datase…

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…

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 i…

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 sta…

> 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 b…

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 altern…

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

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 co…

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 tacti…

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 programm…

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 toward…

Big: * tactics (proof scripts are a lot easier than manual proving) * syntax extensibility (Racket-like, supports custom elaboration/delaboration) * mathlib (library of formalized …

> 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 nu…

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, g…

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 depends on T. In C++ there is std::ar…

template concept has_foo = requires(T x){ { x.foo } -> std::same_as ; }; template int get_foo(T x){...} // or template requires has_foo void f(T x){...} // or even void f(has_foo a…