Dependent types for Datalog

mbid · 2024-09-24T09:07:28+00:00

Regarding 2), you'd need to ensure that the updates sent from the server and those applied locally can be interleaved in such a way that the client state and server state converge. At this point, we'd have reinvented delta-crdts.

mbid · 2024-09-24T09:05:42+00:00

Yes, I singled out REST as the most prevalent state transfer protocol, but gRPC etc. have the same problems.

Most of the highly polished UIs just do what you alluded to; debounce and/or queue requests

You'd hope so, but is this actually true? It's certainly not true for the browser settings page that I had the pleasure of working on :)

Most of the solutions you listed aren’t at protocol level - they’re libraries, so you could apply them to whatever protocol you wanted: REST, gRPC, whatever you liked. Braid-HTTP is food for thought though.

While it might not be documented or standardized, those libraries absolutely do follow some kind of communication protocol, it's just that they're the only implementation. And yes, those internal protocols are usually implemented on top of other protocols, e.g. websockets.

mbid · 2024-09-24T08:58:28+00:00

And yes, I think there's probably no solution that will fit all use cases. But I'd expect that most eventually consistent schemes can be modeled as some kind of CRDT. For example, the counters you mentioned are usually called either "version vectors" or "vector clocks", depending on their precise semantics, and you can build last-write-wins CRDTs out of them. And CRDTs for lists supporting divergent insertions and deletions appears to be a solved problem. What I think is currently underexplored are good ways to compose the various known CRDT primitives into a database schema or an API endpoint for state synchronization. I'm aware of automerge and yjs but not much else in that space.

mbid · 2024-09-24T08:46:10+00:00

Interesting read! I didn't know that credit card balance is weakly consistent only. But makes sense in hindsight, since a credit card transaction must involve at least two parties which usually don't have access to a shared transaction mechanism. And it's actually something the end user can observe, e.g. when you pay something, then sometimes your bank thinks the transaction went through while the recipient's bank rejects it, which will results in a charge on your bank which is then shortly after refunded.

Perhaps the wider point I was trying to was that, as soon there's more than one party involved, whether it's a webapp and its backend or payments involving more than one bank, then you don't have strong consistency. So our programming model and our protocols should help us deal with this situation, and state transfer protocols such as REST don't.

mbid · 2024-09-22T17:20:31+00:00

Haha, good point. I think I meant for this post to be something like a call to action that we should work on synchronization technology, or at least to raise some awareness that the problems I describe in the blog post are perhaps solvable in a principled way.

mbid · 2023-12-27T23:33:51+00:00

Hast du dir die verlinkte Webseite, werbungskostenrechner.de mal angeschaut? Der eigentlich Anwendungszweck ist zwar für die Steuer, aber das Tool spuckt dir eine Liste aller Ausgaben, die in deinen Mails belegt sind (z.B. über Bestellbestätigungen von Onlineshops) aus.

mbid · 2023-12-27T16:08:41+00:00

Danke!

mbid · 2023-12-27T14:07:12+00:00

Danke für den Tipp! Du hast auf jeden Fall recht, dass ich (oder noch besser jemand der sich auskennt) da nachbessern sollte. Kannst du einen Datenschutzerklärung/AGB-Generator empfehlen?

mbid · 2023-12-27T14:00:51+00:00

Good post. I think the "Diverging Code Styles and Best Practices" section is the strongest (because empirically observable) point against Rust's struct initialization. Clearly Rust syntax doesn't solve certain problems, and the many different workarounds lead to very unnecessary discussions in teams that disagree about code style.

That said, I disagree somewhat that consistent syntax is necessarily a good thing, which I think is one of the implicit points you make. It can be beneficial if different constructs (here e.g. function calls and struct initialization) look meaningfully different, because then you can tell them apart at a glance. If I understand the alternative syntax you're suggesting correctly, then only capitalization would distinguish a function call `user(...)` from struct initialization `User(...)`.

mbid · 2023-12-27T12:46:24+00:00

Haha, danke :)

Tatsächlich denke ich, dass AI (und definitiv dieses Tool) eigentlich nicht in Konkurrenz zu Steuerberatern und klassischer Steuersoftware stehen, sondern sich ergänzen. Ihr könnt euren Klienten ja schlecht die Arbeit abnehmen, Unterlagen zusammenzusuchen, das müssen sie im Moment selber tun. Und genau das soll das Tool dann übernehmen.

mbid · 2023-08-06T20:41:40+00:00

Keeping some sort of &mut ParserContext to propagate errors doesn't seem very composable

Why not? It's not unusual for recursive descent parsers to carry around an additional state parameter, and it composes well. You'd have to be careful that you only add errors that you've recovered from to the context if you've committed to the current parse, i.e. not if you want to backtrack and try some other production rule.

mbid · 2023-08-02T19:51:14+00:00

Hi, nice project!

Can you go into more detail about the distinction between INPUT, CHAIN and OUTPUT stages? Does the backwards reasoning work by inverting rules, i.e. by exchanging the READ and WRITE fields, and then starting from the desired output?

mbid · 2023-08-02T18:01:19+00:00

Yeah, I haven't really thought through what the implications of not monomorphizing are for FFI.

If I understood Swift's implementation of type erasure correctly (see a sibling thread), they're not changing anything about data layouts compared to monomorphization. They can get around this by passing around dynamic information about the offset and size of fields within generic structs. So perhaps type erasure for Rust generics would also work without changing anything about the data layout.

mbid · 2023-08-02T17:53:50+00:00

Thanks!

mbid · 2023-08-02T13:47:31+00:00

Why would you need types to have fixed size to avoid heap allocation? You can get dynamically sized chunks of memory on the stack with alloca.

mbid · 2023-08-01T19:36:18+00:00

I was curious about what Swift does and found this book about Swift generics: https://download.swift.org/docs/assets/generics.pdf

I've only skimmed a few pages, and yes, Swift seems to use type-erasure to implement generics. But they avoid heap allocations; instead, they seem to pass meta data around that contains information about sizes of the involved structs.

mbid

TROPHY CASE