Tarean · HackerTrans

15 hari yang laludiscuss

Java can also have 15+ minute cold compiles on large projects if you kill all caches. It's less bad on smaller codebases because you don't have to recompile dependencies if you target a bytecode vm, but if you always gate feedback on a cold compile in a fresh VM you just aren't gonna beat an interpreted language

But I'd look at people a bit oddly if they said: 'We didn't want to set up CI caching and compiled languages took 30 minutes per run so we changed our entire codebase to python'.

Maybe it makes sense for them, and caching across dynamically spawned VM's is admittedly a harder problem which most build systems aren't great at, but still. I can easily believe that getting build caching to be reliable would be a lot of work, but is it more work than a full rewrite of a significant codebase?

Tarean

7 bulan yang laludiscuss

Having pair programmed over some truly awful and locked down connections before, dropped frames are infinitely better than blurred frames which make text unreadable whenever the mouse is moved. But 40mbps seems an awful lot for 1080p 60fps.

Temporal SVC (reduce framerate if bandwidth constrained) is pretty widely supported by now, right? Though maybe not for H.264, so it probably would have scaled nicely but only on Webrtc?

Tarean

7 bulan yang laludiscuss

Intellij also has structural search and replace, where you can do full subgraph isomorphism search in the code and with patterns like

    $x$.foo($args$)

Where you add filters like x's type is a subclass of some class, and args stands for 0-n arguments.

You can also access the full intellij API via groovy scripts in the filters or when computing replacement variables, if you really want.

Though most of the time built in refactors like 'extract to _' or 'move to' or 'inline' or 'change type signature' or 'find duplicates' are enough.

Tarean

9 bulan yang laludiscuss

I think WasmGC is very hard to make work with laziness. A lazy value is always a closure on the heap.

If an expression might be unused, throw a closure which computes it on the heap

If the value is actually needed, invoke the closure. Optionally replace the closure with a black hole. A black hole is just a closure which pauses any thread which calls it, to be resumed once the first thread finishes with the expression

Once finished, replace with a closure which immediately returns the computation result. (Or often save the indirection because most concrete values also act as closures which immediately returns themselves using info table pointers trickery)

Anyway, iirc WasmGC wants very rigid types without dynamic type changes. Extra indirections could fix that, Oor maybe defunctionalizing thunks into a tagged union, but both sound expensive. Especially without being able to hook into the tracing step for indirection removal.

Also, Haskell supports finalizers so WasmGC would need that as well.

Tarean

9 bulan yang laludiscuss

Sometimes keeping a fixed shape for the variable context across the computation can make it easier to reason about invariants, though.

Like, if you have a constraint is_even(x) that's really easy to check in your head with some informal Floyd-Hoare logic.

And it scales to extracting code into helper functions and multiple variables. If you must track which set of variables form one context x1+y1, x2+y2, etc I find it much harder to check the invariants in my head.

These 'fixed state shape' situations are where I'd grab a state monad in Haskell and start thinking top-down in terms of actions+invariants.

Tarean

9 bulan yang laludiscuss

I'm pretty sure recall was specifically a selling point for laptops with ai chips which could do the processing locally and reasonably efficiently?

Though storing the data locally still could make getting compromised by a targeted attack more dangerous.

Tarean

11 bulan yang laludiscuss

Interval arithmetic is only a constant factor slower but may simplify at every step. For every operation over numbers there is a unique most precise equivalent op over intervals, because there's a Galois connection. But just because there is a most precise way to represent a set of numbers as an interval doesn't mean the representation is precise.

A computation graph which gets sampled like here is much slower but can be accurate. You don't need an abstract domain which loses precision at every step.

Tarean

tahun laludiscuss

In my head the two dimensions are tail Vs non-tail jumps, and explicit Vs implicit scope passing.

The most interesting case is implicit scope+non-tail recursion, usually this requires you to capture the variable context in mutable objects/monads/effects or similar.

