11–20 of 35 posts
> Normal type systems (like C#'s) aren't Turing-complete. But it comes very very close: https://blog.hediet.de/post/how-to-stress-the-csharp-compile...
> Normal type systems (like C#'s) aren't Turing-complete. But it comes very very close: https://blog.hediet.de/post/how-to-stress-the-csharp-compile...
TypeScript's type system however is Turing complete!
Earlier quoted context omitted.
TypeScript's type system however is Turing complete!
If I remember correctly, the original issue filed about this was more of an alert than an expression of excitement. In either case the exclamation is warranted, but it’s fascinating how since then the TS type system has grown significantly more expressive in the ways it can perform arbitrary computations. You certainly could write a compile-time JSON parser or a SQL database in TS types well before template literal t…
Another interesting idea I've read, I think in a Haskell context, is proofs attached to values. You prove that a string originating from the user was HTML escaped - by calling the HTMLEscape function which attaches the proof - and then later in the code whenever you output it in the template it won't be escaped anymore because it's proven to be escaped.
[1] https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links
I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not?
(I don't have a robust understanding of Godel's incompleteness theorem.)
This is accurate, but it leaves out something worth note: types can reduce the scope of validation needed. That's still a worthwhile outcome to work towards.
There are ways to fight against this uncertainty (Pydantic, etc.) but you learn to unit test every little damn thing.
Scala will make you feel stupid sometimes because you don't understand the ideas underlying a piece of code, but a language like Python makes you discount your ability to know anything. A line of code "x = y" might be exercised by three different unit tests, but maybe they didn't follow that one code path where y is never bound. I get more paranoid about simplifying logic in Python than I ever did in Scala. Reading other people's code is like being a jaded detective in a noir film. The function parameter is named user_count, but the last time you assumed a parameter like that was a number, you took a blackjack to the back of the head and woke up wanted for murder.
This is just an observation about one narrow aspect of Python, by the way. I'm productive in Python, it's fun, and it's an amazing experience. The feeling of proximity to power with Python is unrivaled.
> This matters because understanding that a normal type system is not Turing-complete means that there are truths it can't express. I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not? (I don't have a robust understanding of Godel's incompleteness theorem.)
I think the primary problem is that the second we cross network or system boundaries all the guarantees go out the window. You have to be very defensive at every layer. If we’re ever able to encapsulate that in a type system that would be… impressive.