4 ms·
> the type signature of your stereotypical statically typed language, e.g. reverse :: [a] -> [a], doesn't have a much information content. It's a little bit un
by grumpyprole 3y ago
> the type signature of your stereotypical statically typed language, e.g. reverse :: [a] -> [a], doesn't have a much information content.
It's a little bit unfair to imply any alternative to bleeding-edge clojure is going to have a simple 70's Damas-Milner type system. Today, static types can describe a lot more. Refinement types (e.g liquid Haskell) and/or dependant types (e.g. Idris or Agda) can describe and enforce the desired properties for reverse statically.
- tome 3y agoI think you're downplaying the strength of types! In any relationally parametric type system `reverse :: [a] -> [a]` has a huge amount of content.
- grumpyprole 3y agoI'm not downplaying anything, it was the parent who was dissatisfied with static checking of reverse. Personally, I think any static checking is better than none at all. Statically typed languages are perfectly capable of checking additional contracts/properties at runtime too (as Clojure does).
- tome 3y agoFirstly, I was being a bit tongue-in-cheek, but secondly you seem to be saying that a "70's Damas-Milner type system" isn't already an extremely powerful type system. I would say that it is!
- grumpyprole 3y agoI was just trying to combat the common narrative that static types are "what Java has". There is so much potential for static typing that has not been explored by industry (e.g structural typing).
- kaba0 3y ago(That common narrative is also quite negative, Java’s type system is surprisingly strong and can express many more things than people give it credit for. See jooq, or several FP java frameworks)
- grumpyprole 3y agoJooq is not a good example as it is essentially dynamically typed. Queries on the relational algebra can be statically typed, with structural typing and a few type-level features like sets. There are lots of papers on this.
- kaba0 3y agoIt is quite statically typed, look at the examples. You might be thinking of the stringly-typed version, but it can generate classes from DB inspection and use columns and whatnot with its respective type throughout a query, failing to compile when a group by value is incorrect! It can’t verify everything what a SQL engine can of course, but it is quite remarkable in my opinion.