[cjbprime]

In case folks miss the link at the top of the article, this is translated from an old 2017 post by Aphyr.

That post was in Haskell, where it's not too surprising that you can do serious computation inside the type system.

This new post translates the ideas to TypeScript, which is more widely known, and which I once heard described as having "accidentally Turing-complete" types:

https://github.com/microsoft/TypeScript/issues/14833

[hnfong]

I'd say it's "inspired" rather than "translated".

The part about using the typescript language server to compute the solution, and the protagonist claiming the code is "concise" because only 4 lines of javascript were generated, was absolutely brilliant. Cracked me up at least.

Glancing at the actual code, I admit I'm with Criss in my ability to follow the logic, but it doesn't look like a direct translation from Haskel types to Typescript types either.

At any rate, very well done.

[blauditore]

The final punch line is that types vanish and the compiled code is effectively useless.

[girvo]

I know my mind is decidedly poisoned when I could follow the type definitions perfectly, and they reminded me of certain types I have written myself… ah, TypeScript, what have you done to me…

[aw9f70gae]

How does one even come close to such wizardry

[WorldMaker]

Deep diving into lib.d.ts and DefinitelyTyped dealing with the weird boundary space between poorly typed JS and strongly typed TS can teach a lot these days.

Also, being able to recognize the Peano S-function on sight (and thus uses of Church-Peano numbers) is a fun part of that wizardry. (Maybe not necessary to remind the usefulness of the Lambda Calculus canon on a site named after one of the most famous combinators.)

[girvo]

Going deep into conditional types, and trying to contort Typescript into a dependent type system despite the fact it is not one!

[the_gipsy]

I am not well versed in Haskell, but wasn't the original also computing the solution with just the type system?

[tome]

Yup

[eyelidlessness]

Here[0] is the open issue about TypeScript being Turing complete. The current most recent comment[1] is showing the type system parsing its own type syntax. Of course there have been many parsers written in the type system since template literal types landed, but I found this one particularly amusing.

0: https://github.com/microsoft/TypeScript/issues/14833

1: https://github.com/microsoft/TypeScript/issues/14833#issueco...

[MatthiasPortzel]

Aphyr has a series of posts in this style, all of which are excellent.

[dabreegster]

I love this series. It also reminds me a bit of https://unsongbook.com -- another beautiful work of creative writing combining technology and magic.

[faitswulff]

This post also mentions "Vidrun," which features heavily in Aphyr's posts. And the interviewer in this post recognizing the situation they were in had me literally laughing out loud!

[throw2311]

All useful type systems are turning complete. The only people who don't realise are those that want to rewrite everything in rust.

[nine_k]

Were this true it would be terrible, because Turing-completeness necessarily includes non-termination. This would mean that a compiler would crash, or get stuck in an infinite loop.

[WorldMaker]

It is true and it is terrible. Woe to be a programmer. The Church-Turing Theorem implies it is almost impossible for any languages exhibiting recursion to not be (Church-)Turing Complete. It is easy to forget how deeply, darkly, and deceptively simple the Lambda Calculus is. It is easy to forget that anywhere you may splice in something that even gently resembles the Lambda Calculus you may draw out the frightening runes of the many eldritch combinators many of which are indeed subject to accidental infinite recursion and The Halting Problem. (Including the infamous Y combinator.)

I have seen the Typescript "computing this type lead to what appeared to be infinite recursion and I gave up" errors. The compiler is well built, it mostly does not truly crash in an exceptional case like that, but it does have to use hard, practical heuristics to avoid getting stuck in infinite loops (including harsh stack depths and calculation timeouts for type checking).

[cben]

https://3fx.ch/typing-is-hard.html is a neat summary, and yes the situation is worse than most programmers would guess: Most industry languages, including "boring" reliable ones like C++, Java or Rust have _undecidable_ type systems;( and quite a few are unsound as well.)

This doesn't mean type systems are useless! But as GP said there are tradeoffs, and suspiciously many language designers gave up "clean" properties like guaranteed-terminating compiler, or you know actually guaranteeing run-time safety...

BTW, TypeScript documents where it's unsound and why consciously made those choices: https://www.typescriptlang.org/docs/handbook/type-compatibil...

[illiarian]

This also probably means that you really need to start writing tests for your types :)

[efficax]

yes, all turing complete type systems make it possible to define type structures that would cause infinite loops, but typically they are able to detect this and refuse to compile

[hoseja]

-_-

“Oh, right.” He blusters a non-termination argument at nobody in particular. “That’s why we usually think in subsets of Haskell where types don’t have bottom values.”

[throw2311]

Yes, this is why unsafe exists. It tells the typing system to take a hike and let the natural Turing completeness of types happen. Trying to explain to people who don't understand higher order functions that types are the first rung of an infinite ladder of meta languages is like trying to explain the colour blue to nematodes.