Clojurians Log v2
core-typed
@ambrosebs Have you thought about tracking borrow information a la Rust in the type system? It would be convenient if functions with appropriate type annotations could be completely verified and inferred internally and potentially compiled to bare metal targets. https://github.com/carp-lang/Carp aims for something similar, but it is not a restricted subset of Clojure.
we dabbled in affine types for a GSoC project once. I wonder if it's related.
IIRC it was related to only using transients once. the complexity ramped when thinking about functions.
That makes sense. What is your take on having a unified type/constraint specification language? It is a bit odd that Clojure has so many that are each incomplete.
I would love to see full expressivity, where a subset of them can be statically checked and then maybe you only use this subset for most of your functions, or, in the ideal case, it could be reduced/weakened automatically until it can be checked.
There was for example https://typedefs.com/, which seems to be stale now (given the SSL error). I don't think it was complete, but it tried to have a fairly general language. I think spec is not too bad in general, but you are absolutely right about the parametric type problems it has and it is not very declarative and might be hard to reliably check. But I think for instance, I could declare a number as even? and then where the even? spec is defined it is declared that a weaker predicate is integer? , where the latter is type checkable by many checkers. So the type checker could just work with weaker types if needed to see whether it can find a proof of type safety and then optionally show its choices to the user.
In general it would be very good to have one sufficient dependently typed specification language that covers all the different use cases and can also be just checked at runtime like spec in case where type inference is not available (or possible), similar to how Python separated the specification of syntax from the actual type checking mechanism. I recently wrote an API specification for datahike which is used to automatically create bindings for Clojure, REST API and REST client. I would also like to use it for CLI, babashka pod, Datahike.java, libdatahike (C++) and Python bindings so I don't have to manually edit all the bindings every time I extend the API (and also to ensure consistency). I am using spec at the moment to define boundary information and translate that, but it would be nice if I could also encode parametric types and memory ownership directly. https://github.com/replikativ/datahike/blob/main/src/datahike/api/specification.cljc#L34
I guess my question is whether the current spec language is sufficient for that and what the limitations are.
It seems more verbose, but also more expressive than core.typed's type signatures.