edwardkmett

We get first-class cross-language FFI to truffled language implementations: Python, Ruby, R, Javascript with shared objects, which can JIT together. The idea is that fully fleshed out this would give Haskell a clean path to reach over to pytorch to run an AI model, take the answers, smash them through some statistical analysis using an obscure R library and send the result to d3.js to get pretty visualizations. Are we there yet? Hell no.

We get access to the java incubator vector API allowing us to JIT SIMD kernels for the target platform with less pain. Haskell has just been bad at high speed SIMD code since I found my way into the ecosystem, and it hasn't shown much sign of getting better. This lets me theoretically sidestep those issues.

Using Sulong for C/C++ FFI means we don't give up native cbits and host code, unlike old bad hard-to-use JVM language ports like JPython.

Future work could for instance make Natural number code use java deoptimization paths keeping it generally in unboxed ints until you finally need something too big through a given codepath. Again, just more paths to potentially make things faster or easier to use.

Without Truffle/Graal the limitations of the JVM are just too severe. It is an awkward runtime full of limitations. The lack of proper tail call optimization for instance would kill GHC-style evaluation performance, and has left a long list of functional language corpses in its wake that tried to make the JVM their home.

With the "Cadenza trick" I use to eliminate that we can have highly performant loops. Using assumptions lets it compile with the equivalent of GHC's single threaded runtime and then downgrade performance to the equivalent of the multi-threaded runtime when you first call a threading operation, so users don't have to pick, they just get the benefits. I, in turn, get headaches.

We get stuff that GHC just will never even try to get around to. CompressedOOPS give us 32 bit pointers on 64 bit platforms if the heap is < ~32GB. So about twice as much stuff can fit into cache especially in a language with as many pointers running around as ours compared to the normal Haskell runtime.

My goal is to keep pushing forward with the bits that this can do that GHC can't do, and to generally try to get to or maintain parity wherever possible for the things that GHC can do.

It also helps us tease apart where the line should be for GHC as a runtime system vs. GHC as a compiler. The former has been languishing behind comparatively, ever since Simon Marlow left GHC headquarters to go fight spam for Meta.

I wrote a blog post targeted at an insider audience to tease at something that was coming. It has since spread outside of that audience. There's no gatekeeping going on here, no secret enlightenment required, just a poorly drafted research note thrown over the fence to his peers to see if anybody else might be interested in his new favorite toy by a very busy person. I'm sorry.

Text is presented in a faux IBM VGA font, blue background, and in any of the non-terminal choices a subtle CRT grading/vignetting is applied if desired, but it is extended to full unicode including emoji with an optional stylization pass to make them feel more like the period editor experience. You can even switch display modes because most of the time I used Borland tools in my youth I'd run them in 80x50 mode.

My general intent is that the final installer will package both of them, just like Turbo Pascal bundled TP and TPC or Turbo C bundled TC and TCC.

In the original commenter's defense, I _did_ let the agents I have working on this get a more than a bit test harness crazy back when I was able to use GHC itself as a behavioral oracle. That worked fine through the initial build out, but then it rushed ahead with a broken CI due to misalignment in priorities, and then kept piling fixtures on top of fixtures and didn't properly track their cross-dependencies. My work on this in the last 48 hours has mostly been about getting that part under control and stable across my target platforms so I have better bedrock to build atop.

Now picking CBD for the compressed Core Binary Distribution format we use? That? That was gratuitous.

Talking about Java FFI invites you to say 'well then smart-ass how do you extend this Java class/interface over here with code written in your language' and frankly, that has never had a satisfying answer for any language that isn't Java.

But today you can pass Haskell Data.Text out through the FFI binding framework and it shows up on the other side as a valid TruffleString, in UTF-8 with zero copy semantics and if any Truffle language passes in a TruffleString that is UTF-8 encoded it gets unwrapped into Data.Text using the same.

That and some array support is pretty much enough to talk to everybody else.

Next?

Sounds like a very democratic, open source, do what you will solution to me.

We'd like to get some of the old logging bots moved over, etc.

We have some number of users who connect from tor, from matrix, or from webchat that simply can't move right now. These are things being looked at from the libera.chat side, but that work isn't done.

I very much value those users being able to continue to ask and get their questions answered.

That said, we used to have like 3-4 server ops lurking in the channel, and 15-16 channel ops that were active on the server. We just don't any more. This makes me rather concerned from a spam perspective.

On the other hand, there are < 80 people in the channel now, so perhaps spam is less of an issue now that we're a much smaller target.

That said, they have many of the elements of the solution. With monotonicity this starts to resemble the more recent work on Lasp, which is being used explicitly to tackle the domain you mention: (strong) eventual consistency: or Kuper's work on LVars, where she drops the idempotent condition fairly early on in the thesis to get closer to CmRDTs, but which then burdens reads in a way that makes them automatically monotone.

I started a project at https://github.com/ekmett/propagators which at least gets the basic execution of them right, and have been working on a larger project.

Now, Sussman and Radul manage propagation and track provenance through using an assumption-based truth management system. This unfortunately results in a 2^n blowup in space, but if you change the schema somewhat you can treat it more like enumerating solutions in SAT, where you get a blowup, but in time not space -- and as usual with SAT "it usually isn't that bad".

In any event, a lot of work out there overlaps with the propagators story:

Lindsay Kuper's work on LVars drops idempotence and doesn't deal with 'triggering on change' but gets a parallel computation with forking and writes to "lattice variables" and uses threshold reads to manage communication.

Sussman and Radul's work really needs the notion of the propagators themselves being monotone functions between the semilattices that they are working with. Unfortunately in neither the paper or Radul's thesis do they ever actually spell that out.

