Type-Safe Printf() in TypeScript

[jitl]

Word of warning: the typescript compiler is not a particularly fast evaluator of recursive list manipulation programs, which is what these kinds of types are.

They’re great in small doses where you really need them, but overuse or widespread use of complex types will make your build slower. It’s much better to avoid generics or mapped types if you can. The typings for a tagged template literal (without digit format specifiers like %d4) don’t require any generics.

I love to write code like this, but I’m guilty of over using fancy types and I flinch when I see a typescript build profile showing 45s+ spent on generic types I wrote without realizing the cost.

[kevingadd]

The nature of ts also means that if you make your files slower to build via type/list nonsense, the language server is going to bog down and the editing experience will mysteriously become bad for everyone. Strongly discourage doing slow stuff with the type system.

[quaunaut]

While I certainly agree, I've found that this is often an indication of too-complex an architecture, and a fundamental re-think being necessary. I've had projects that depend on [fp-ts], which end up incredibly generic-heavy, but still make it entirely through a typecheck(not build- typescript's just worse at that than other tools like esbuild) in seconds-at-worse.

Obviously depends on your organization/project/application, but I do like these things as complexity-smells.

[fp-ts]: https://gcanti.github.io/fp-ts/

[eyelidlessness]

Minor nit: I’ve found types like these—that is, iterative recursive types—benefit from using terminology common to map/reduce. And by “benefit from”, I mean become more understandable by a wider audience—not necessarily the HN audience per se, but quite likely teammates and future selves.

Which is to say, these names almost always make types like this more clear:

- Head: the first item in the input type you’re iterating through

- Tail: the remaining items or unprocessed structure you’ll likely recurse on next

- Acc (or pick your favorite “reduced” idiom): a named type for the intermediate product which will become the final type when you finish iterating. This can be provided as an optional parameter with an empty tuple as its default, largely modeling a typical reduce (apart from inverting the common parameter order).

It also helps, IME, to put a “base case” first in the type’s conditions.

When all of these names and patterns are utilized, the resulting type tends to look quite a lot like an equivalent runtime function you could encounter for producing the value equivalent to its type. This is great because you can even write the runtime function to match the type’s logic. This demonstrates both what the type is doing for people who find these “complex types” intimidating, and that the type accurately describes the value it’s associated with.

[AbuAssar]

this sounds similar to prolog!

[IceDane]

Cool.

There is a way to make this easier to extend, though: https://tsplay.dev/WGbEXm

Can't tell off the top of my head if there are any disadvantages to this approach though.

[crgwbr]

Neat, but this is basically a ripoff of this post from a few years ago (even to the point of not including the runtime implementation):

https://www.hacklewayne.com/a-truly-strongly-typed-printf-in...

[pkkm]

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?

[jamespwilliams]

> 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).

[doctor_phil]

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

[winwang]

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.

[paulddraper]

> 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)

[codr7]

Maybe check out Clojure spec?

https://clojure.org/guides/spec

[keybored]

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

[yen223]

The interesting thing here is that the typesafe printf has its function arguments inferred from a string literal, at compile time. You can change the 9 to a "9" and see the type error even before running the code.

This is something that most mainstream language's type system cannot do.

(This may be obvious, but a lot of commenters here might have missed that.)

[ruined]

not sure i understand the utility of this when format strings and string template types already exist.

you can also use typescript-eslint/restrict-template-expressions if you find yourself running into problems with that

https://typescript-eslint.io/rules/restrict-template-express...

[klodolph]

I think this is less about the utility and more about showing off unusual ways to use the TypeScript type system.

[taeric]

I've been kind of curious why tricks like this aren't used more to make sql and such. Heck, you could do similar tricks for shell execution. Or any general "string that is parseable." Seems we always take the route of not parsing the string as much as we can?

[lolinder]

This is a pretty neat application, but most embedded languages like SQL have a way more complicated grammar that would require a really complicated set of types to parse. This can tank the performance of your type checking step and it also means that the error messages you get out of the parser-in-types are going to be nearly useless.

A more common solution is to parse the string at runtime with a proper parser with decent error handling and then have the parser return a branded type [0] which you can use elsewhere to ensure your strings are well formed.

[0] https://egghead.io/blog/using-branded-types-in-typescript

[mind-blight]

I can't find it now, but someone actually built that for SQL in Typescript as an experiment. The problem folks run into is IDE and compiler performance. These sorts of features are what make your system turing complete, so they start stressing the compiler pretty quickly

[shirogane86x]

I think, from having it used recently, that supabase's TS library does this. I had to write a wrapper around it a few months ago at $dayjob and was really surprised when select/from parts of a "query" (not really a SQL query, because it's just a postgrest query) actually got parsed at compile time and spit out the right types. And since our code is pretty type heavy, I was gonna have to do that anyway, so I really appreciated it

[quaunaut]

There is actually efforts in the Typescript community attempting to do just that. Personally I think it'll end up being a waste, but these sorts of experiments, even when they fail, often can help along new discoveries.

And on the off-chance they get it right, then damn that's pretty great.

[jitl]

There is an implementation of SQL that operates on a table shaped type, entirely at type level. For your amusement: https://github.com/codemix/ts-sql

There are a bunch of more practical takes that codegen types from your database and generate types for your queries, eg: https://github.com/adelsz/pgtyped

To me the second approach seems much more pragmatic because you don’t need to run a SQL parser in your typechecker interpreter on every build

[aethros]

> why tricks like this aren't used more

Some languages don't support this.

The languages that do would require extensive systems to implement this feature. It may simply not be a priority over other requirements like thread safety, atomicity, etc.

> similar tricks for shell execution

Shell only supports strings, integers and lists. The type system is too limited for this level of type-checking.

This works in typescript due to the advanced type operations built into the language.

[akira2501]

Am I missing something? This is just a toy implementation of a function prototype, that only includes integers and strings?

[aroman]

As a general rule, if something is on the HN homepage and you find yourself asking "am I missing something?", the answer is almost by definition "yes" :)

It's just a cool use of some of typescript's more advanced features that many developers probably don't use on a day-to-day basis (likely for good reason, as other comments have pointed out!)

[k__]

Nice!

Now do ReScript. :D

[quaunaut]

Go's type system is inferior to Typescript's in every possible way. About the only saving grace it has is that it didn't start out in a non-typesafe ecosystem, but most of those issues have been alleviated in Typescript for years.

At this point, folks are seeing how far they can push the Typescript type system because it's capable of expressing so, so much more with its types than is seen typically(including in most other languages).

[dragonwriter]

> If JavaScript was a failure

By almost any reasonable measure it is one of the strongest candidates for “biggest success ever as a programming language”. Sure, you can argue that the reasons for that aren’t mainly language design related, but it is absolutely not anything like a failure.

[solumunus]

But the Go type system is pathetic in comparison to Typescript.

[beders]

Honestly, if you spend that much code on a single `printf`, I will reject your PR and we will have a conversation about code maintenance and cost.

Please don't adopt this.

[jitl]

printf is about 700 lines in musl libc https://git.musl-libc.org/cgit/musl/tree/src/stdio/vfprintf....

and there's no language-level type safety, although plenty of tools lint printf now

[Touche]

Except missing the pesky runtime implementation. We don't need though, right? As long as the types say it's right.

[smcl]

I think the point is safely typing the pattern of having variadic functions with a format string argument.

The function implementation itself isn’t that interesting, or “pesky” to be honest

[cobbal]

The static types depicted in typescript are entirely fictitious. Any similarity to runtime types is purely coincidental.

[davidmurdoch]

What do you mean? `console.log` supports `%d` and `%f` already.