This explicit capturing is neat because you still have consistent shapes for your state to define invariants over, but it's easier to decompose the logic and ignore parts of the context which are irrelevant. It lets you split problems into domain specific languages, each of which has a set of (maybe overlapping) contexts, and ideally each of which can be proven in isolation.

Also, the control flow of loops is a very restricted case of even tail jumps. Tail recursion has arbitrary jumps between basic blocks and loops are properly nested basic blocks. Even with labeled breaks, efficiently simulating arbitrary tail recursion without goto is tough. Induction proofs/data flow analysis/abstract interpretation don't care, but I'm not sure it makes proofs easier.

Tarean

2 tahun yang laludiscuss

Forgot to mention: In the twee style, the int for the function id contains metadata (is it a unification variable or constant name? how many args does it take?). That way f1(f3(f5(), f7())) would be serialised as something like [1,3,5,7], without even references to other offsets

Tarean

2 tahun yang laludiscuss

Twee (an equational theorem prover in Haskell used by quickspec) has an interesting take on this. Terms are slices of arrays, but you get a normal interface including pattern matching via synonyms. It can also be nice to use phantom types of your references (array offsets), so if you project them into flat view types you can do so type safely

Requires the language to have something equivalent to pattern synonyms to be as invisible as twee, though.

In twee a TermList is a slice of a bytearray (two ints for offset/length plus a pointer).

And a term is an int for the function symbol and an unpacked TermList for the arguments.

The pattern match synonyms load a flat representation from the array into a view type, and the allocation of the view type cancels out with the pattern matching so everything remains allocation free.

https://hackage.haskell.org/package/twee-lib-2.4.2/docs/Twee...

Tarean

2 tahun yang laludiscuss

As of python 3.6 you can nest fstrings. Not all formatters and highlighters have caught up, though.

Which is fun, because correct highlighting depends on language version. Haskell has similar problems where different compiler flags require different parsers. Close enough is sufficient for syntax highlighting, though.

Python is also a bit weird because it calls the format methods, so objects can intercept and react to the format specifiers in the f-string while being formatted.

Tarean

2 tahun yang laludiscuss

This behaviour was introduced in 3.6 (and made part of the spec in 3.7 iirc)

From the python 3.6 change log:

New dict implementation¶ The dict type now uses a “compact” representation based on a proposal by Raymond Hettinger which was first implemented by PyPy. The memory usage of the new dict() is between 20% and 25% smaller compared to Python 3.5.

The order-preserving aspect of this new implementation is considered an implementation detail and should not be relied upon (this may change in the future, but it is desired to have this new dict implementation in the language for a few releases before changing the language spec to mandate order-preserving semantics for all current and future Python implementations; this also helps preserve backwards-compatibility with older versions of the language where random iteration order is still in effect, e.g. Python 3.5). (Contributed by INADA Naoki in bpo-27350. Idea originally suggested by Raymond Hettinger.)

https://docs.python.org/3.6/whatsnew/3.6.html#new-dict-imple...

Tarean

2 tahun yang laludiscuss

Either hackernews or autocorrect ate the p, it was supposed to be \p{L} which is a unicode character class.

As the other comment mentioned pcre-compatible Regex are a standard, though the pcre spec isn't super readable. There are some projects that have more readable docs like mariadb and PHP, but it doesn't really make sense to repeat the spec in library docs https://www.php.net/manual/en/regexp.reference.unicode.php

There are libraries for pcre2 or gnu regex syntax with the same API if you prefer those

Tarean

2 tahun yang laludiscuss

For Regex I like lens-regex-pcre

    > import Control.Regex.Lens.Text
    > "Foo, bar" ^.. [regex|\p{L}+|] . match
    ["Foo", "bar"]
    > "Foo, bar" & [regex|\p{L}+|] . ix 1 . match %~ T.intersperse '-' . T.toUpper
    "Foo, B-A-R"

