Hacker News Reader

Comment by pkkm | Hacker News Reader

Reminds me of Idris: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...

Recently though, I've been wondering whether advanced type system stuff is the right approach. It usually becomes pretty complicated, like another language on top of the regular language. Maybe it would be easier to have some kind of framework for compiler plugins that do extra checks. Something that would make it easy to check format strings or enforce rules on custom attributes, like Linux's sparse does, using plain imperative code that's readable to the average dev. Large projects would have an extra directory for compile time checks in addition to the tests directory they have now.

But I haven't seen any language community do something like that. What am I missing?

View on HN

> Maybe it would be easier to have some kind of framework for compiler plugins that do extra checks. [...] But I haven't seen any language community do something like that. What am I missing?

Go has adopted a similar approach to this - they've made it fairly easy to write separate plugins that check stuff like this. The plugins aren't executed as part of the compiler though, they're standalone tools. For example, see golangci-lint, which bundles together a load of plugins of this kind.

Some of these plugins are shipped within the go command directly, as part of the "go vet" subcommand. (including a printf format check, which is similar to what's described in this post, i.e. it checks that arguments are of the correct type).

Sounds like comptime from Zig. There are a few others that does something similar, but Zig probably has most mind share right now.

You parse the string and then iterate over the passed arguments and check if everything adds ups. Rather straightforward.

Expressing it in the type system like TS did is impressive, but not simple.

I wonder if we should have a kind of "hidden type system", where we still take advantage of having a single type system to reason about, but the extra-specific "weird-ish" types can be hidden, almost like private variables, where visibility is literally hidden from the programmer unless obtained from debug modes or errors.

You mean like the C++ auto keyword but everywhere?

auto is just type inference, doesn't change any visibility

> another language

With the property of verifiably correct behavior

> compiler plugin

A number of languages allow it (Haskell being the most prolific example, but also Java, Scala, gcc, many others)

Maybe check out Clojure spec?

https://clojure.org/guides/spec

Unless I'm mistaken, Clojure spec operates at run-time, not at compile-time.

I don’t see why static assertions wouldn’t be enough in this case.

Reply on news.ycombinator.com