5 ms·

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 surprisi

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 https://github.com/microsoft/TypeScript/issues/14833

MatthiasPortzel 4y ago
Aphyr has a series of posts in this style, all of which are excellent.
- faitswulff 4y ago
  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!
- dabreegster 4y ago
  I love this series. It also reminds me a bit of https://unsongbook.com https://unsongbook.com -- another beautiful work of creative writing combining technology and magic.
eyelidlessness 4y ago
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 https://github.com/microsoft/TypeScript/issues/14833 1: https://github.com/microsoft/TypeScript/issues/14833#issuecomment-1454306600 https://github.com/microsoft/TypeScript/issues/14833#issueco...
hnfong 4y ago
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.
- the_gipsy 4y ago
  I am not well versed in Haskell, but wasn't the original also computing the solution with just the type system?
  - tome 4y ago
    Yup
- girvo 4y ago
  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 4y ago
    How does one even come close to such wizardry
    - girvo 4y ago
      Going deep into conditional types, and trying to contort Typescript into a dependent type system despite the fact it is not one!
    - WorldMaker 4y ago
      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.)
throw2311 4y ago
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 4y ago
  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 4y ago
    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 4y ago
    https://3fx.ch/typing-is-hard.html 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-compatibility.html https://www.typescriptlang.org/docs/handbook/type-compatibil...

MatthiasPortzel 4y ago

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

faitswulff 4y ago
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!
dabreegster 4y ago
I love this series. It also reminds me a bit of https://unsongbook.com https://unsongbook.com -- another beautiful work of creative writing combining technology and magic.

eyelidlessness 4y ago

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 https://github.com/microsoft/TypeScript/issues/14833 1: https://github.com/microsoft/TypeScript/issues/14833#issuecomment-1454306600 https://github.com/microsoft/TypeScript/issues/14833#issueco...

hnfong 4y ago

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.

the_gipsy 4y ago
I am not well versed in Haskell, but wasn't the original also computing the solution with just the type system?
- tome 4y ago
  Yup
girvo 4y ago
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 4y ago
  How does one even come close to such wizardry
  - girvo 4y ago
    Going deep into conditional types, and trying to contort Typescript into a dependent type system despite the fact it is not one!
  - WorldMaker 4y ago
    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.)

throw2311 4y ago

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 4y ago
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 4y ago
  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 4y ago
  https://3fx.ch/typing-is-hard.html 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-compatibility.html https://www.typescriptlang.org/docs/handbook/type-compatibil...