For web requests wreq has a nice interface. The openssl bindings come from a different library so it does need an extra config line, the wreq docs have this example:

    import OpenSSL.Session (context)
    import Network.HTTP.Client.OpenSSL

    let opts = defaults & manager .~ Left (opensslManagerSettings context)
    withOpenSSL $
      getWith opts "https://httpbin.org/get"

There are native Haskell tls implementations that you could plug into the manager config. But openssl is probably the more mature option.

Tarean

2 tahun yang laludiscuss

Both strategies start from roots (e.g. the stack) and then transitively chase pointers. Any memory reachable this way is live.

To do this chasing precisely you need some metadata, saying which fields are pointers vs other data like ints. For OOP languages this metadata is stored with the vtables for objects. For the stack you need similar metadata, at the very least how many pointers there are if you put them first in the stackframe.

Not having this metadata and conservatively treating random ints as pointers isn't always catastrophic, but it has some drawbacks. Two big ones:

- a moving GC is tough, you have to update pointers after moving an object but can't risk updating random ints that happen to have that value

- You do more work during GC chasing random non-pointers, and free less memory meaning more GC runs

Generating ths precise GC metadata for stackframes is sort-of easy.You need specific Safe-Points where all data is at known locations for the GC to work anyway, usually by spilling resgisters to the stack. These GC checkpoints usually coincide with heap allocation, which is why long non-allocating loops can block stop-the-world GC and send other threads into a spin-lock in many GC implementations

Maybe a non-precise GC could treat registers as possible pointers and skip spilling to the stack for Safe-Points? There are alternatives to spilling like a precise stack-map for each program instruction (so every instruction is a safe point), but those are expensive to process. Usually only used for debugging or exception handling, not something frequent like GC

Tarean

2 tahun yang laludiscuss

But that stores all elements into memory?

Tarean

2 tahun yang laludiscuss

Love this algorithm. It feels like magic, and then it feels obvious and basically like binary search.

Similar to the algorithm to parallelize the merge step of merge sort. Split the two sorted sequences into four sequences so that `merge(left[0:leftSplit], right[0:rightSplit])+merge(left[leftSplit:], right[rightSplit:])` is sorted. leftSplit+rightSplit should be halve the total length, and the elements in the left partition must be <= the elements in the right partition.

Seems impossible, and then you think about it and it's just binary search.

Tarean

2 tahun yang laludiscuss

To me the big winning is that you don't have to memoize transitively. Occasionally someone asks me for help to optimize some react code, and then the dependency array contains some object/callback that has a dependency which has a dependency which wasn't memoized.

Tarean

2 tahun yang laludiscuss

The big problem is that

- memoization sometimes crucial for performance.

- passing objects and functions around is common.

- you cannot compare objects and functions for semantic equality

If you wrote larger react apps you almost certainly had to useCallback at some point so that memoization worked, the compiler fixes that.

Whenever you construct an object or function the react compiler memoizes on their free variables so pointer equality is sufficient.

Though I do think the compiler caches too aggressively, even if there are no free variables and hoisting is sufficient or escape analysis shows it is unnecessary for semantics.

Tarean

2 tahun yang laludiscuss

Computer-Checked proofs are one area where ai could be really useful fairly soon. Though it may be closer to neural networks in chess engines than full llm's.

You already use tons of solvers because proving everything by hand is mind numbingly tedious and time consuming, but tactics/solvers really struggle if you throw too many theorems and lemmas at them. Neural nets as search machines to pattern match relevant lemmas fit perfectly. Similarly induction and higher order unification are full-on code synthesis where brute-force iterating over all possible syntax trees is really inefficient.

And solvers do a backtracking solve anyway, so if the ai returns 95% irrelevant lemmas it doesn't matter. Still would be a dramatic improvement over manually searching for them.

Though I'm not convinced that computer checked proofs are necessarily good for communication. There are reasons beside page-count that proofs for human consumption are high-level and gloss over details.

comments