Clojurians Log v2

I gave codex a spin today and ported cur in a simplified form to Clojure https://github.com/whilo/cur (WIP).

Well I didn't mean Julia for its type system but as an example of a performant implementation of an expressive abstraction. As for dependent types, I know some languages in that category (agda, idris, lean...) but have never written a program in any of those languages. My recent (very modest) efforts were only formalizing an abstraction in agda (because Conal recommended agda specifically).

I think coding assistant can be very helpful at picking one up. I would go for Lean if you are interested in general proofs for mathematics, and maybe F* if you want to see real world code written in it. But it all depends. I think Conal recommended it back in the day compared to Haskell. I think he started using it around 2019-2020.

I see. It depends on what you want. Conal does PL research and verification of ideas. If you care about a more practical language with dependent type features then F* is definitely a candidate.

I am not an expert in any of these systems, I only played a little with them. But I have been roaming in the academic context around them a bit.

If you like this material, you should go to a PL conference, maybe ICFP. I met Conal there in 2019.

I am also happy to help in so far as I can. I think it is a very valuable direction to explore, and it is a shame that Clojure does not have stronger specification and verification tooling. The attitude of its creators has a blind spot there.

I have worked repeatedly in Julia for simulations. E.g. https://github.com/whilo/Firms.jl. It is not a bad take on integration of types with a dynamic language, but the type system is also not super expressive, and the way it compiles creates a lot of compile cliffs (probably because of all the LLVM machinery). I find F* and Lean more interesting with respect to type systems. But type checking there often requires helping the system prove invariants, in particular for Lean. Personally I would find something closer to Dafny or https://www.youtube.com/watch?v=er_lLvkklsk most interesting, where everything bottoms out in the same environment and you can describe invariants in the same language as the code, e.g. through local assert statements that you then prove are never violated for certain input constraints. I haven't investigated Lean enough yet to see how flexible it is with metaprogramming and typing.

On read is very lightweight and mostly is there to make sure that refs get mapped properly. The main schema functionality is on write, which ensures Datomic compatibility. @konrad.kuehne implemented this some time ago for Job tech (@uppfinnarjonas has continued this work to make Datahike replace their Datomic backend). I agree that this form of schema is fairly limited, we have been working on something similar to what you are describing by simply using Datalog itself https://github.com/datopia/invariant. Each attribute has a query assigned to it that needs to unify for a transaction to be accepted. This is part of a blockchain system we were developing on top of tendermint, to show that this would also be a very elegant way to write smart contracts. Unfortunately we were a bit too busy, but I think the idea is still valid and Datahike has also come a long way and scales much better now.

Wow! That looks very promising! @itai and me have also speculated that we could implement a more flexible layer of validation on top of tx function and entity/attr preds. We were somewhat worried about the impact on performance of the single transactor (it's not something that would stop us from going forward, but something that we thought and were aware of). Have you engaged in performance and scale work with datahike & invariant yet?

Sure, you can slow it down a lot with the current approach potentially, and there are fundamental trade offs between expressivity and spped (this is one reason for Datomics/SQL database's simple schemas). The beauty of the invariant direction though is that to speed things up in general you need to work on the Datalog query engine. This is something that is fairly well studied and understood (take Souffle or other Datalog implementations for example [I can pull out more specific papers if needed]). Another angle to speed things up is to first speculatively execute the invariant in parallel and then check that the datoms the invariant query has consumed have not been changed by other queries. In the current approach this can be done beforehand for a large batch of new Datoms, as you can see which attributes they touch.

Do you already have specific plans where to go with this?

The schema is not necessary, but it will make querying more tricky if your data is heterogeneous and you don't know about it. E.g. if an attribute is sometimes a string and sometimes a nested data structure. Enforcing a schema during write is recommendable for databases that you use for your business logic and that you want to rely on. Having said this, there is value in having databases that don't require a schema. xtdb has done this right. I opened an issue here and will try to merge a PR with an experimental feature for unstructured input https://github.com/replikativ/datahike/issues/729

I understand the value proposition of a schema. I believe a db should support an integration with a declarative schema language and enforcement layer. But I could argue that for my case the schema language is not expressive enough (i.e I can't express my needs in the boundaries of this language). And therefore I would expect some escape hatch for users to escape my (probably) not perfect schema layer. But you seem to understand that there are use cases where a rigid schema is not appropriate so I'm preaching to the choir here 😅.

That makes sense. What schema language would you like? Maybe something like spec might be better. You could use it and then use schema-on-read maybe with the PR I just opened.

@whilo that's a great question, I'm so happy you're driving to this subject with me. Actually me and @itai have been researching this topic a lot lately. If we're looking into the clojure ecosystem spec is the official goto but doesn't seem to pass the alpha phase, either they work on something really big that the current state doesn't pass the bar or they're blocked on something or stopped working on it altogether. Either way, it seems that spec has not gained the confidence of its creators or this community. In this ecosystem I'd go with Mali. It seems most mature and actively developed. But I really liked fluree's choice to go with w3c standards. In this space you have json-schema or SHACL...

adding to that, you are talking about data shape. i would also like a way to express "rules" that depends on existing data (like datomic tx fn), for example max cardinality of 5, or min cardinality of 1 for another entity (ref integrity). these rules do assume a single transactor tho and require a schema on write, so i guess we have to think of some combination of these two

@itai , @whilo mentioned schema-on-read. Maybe what you described can also happen on read and the question is what would happen when the schema fails? Maybe it returns the last point at which the data was valid?

i think that there are cases where you want to "fail" a transaction on write and let the client know about the failure (and the reason) for example, a withdrawal of an amount larger than the balance

@whilo IIUC in datahike it's either on write or on read right? You can't declare an on-read schema & on-write schema

This is also a tradeoff for dependent types. Fundamentally you cannot have everything, but exploring good tradeoffs is the best thing we can do ofc. Have you explored systems like this? What are you currently exploring?

I happened to play a bit with agda recently in an attempt to formalize an abstraction we developed which hit performance issues. I actually wanted to formalize the abstraction in order to have greater confidence with optimizing it (an idea I got from Conal Elliott).

As for the fundamental tradeoff between expressivity and speed: I have a notion of the relation between late processing, flexibility and speed, i.e. the more knowledge I have prior (or alternatively, the more constraints I have on the future), the more I can optimize early for faster execution in the future (aka compilation). Or the opposite: the less constrained the future is (aka the more flexible the future is) the less optimization I can apply early. But it's mostly a vague notion, a rule of thumb, not a law I know to be proven. I can also see a relation between flexibility and expressivity but that is all the more vague...

I am, actively looking for the fundamental principles in the area of expressivity (the expression problem is very interesting to me)

BTW, Julia is an interesting study case here: it seems to have implemented one of the most flexible (expressive?) abstraction I know (multiple dispatch) and archived somewhat of a top tier performance. Unfortunately I haven't experienced it first hand, and I can't tell what tradeoffs were made there.

@whilo thank you for your useful responses it's definitely helpful. I asked in the datomic channel but couldn't find an answer there, maybe you'd know: why is the schema (even only at the ref level) necessary? I'm guessing you need a way to distinguish values from refs, I think you could do that at the particular value level. I'm also guessing it would impact performance, does someone know how to measure that impact? And more importantly: are my guesses correct or are there other considerations?

No, we're still not in the performance analysis and optimization phase yet, we're on the abstractions and interface design phase but we want to learn on the subject as much as we can in advance because performance considerations can devastate abstractions and interfaces if ignored completely...