creata

51 ms·

661.
by creata 5y ago
> Sadly even worse than clojure's which is already not great. I thought Clojure's immutable collections were generally considered good. What else would you consider "great"? Edit: or was that a complaint about the qua
662.
by creata 5y ago
> I don't know enough about rust Rust allows cyclic dependencies between modules within a single crate, but not between crates.
663.
by creata 5y ago
In some incredibly pedantic sense, sure. But the difference is that every computer comes with what a human needs to read a CSV file. That's not true of an SQLite database.
664.
by creata 5y ago
On iOS, there's AdGuard if you want to use Safari, and Firefox Focus if you don't.
665.
by creata 5y ago
See also: https://medium.com/@veedrac/why-unary-is-the-best-number-sys...
666.
Diffractor.jl – Next Generation Automatic Differentiation(github.com)
3 points by creata 5y ago|0 comments
667.
by creata 5y ago
> I use https://lib.rs/cap which self-imposes memory limit on the process. How do you choose that limit?
668.
by creata 5y ago
Agreed: I meant that there were superficial similarities, not merely superficial similarities. Here's the original paper (I think?) on self types; maybe there's an obvious link in there. https://homepage.divms.uiowa.e
669.
by creata 5y ago
I think they're referring to the least fixpoint operator μ, whose interface you can find in section 15.2.1 of PFPL.[0] The idea and consequences superficially seem to be very similar. [0]: https://www.cs.cmu.edu/~rwh&#x
670.
by creata 5y ago
> Even though Idris is marketed for “practical programming” it doesn’t have partial functions!! Both Idris and Agda have partial functions. Idris uses a keyword "partial", and Agda uses a pragma "NON_TERMINATING".
671.
by creata 5y ago
> Keep in mind that cubical type theories are somewhat complex (in sheer amount of code), And in computational efficiency, no? I think making an efficient implementation of a cubical type theory is still an ongoing effort.
672.
by creata 5y ago
It looks[0][1] like they do want to be an OS comes with your computer, which is pretty exciting. [0]: https://news.ycombinator.com/item?id=28133146 [1]: https://au.starlabs.systems/pages/laptops
673.
by creata 5y ago
Funnily enough, that variable arity is mentioned in the article as a nuisance: > ... wincing slightly at the lambda notation you need to avoid running afoul of JavaScript’s variadic Math.max()...
674.
by creata 5y ago
So Apple might end up with thumbnails of the "end-to-end encrypted" content I send, and you think that it counts as end-to-end encryption even if (a low-resolution version of) my messages can end up in a third party's hands.
675.
by creata 5y ago
The "end" will happily send information to Apple such that under certain circumstances (that Apple and various organizations get to decide) low-resolution versions of the "end-to-end encrypted" messages can be obtained.
676.
by creata 5y ago
> Programming is significantly easier... because of things like syntax checking and compiler/interpreter errors. People[0][1] are using theorem provers to help teach students the general structure of a proof. And this is a bit of a
677.
by creata 5y ago
Sure, this particular move strictly improves privacy. But it has some terrible implications: 1. That there are circumstances in which it's okay to design an electronic device to work against its owner: an accusation is all it takes to
678.
Half a year of the Liquid Tensor Experiment: developments(xenaproject.wordpress.com)
1 points by creata 5y ago|0 comments
679.
by creata 5y ago
I think the relevant topology on the space of binary streams is the Cantor space.[0] It's compact, and can be seen as a subspace of the real line.[1] The fact that it's compact is equivalent to a principle called the fan theorem
680.
Representations of Uncomputable and Uncountable Sets (2008)(math.andrej.com)
45 points by creata 5y ago|9 comments
681.
by creata 5y ago
Imo, the advantage of "Haskell's approach" is that it's always obvious when you can and can't use imperative code, and the type system enforces it. I think this is important in many contexts, like STM[1] or Facebook
682.
by creata 5y ago
True, but imo Haskell I/O was less than pretty before monadic IO came along: https://stackoverflow.com/a/17004448
683.
by creata 5y ago
Sure, I/O in Rust is a little easier because it's not wrapped up in an abstract type, but in exchange, Rust needs Try, async/.await and const-fn to solve just a few of the issues that monads solve in more generality. I don&#x
684.
by creata 5y ago
How is intuitionistic type theory a "better" foundation? As a simple example, where can I find a statement of Brouwer's fixpoint theorem in an intuitionistic type theory, and how is it better stated than its classical counter
685.
by creata 5y ago
> Instead, coercions are used to emulate some of the advantages of subtyping. Maybe I missed it in the article, but what does subtyping give you that coercions don't?
686.
by creata 5y ago
Sure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could eva
687.
by creata 5y ago
> The issues are fixed and life goes on. Some bugs can't be fixed: once you've leaked millions of people's personal information, you can't really take it back. The "stakes of building it wrong" are very high
688.
by creata 5y ago
This is way off topic, but that's funny, because it's the other way around for me: I can install Agda with a `pacman -S agda`, but I'd need to go through the AUR for Lean.
689.
by creata 5y ago
> constructive math can be very convenient for proving stuff about programs/computations. How? I can see how proving properties of programs is a place where constructivism won't get in the way, but do you have an example of whe
690.
by creata 5y ago
And you can put %B in your status line to show the Unicode value of what's under your cursor.

More ›