siknad

5 ms·

1.
by siknad 2mo ago
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
2.
by siknad 3mo ago
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 us
3.
by siknad 1y ago
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 b
4.
by siknad 1y ago
New mainstream languages are rarer than new better (in some way that can be favorable) languages.
5.
by siknad 2y ago
Perhaps together with Agda (compiles to Haskell, has FFI to it, is more higher-level), some not-pure ML, and maybe Rust or ATS?
6.
by siknad 2y ago
Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.
7.
by siknad 2y ago
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.
8.
by siknad 2y ago
> 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
9.
by siknad 2y ago
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
10.
by siknad 2y ago
> 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
11.
by siknad 2y ago
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.
12.
by siknad 3y ago
> Lack of access to the C libraries. Isn't CFFI enough for that?
13.
by siknad 3y ago
> 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&#
14.
by siknad 3y ago
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 l
15.
by siknad 3y ago
How can the audience of a general-purpose programming language not be "programmers"?
16.
by siknad 3y ago
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 ru
17.
by siknad 3y ago
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 i
18.
by siknad 3y 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 hav
19.
by siknad 4y ago
> that can accept any number of functions So, `(a -> b) -> (b -> c) -> (c -> d) -> ... -> a -> z`.
20.
by siknad 4y ago
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.
21.
by siknad 4y ago
Reversing bytes sounds like reversing their bit orders to me.
22.
by siknad 4y ago
> 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 locati
23.
by siknad 4y ago
Small core is easier to verify.
24.
by siknad 4y ago
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)
25.
by siknad 4y ago
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
26.
by siknad 4y ago
> given that there isn’t even any clean way to specify interface expected by C++ template, all you have is type traits Concepts?
27.
by siknad 5y ago
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. Oth
28.
by siknad 5y ago
> 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 t
29.
by siknad 5y ago
> 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 lang