[HN Gopher] Extreme explorations of TypeScript's type system
___________________________________________________________________
Extreme explorations of TypeScript's type system
Author : joshuakgoldberg
Score : 80 points
Date : 2022-06-27 18:13 UTC (4 hours ago)
(HTM) web link (www.learningtypescript.com)
(TXT) w3m dump (www.learningtypescript.com)
| evolveyourmind wrote:
| Some other type-only TS projects:
|
| - RegExp matching through types: https://github.com/desi-
| ivanov/ts-regexp
|
| - Lambda calculus through types: https://github.com/desi-
| ivanov/ts-lambda-calc
|
| - Brainfuck through types: https://github.com/susisu/typefuck
| joshuakgoldberg wrote:
| These are wonderful, thank you!
| joshuakgoldberg wrote:
| TypeScript's type system is Turing Complete: meaning it has
| conditional branching (conditional types) and works with an
| arbitrary huge amount of memory. As a result, you can use the
| type system as its own programming language complete with
| variables, functions, and recursion. This blog post is a starting
| list of a bunch of the shenanigans TypeScript developers have
| pushed the type system to be able to do.
| tadfisher wrote:
| It also makes static checking undecidable in pathological
| cases. I know Idris has this problem as well; they work around
| it by skipping partial functions in types, so you end up with
| "total" and "partial" programs where only the former are
| completely typechecked proofs.
| Gehinnn wrote:
| That's not the meaning of turing completeness, just an
| implication of the space hierarchy theorems. There are systems
| that also have branching and unbounded memory, but are not
| turing complete. Context free grammars for example.
|
| Turing completeness means for TS that for every computable
| function, there is a TS type that can compute that function (if
| TS wouldn't limit the recursion depth).
| tobr wrote:
| > You have to wonder whether you could implement TypeScript
| itself in that language...
|
| I also wonder if you could compile TypeScript to TypeScript
| types? After all, you want your type manipulation code to be
| typesafe.
| adamddev1 wrote:
| Are there (m)any other languages with type systems as flexible
| and powerful as Typescript's?
| cjbgkagh wrote:
| I would guess that all languages with Turing complete
| typesystems would be technically equally powerful. I think
| Typescript supports more useful behaviors out of the box.
| dllthomas wrote:
| Equally computationally powerful, but not necessarily equally
| powerful as type systems. "X is Turing complete" means that
| it can compute the same set of computations as any other
| Turing complete system, but it does not mean that it can
| accept inputs and produce results in an encoding relevant to
| what you're trying to do.
| [deleted]
| yulaow wrote:
| I believe that typescript type system is so flexible, powerful
| and complex just because it had to be adapted and built around
| the shortcomings and limitation of javascript. It makes no
| sense to have something like it if you build a language from
| the ground up (or if you could just scrap backward
| compatibility in a bad designed one)
| valenterry wrote:
| Yes there are. For instance Idris (https://www.idris-lang.org/)
| has a way more powerful typesystem than Typescript.
|
| If you are looking for more practical and less academic
| languages, then Scala would be one of the languages that
| technically has a more powerful/generalized typesystem but at
| the same time is harder to use compared to Typescript's and
| cannot do some things that Typescript can do.
| singaporecode wrote:
| This was a good guide on TypeScript that I found online:
| https://ashok-khanna.medium.com/introduction-to-typescript-c...
| dllthomas wrote:
| > If you do find a need to use type operations, please--for the
| sake of any developer who has to read your code, including a
| future you--try to keep them to a minimum if possible. Use
| readable names that help readers understand the code as they read
| it. Leave descriptive comments for anything you think future
| readers might struggle with.
|
| Also, as you start getting complicated logic in your types, you
| need to test your types; make sure they admit things they should
| admit and reject things that they should reject. Ideally these
| tests can also serve some role as examples for your
| documentation.
| acemarke wrote:
| We do a _lot_ of this in the Redux library repos (examples: [0]
| [1] [2] ). We have some incredibly complicated types in our
| libraries, and we have a bunch of type tests to confirm
| expected behavior.
|
| Generally, these can just be some TS files that get compiled
| with `tsc`, but it helps to have a bunch of type-level
| assertions about expected types.
|
| I actually recently gave a talk on "Lessons Learned Maintaining
| TS Libraries" [3], and had a couple slides covering the value
| of type tests and some techniques.
|
| [0] Redux Toolkit's `createSlice`:
| https://github.com/reduxjs/redux-toolkit/blob/9e24958e6146cd...
|
| [1] Reselect's `createSelector`:
| https://github.com/reduxjs/reselect/blob/f53eb41d76da0ea5897...
|
| [2] React-Redux's `connect`: https://github.com/reduxjs/react-
| redux/blob/720f0ba79236cdc3...
|
| [3] https://blog.isquaredsoftware.com/2022/05/presentations-
| ts-l...
| brundolf wrote:
| @ts-expect-error is useful for this
| yulaow wrote:
| I lost it when at my previous job I found a 20 multiline super
| complex type defined by another dev, asked him to describe it
| because I was in a tight deadline and had not time to parse
| whatever he was defining. He starts with "it's pretty simple"
| and then used like 10 minutes to describe me what he meant
| while writing on paper the various pieces getting confused two
| times. At the end of the day it could be simplified in a one
| line union type of a few strings which would cover 99% of the
| usecases and the other 1% was something we had never used and
| would never use.
|
| I really wish people would focus more on keeping types as
| simple as possible instead of using that complexity just
| because the language allowed it.
| fishtoaster wrote:
| You can do some truly silly things with sufficiently ridiculous
| uses of typescript. I built a typecheck-time spell checker[0] in
| it such that: import { ValidWords } from
| "./spellcheck"; // Typechecks cleanly: const
| result: ValidWords<"the quick brown fox."> = "valid";
| // Throws a type error const result: ValidWords<"the qxick
| brown fox."> = "valid";
|
| [0] https://github.com/kkuchta/TSpell
| idontwantthis wrote:
| So does spellcheck contain a gigantic array of the English
| language?
| jjtheblunt wrote:
| the source code to answer your question is directly above
| your question
| xdennis wrote:
| Yes. It looks like this: export type
| ValidWords<T extends string> = T extends "" ?
| "valid" : T extends `the${infer Rest}` | `of${infer
| Rest}` | `and${infer Rest}` | ...
| joshuakgoldberg wrote:
| This is great!
| theogravity wrote:
| This is a great list. I feel I'm only scratching the surface when
| it comes to Typescript, and it would be awesome to have a place
| where we can see advanced examples of Typescript usage like this.
|
| I've seen many projects where the typing is done so well that it
| can infer and include all the data I've fed into the TS-defined
| functions / classes, which is great for IDE autocompletion.
| HyperSane wrote:
| What are some of the projects have done typing that well?
| theogravity wrote:
| If you're a GraphQL developer, Pothos is the best example -
| all your user-defined types just fits in it like a glove 99%
| of the time. It definitely makes the most use of TS generics.
|
| https://pothos-graphql.dev/
|
| (I'm a bit sleepy, so this is the main one I can think of at
| the moment that I really enjoy using.)
| sir_pepe wrote:
| Not really a "project", but TypeScript's own type definitions
| for the DOM are a great example. Eg. document.createElement
| returns different subtypes of HTMLElement depending on the
| string argument (HTML tag name) it gets called with.
| girvo wrote:
| purify-ts is my favourite currently.
| kevingadd wrote:
| When doing fancy things with typescript types, be really careful
| - it's possible to accidentally construct typescript types that
| will increase your tsc compile times by _multiple seconds_ and
| the tooling for troubleshooting this is nonexistent. A tiny
| change to one codebase I work on made compile times go from 300ms
| to something like 7 seconds and it took me something like 14
| hours of grepping and manually bisecting source code to find the
| cause - tsc was O(N * N * N) trying all possible types for a
| string literal to determine whether any of them were valid
| matches, and someone had defined a _very_ fancy string literal
| type.
|
| When this happens, typescript language integration (like in vs
| code or sublime text) will suddenly fall over and stop working
| correctly, and it'll be near impossible to figure that out too.
|
| Our build uses rollup to invoke tsc and as it happens their
| profiling system doesn't actually measure how long tsc takes to
| run - the time is unaccounted :) So in general, be aware that
| 'typescript is taking a long time to compile' is a blind spot for
| this whole ecosystem and if you hit it you're going to have to
| work hard to fix it.
| sir_pepe wrote:
| To try and limit one's use of operations on types, as suggested
| in the article, is not really great advice in my opinion. Sure,
| you would not want to actually implement and use a VM in types,
| but distilling rules about a program into types and then deriving
| the actual interfaces and signatures from those rules with
| operations on types? That's quite powerful.
|
| TypeScript's type annotations are really a DSL embedded into
| JavaScript. And they can, and, depending on the problem at hand,
| _should_ be treated as such.
| vore wrote:
| I think it depends how far you go: if you start encoding rules
| into the type system that are undecidable then you can quickly
| run into trouble.
| tevon wrote:
| To me its about readability. I agree that operations on types
| generally are a good thing because I find them more readable.
| Not using operations I've found leads to many very specific
| types which are hard to read and understand from the devs
| perspective.
| lf-non wrote:
| Yes, while that is true, TS errors can sometimes be really
| clunky. And sans a debugger, it is not uncommon for me to be
| spending stretches of 20-30 mins almost every week trying to
| unravel complex type errors that span multiple pages. I
| recently traced a very weird error to TS changing what keyof
| never evaluates to in a minor version.
|
| So yeah, using discriminated unions, branded types, mapped
| types etc. in moderation can substantially reduce the surface
| area of errors - more so than other mainstream nominally typed
| languages. However, trying to model and prevent every invalid
| state at type level can lead to a serious drain in
| productivity. And, I am not really sure how to draw a line
| between.
| jasonkillian wrote:
| > TypeScript's type annotations are really a DSL embedded into
| JavaScript. And they can, and, depending on the problem at
| hand, should be treated as such.
|
| I think this is the key. If treated as you describe, meaning
| the advanced types are well-written, well-documented, and well
| unit-tested as if they are "true" code, then using them
| shouldn't be too much of an issue.
|
| However, I think people often just assume that the types aren't
| "real" code and thus the normal concepts of good software
| engineering don't apply and type monstrosities which nobody can
| understand result.
|
| Imagine if this code[0] wasn't well-documented, fairly clearly
| written, and also tested. It would definitely be a liability in
| a codebase.
|
| In addition, the rules of how advanced TypeScript concepts work
| can be quite nuanced and not always extremely well defined, so
| you can end up in situations where nobody even _really_
| understands why some crazy type works.
|
| [0]: https://github.com/sindresorhus/type-
| fest/blob/2f418dbbb6182...
___________________________________________________________________
(page generated 2022-06-27 23:00 UTC)