Once you do spell it out you get something like Christopher Meiklejohn's on LASP. Both he and Lindsay Kuper have been tackling the issue of composing CRDTs lately. Her notion of threshold reads works well here when it can be applied because such functions are automatically monotone, there is nothing to check.

On the other hand, we can view things like datalog as a propagator network. You have tables which accumulate information monotonically. You have IDB statements that execute joins between those lattice variables. Now this starts to show some of the differences. There we don't bother sending the entire lattice. In seminaive evaluation of datalog we send deltas. So it becomes interesting instead to walk back the notion of a lattice variable and to think instead of a commutative (possibly idempotent) monoid acting on an ordered set. Now your "update language" is the monoid, and we can think of this in terms of firing updates at a set and tracking what makes it through, and propagating _that_. I've been playing with various ways to get a closer analogue to datalog processing and to effectively track these partial triggers.

Another issue is that propagator networks as they are currently designed typically do too much work. Too many things are woken up and fired. We can mitigate that somewhat. Consider a propagator that adds two lifted numbers. We can also add a propagator backwards that does the subtraction, etc. This yields a (local) propagator for which if you tell me any 2 of the arguments, I can tell you the third.

A more efficient scheme would be to adopt a "two watched literal" scheme like a SAT solver. Pick two lattice variables that are still at _|_. When one of those is written to, check to see if you're down to 1 variable not at _|_. If so we have to "wake up the propagator" and have it start listening to all of its inputs. If not disconnect this input and start listening to a different input. For 3 variables this isn't a big deal. For a propagator where you can use 499 variables to determine the 500th? You can get some nice zChaff like speadups!

We can also use a 2 watched literal scheme to kill a propagator and garbage collect it. If we use a covering relation to talk about 'immediate descendants of a node' in our lattice, we can look for things covered by our _|_ contradiction node. These are 'maximal' entries in our lattice. If your input is maximal you'll never get another update from that input. So if we take our (+) node as an example, once two of the 3 inputs are maximal this propagator has nothing more to say and can be removed from the network.

We can indicate that you don't want to say anything "new" to a lattice by adjoining a "frozen" flag. You can think of it as the moral equivalent of saying we'll tell you nothing new from here out. This winds up the moral equivalent of Lindsay's quiescence detection.

Now we can look at a propagator network itself as a lattice in one sense, in terms of adding propagators to the network as increasing information. Then taking the ability to tell the network that it is frozen to give us opportunities to topologically sort the network, in the same fashion as stratified datalog. Now we can be more intelligent about firing our propagators:

I can run the network in bottom up topological order, queuing updates from SCCs in parallel. It gets a little tricky if we want the 'warm start' scheme from 2 watched literals -- you need to make sure you don't miss updates if you want to be able to do some more CmRDT-like cases rather than CvRDTs.

Finally, there are a lot of problems where we can view a propagator network itself as something useful to implement a propagator.

Consider constraint propagation. We can view the classic AC-3 algorithm for enforcing arc consistency as a propagator network. Once it is done _now_ we have arc consistent domains to enumerate with our finite domain solver. Which we can drive in the fashion I mentioned above to avoid the ATMS overhead.

On the other hand, a linear programming or mixed integer linear programming solver can also give lattice like answers as you add cutting planes to the model and monotonically increase the information present. In the MILP case we typically loop over these considering relaxations which inform us of new cuts we can make, etc.

Both of these are computations that _use_ lattice variables with propagators between them to build a better propagator themselves.

They are also nicely both fairly 'convex' theories. You could run propagators for constraint programming and MILP on the same variables and they can mutually reinforce with nicer guarantees than the dumb (+) propagator that I mentioned.

That one runs into issues when you go to do something as simple as y = x + x, and try to run it backwards to get x, because it looks locally to the propagator like 2 unknowns. We could of course try to globally rewrite the propagator network, by adding propagators to work around that, in this case it works if you transform it into 2 * x, and now the 2 is a known as is the y, and you can get to x. Here it is probably better to just borrow tools from the clpqr crowd, but it requires an unfortunate amount of introspection on the propagator network.

I have a couple of dozen other sub-domains that fit into this model.

I mostly find it interesting how all of these subtly different domains over almost exactly the same tools with minor differences, and how powerful it is to adapt those differences to other problems in the nearby domain.

Extend your numeric type tower to handle whatever new numeric types I come up with in an internally consistent manner.

In haskell I have number types for things that automatically compute derivatives. I have number types for functions that go to number types so all vector spaces work like numbers as well. I have number types for arbitrary precision floating point numbers, and I can build these things on top of each other.

It is a trade-off. We give up a bit of one thing to get something else.

You can take either side of the deal. I'd argue that the weight of benefit is on the side where we don't have a magic type tower to reason about, but it is a perfectly reasonable stance to say that the thing you want is more important to you.

On the other hand, I can turn around and argue that if what I really want is an ad hoc tower of numeric types I can just make a type for that and work inside it.

data Number = Int Int | Rational Rational | Double Double | Complex (Complex Double) | ...

instance Num Number

Now I can opt into your model. Can you opt into mine?

    import Control.Lens

    rewriteOf :: Setter' a a -> (a -> Maybe a) -> a -> a

    uniplate :: Data s => Traversal' a a

Now

    rewriteOf uniplate $ \case 
      Neg (Lit a) -> Just $ Lit (-1)
      _ -> Nothing

The data type itself was just something like:

    data Term 
      = Var String 
      | Neg Term 
      | Lit Int 
      | App Term Term 
      | Abs String Term 
      deriving Data