> A program P is monotonic if for any input sets S,T where S ⊆ T, P(S) ⊆ P(T).
> A program is monotonic if, when you run it on a subset of its inputs, you get a subset of its outputs. As you run it on more data, the set of true things may grow, but it never shrinks.
Yeah, this framework seems powerful.
Something I find interesting is that you can get monotonic (and therefore coordination-free) relaxations of arbitrary problems. In extremis, you can derive a relaxed version P' thus
P'(S) = {<s, P(s)> | s ⊆ S}
and now
P'(S) ⊆ P'(T) if S ⊆ T for _any_ (well defined) P
This seems tautological but in some cases a relaxed version is good enough: it gives you convergence and eventual consistency in a coordination-free setting, at the cost of maybe having to roll back some results. And when it doesn't, it gives you a coherent model of what to make of the situation until coordination yields a definitive answer.
But that was like last week, haven't really put this in practice yet.
In those examples what is being processed are partially-ordered operational logs, but it's essentially the same (just that whenever S ⊆ T there, what you're seeing is an extension of an op log, which is a bit more intuitive).
This boils down to materalizing every possible nondeterministic outcome.
I wouldn't call anything that involves a power set with 2^n space complexity "relaxed" tbh ^^'.
While I do agree with the general sentiment, I do still think that going with states that can be reconciled/merged is a more realistic approach, than just wildy diverging.
The logic for taming unbounded nondeterminism has been around for decades though. As Dijkstra and Scholten admit, it’s basically just applied lattice theory.
In fact, at a glance, this paper appears to be building on that foundation. It’s not hard to see how monotonicity makes reasoning about nondeterminism considerably more manageable!
Did you read the remark at the end of my comment? In the practical cases I was exploring, that combinatorial explosion does not happen. It's relaxed in the sense that it is coordination-free.
Yep. The DID is kind of like an internal UUID, so we don't have to show it to them often. The three cases off the top of my head where you'll care
1. You're setting your own domain handle, in which case you're putting it in your dns record. In this case, it'll just be that string you're sticking in the TXT record.
2. You're migrating hosts. We haven't implemented this flow yet, and since the DID will be referenced in your data export you may not even be aware of it in this case.
The case I found more worrisome is you follow someone, they then start using a new domain, and now it seems you're following a different handle (IDK if handles are immutable in Twitter, maybe they are not?).
Maybe BlueSky could offer a registrar that would do steps 1 & 2 for you transparently upon domain purchase.
Ah sure, that could be confusing -- though I believe Twitter allows you to change your handle as well. We could probably try to let people know when a handle changes, but we'll wait to see if it causes a problem before we get into it.
If there is not a mapping to some sort of immutable handle, i imagine some sort of announcement in the timeline(example.com has changed their handle to example.xyz) and a history in their profile (handle = example.com 2017 to 2020-01-01. example.xyz 2020-01-01 to now) would cover it
Ideally you could use the domain as a (vanity) pointer to an immutable handle and when someone follows the domain they'd actually be following an immutable identity that's a combination of the domain + immutable handle which reference each other.
example.com <--> ryan29-abcdef
I was trying to explain how I'd do it for a package repo a few months back.
You can change your handle on Twitter, but it's not recommended if you have any "follow me on Twitter @soAndSo" links out in the wild, because it opens people to handle squatters taking your old handle.
This sounds a bit like those stories about Kodak having a digital camera before anybody else did, and they just fearfully watched the thing from a distance doing nuthing until someone else brought it to market and ended the party for them.
May be an entirely different thing this time of course. But still...
Well they had a giant conversational size bigger than GPT3. It was not as safe or good at following instructions as ChatGPT. But it was as flowing as it is. So maybe it's an exaggeration (this word has two gs in english!?) to say that it's as good, but it was also extremely strong and impressive
This is a cool idea, but I didn't find any examples of max length constraints or other normalization rules in the source code I reviewed. Maybe there's something in there.
Hey! Author of the post responding here :) Unfortunately max/min-length is a global invariant and not one that can be reinforced by CRDTs without coordination
bloom-lang.net is a really cool project working on trying to figure out what types of program state actually require coordination at compile time
Right - I think what Sam is wondering about is if there’s a better way to maintain some of those invariants when decoding the CRDT data or at least preserve user intent with more fidelity by taking the invariants into account. For example, if a ProseMirror schema says “figure can have one caption child”, then a CRDT library can assist by making Child a LWW register instead of an array; or picking the last item in the array instead of the first when limiting length.
To me it seems mostly a composition problem; we need a better way of expressing these kinds of application constraints in a formal schema so we can encode/decode application data structures to CRDTs without requiring invasive intermixing of the two concerns in a way that explodes complexity of both the app and the CRDT details.
Okay wow, it's fun and surreal to see code you're working on pop up in the comment section unexpectedly right in front of your eyes :D
I've been helping Santi on this wiki application and we've actually been dreaming about how nice it'd be to eventually have some kind of schema language for defining Hyper Hyper Space types. In the current version of HHS, data types are fully defined via TypeScript classes, and constraints like that are implemented via the validation method you discovered. If that method returns false, the data won't even be stored or synced, let alone make it to the UI. So for now it's an open ended way of defining constraints, making it easier to explore and experiment. Many of the core HHS data types have constraints built into them too, enforced via the validate method. For example, the CausalSet type can be made to only allow certain elements as members.
Anyway there are a few reasons I can see that it'd be amazing to have something more like JSON Schema. One is that it'd just clarify using these data types outside of TypeScript, and ideally they'd be more succinct to read and write than TypeScript classes.
Another reason I'm especially curious about is the possibility of using it along with some kind of query system, which could potentially make a bunch of stuff easier both both in selecting data for applications and in implementing casual validation logic. Validating multiple interacting causal data types requires looking at chains of events in the DAG. Maybe being able to query for these chains could make this nicer?
All that to say, my guess is that the hardest part of moving to a succinct schema definition format would be how to deal with constraint/validation specification.
> I haven't found the underlying text or rich text CRDT implementation yet.
I think something like this in the works! Right now we're just using last write wins. We did experiment with using Y.js for realtime collaboration, but we ran into some complexity in reliably ensuring that the Y.js state could get persisted to the HHS data types without race conditions, so we took a step back from that idea.
I encourage you to follow up on the schema language plus a code generator. It’s a powerful technique that can make your implementation more agile as you develop new strategies.
In the 2000s we spoke about distributed operating systems (Inferno, etc.). That's where systems research seemed to be headed, yet that never really took off. But maybe we're revisiting the concept now, just coming down from the layer above (e.g. application data types) instead of trying to rethink the OS.
I work on this [1], it kinda looks like systems software, and it doesn't feel stagnant. But then, nobody uses it (yet - I hope).
And there's a plethora of similar ideas (DAT, OrbitDB, etc.).
The Web is our distributed operating system. You say the name of an application, and the latest version of its code gets loaded into your computer over an encrypted and authenticated connection, compiled for your platform, and run in a sandbox that isolates it from all the other applications you're running. You can use any device interchangeably to run it, and all your data is just there.
It's not a very good distributed OS (our data belongs to the applications, and integration between them is very limited) but we've definitely realized the mobile code and portable executable dreams of the 90s.
> we've definitely realized the mobile code and portable executable dreams of the 90s
Fine, now how to get rid of it, along with the lack of innovation and the entangled group or naive nerds and salesmen taking advantage of them who think or pretend the web is about their fscking apps when it was always about content.
Arithmetic is usually formalized using first order logic (that's what Godel did in his incompleteness paper, for example).
That means that one can write formulas quantifying only over numbers (that's what's done for the axioms defining addition and multiplication), but in order to get recursion, one needs to use infinite many axioms, one for each predicate P, saying:
if P(0) and (∀n)P(n) => P(n+1) then (∀n) P(n)
Intuitively, this gets us that all the numbers that can be reached starting from zero by using the "+1" operation will follow the rules of arithmetic.
But it does not guarantee that all numbers _can_ be reached this way. In the standard model, the one we have in mind, that is the case, but it turns out that there are constructions like this
0, 1, 2, ... -2', -1', 0', 1', 2' ...
having numbers that came after the ones in the standard model, but that cannot be reached by applying "+1" a finite number of times, where all the axioms of arithmetic are also true, and are therefore also models of arithmetic.
Some formulas are going to be true in one and false in the other, but all those are independent of the axioms of arithmetic. The study of formal methods in mathematics and their limitations is truly fascinating.
The Internet became mainstream because folks could use modems and phone landlines (circuit switching technology, that the new TCP/IP end-to-end packet switching stack would eventually replace) to get online.
The path for mass adoption of the new, p2p and interoperable technologies is the same: make them work on web browsers (using the browser as a full peer, not a client). It is the ubiquitous VM: JavaScript, WASM, IndexedDB, WebRTC+WebSockets, all the pieces are there.
The building blocks for a representation / data model are all in the air as well: CRDTs, Merkle-ized structures, content-based addressing, etc.
> A program is monotonic if, when you run it on a subset of its inputs, you get a subset of its outputs. As you run it on more data, the set of true things may grow, but it never shrinks.
Yeah, this framework seems powerful.
Something I find interesting is that you can get monotonic (and therefore coordination-free) relaxations of arbitrary problems. In extremis, you can derive a relaxed version P' thus
P'(S) = {<s, P(s)> | s ⊆ S}
and now
P'(S) ⊆ P'(T) if S ⊆ T for _any_ (well defined) P
This seems tautological but in some cases a relaxed version is good enough: it gives you convergence and eventual consistency in a coordination-free setting, at the cost of maybe having to roll back some results. And when it doesn't, it gives you a coherent model of what to make of the situation until coordination yields a definitive answer.
I wrote about this idea here: https://www.hyperhyperspace.org/report.html#conflict-resolut...
But that was like last week, haven't really put this in practice yet.
In those examples what is being processed are partially-ordered operational logs, but it's essentially the same (just that whenever S ⊆ T there, what you're seeing is an extension of an op log, which is a bit more intuitive).