[HN Gopher] Making sense of TypeScript using set theory
___________________________________________________________________
Making sense of TypeScript using set theory
Author : hrafnstrom
Score : 101 points
Date : 2023-01-24 15:01 UTC (7 hours ago)
(HTM) web link (blog.thoughtspile.tech)
(TXT) w3m dump (blog.thoughtspile.tech)
| clord wrote:
| Having set types like this and refining them smaller is something
| I wish Haskell would learn from Typescript, especially the
| automatic inference side. I wonder if it would help with linear
| types? Are there any proposals? I know there are type level
| naturals in the type system, but this is more like wanting to
| deconstruct existing types like Int or String into subset types.
|
| e.g.,
|
| foo :: Int -> 3::Int | 4::Int
|
| foo 4 = 4
|
| foo _ = 3
|
| bar :: 3::Int | 4::Int -> Bool
|
| bar 4 = True
|
| bar 3 = False
|
| -- (bar 12) is a compiler error, and no need to handle other
| patterns
|
| baz :: 3::Int | 2::Int -> Bool
|
| bar 3 = True
|
| bar x = False -- Type of x is 2::Int
| consilient wrote:
| > Having set types like this and refining them smaller is
| something I wish Haskell would learn from Typescript,
| especially the automatic inference side
|
| Haskell has far better type inference than Typescript in large
| part _because_ it doesn 't have subtyping.
|
| There are libraries for open records and sums (e.g.
| https://hackage.haskell.org/package/vinyl) but they're almost
| always the wrong choice.
| scotty79 wrote:
| > Why does 0 | 1 extends 0 ? true : false evaluate to false?
|
| Because 'extends' really means 'is assignable to'.
|
| I feel like most of the questions from the post might be answered
| fairly easily by using reasoning of 'is assignable to'.
|
| Things assignable to A&B are things assignable to both A and B.
|
| Things assignable to A|B are things assignable to A or to B.
|
| 'never' means a type that nothing is assignable to and is
| assignable to everything (bit weird because it usually doesn't
| have any values but you can create value of type never with the
| use of 'as').
|
| 'unknown' means a type that everything can be assigned to but
| it's not assignable to anything (except itself and any).
|
| 'any' means a type that everything is assignable to and that is
| assignable to everything (except never).
|
| Ok. Ok. {} types is bit weird way to denote interfaces. :-)
| thoughtspile wrote:
| Fair enough, "is assignable to" is another synonym for "is
| subset of". I find it much easier to reason about things I can
| visualize, like sets, which is why I love my set
| interpretation.
|
| Edit: besides, it's quite unintuitve that "never" is assignable
| to anything. How can never be something?
| scotty79 wrote:
| > it's quite unintuitve that "never" is assignable to
| anything
|
| Yeah, at first I was mislead by this.
|
| Initially I thought never is opposite of any while, it turns
| out, it's opposite of unknown. And any is just super weird,
| dynamic wildcard thing that is as large or as small as needed
| for any given operation (but not as small as never).
| scotty79 wrote:
| It's harder for me to make that connection but thank you for
| your write up. It's really great.
| Danoha wrote:
| Because "never" is an empty set and empty set is a subset of
| all sets.
| thoughtspile wrote:
| Exactly, that's why I wrote the article =) Makes perfect
| sense in "set world", but not in "common sense" based on
| your feeling of the word "never"
| clord wrote:
| > unknown is the set of all JS values. any is a paradoxical set
| that includes everything, but might also be empty.
|
| Not really a paradox.
|
| - `unknown` is the intersection (&) of all types, including an
| internal one that has no shape or characteristics. `unknown |
| {int: number}` should be `{int: number}`. `unknown & T` is always
| `unknown`, any characteristic T has will be discarded by the
| intersection.
|
| - `any` is the union (|) of all types, including that internal
| one that can be anything, and yes, `unknown` too. `(any & {int:
| number})` should be `{int: number}`. also, `const x: any = 5 as
| unknown`. Union with `any` should always produce `any`.
| thoughtspile wrote:
| I'm afraid you're confusing something!
|
| The intersection of all types is never, because, say, number
| and string don't intersect. The union of all types is unknown.
|
| any doesn't show set-like properties and yields ternary logic
| in clauses like any extends T, which makes it a paradox.
| bazoom42 wrote:
| I think you have switched union and intersection. 'Unknown' is
| a type which can be anything, so it is the union of all types.
| 'Never' is the empty set of types.
|
| 'Any' does not really fit into a set theoretical model because
| it can be assigned to anything and anything can be assigned to
| it, so it is both a supertype of anything and a subtype of
| anything. Basically it just disables type checking.
| jakelazaroff wrote:
| I might be missing something, but isn't this line backwards?
|
| _> Subtype of type A is a subset of type A. Supertype is a
| superset. Easy._
|
| Subtype of type A is actually a _superset_ of type A, since it
| contains _at least_ all the properties of A.
|
| If you had (contrived example) a Dog class that inherited from an
| Animal class, Dog would be a sub _type_ of Animal, but its
| additional properties (say, a bark() method) mean that it
| actually has a super _set_ of the properties in Animal. And vice
| versa: Animal is a super _type_ of Dog, but it 's a sub _set_
| because it contains only the properties that Dog inherits.
| hbrn wrote:
| Types are not _features_ , they are _constraints_.
|
| "at least all the properties of A" means "all of the
| constraints of A and some more". Subtype of A is more _narrow_
| than A, even if it means that object of subtype A has to have
| more fields.
| feoren wrote:
| In your case, dogs are only those animals that bark. That's a
| subset of animal. Think of it this way: can you think of an
| object that satisfies (is-a) Dog, but not Animal? No. Can you
| think of an object that satisfies Animal, but not Dog? Yes. So
| Dog [?] Animal.
|
| hbrn has it right calling those properties _constraints_ , not
| features. With anything but a sealed class, the properties that
| are not present are _unspecified_ rather than _missing_.
|
| And indeed sealed classes feel very "un-set-theoretic" to me.
| RyanCavanaugh wrote:
| Nope. This is a common confusion.
|
| The set of properties of objects and the sets of objects
| themselves have a complementary relationship when it comes to
| union / intersection and subset / superset.
|
| Let's define a "property" as being a predicate that is true for
| all elements of a set. For example, a collection of red objects
| has the "red" property.
|
| A subset of a set of objects can only have _the same or more_
| properties than the set you started with. If you take a bunch
| of marbles of varying colors, selecting a subset of those
| marbles can yield a set with a new property (such as them all
| being red), but they are guaranteed to have the "marble"
| property.
|
| A superset of objects can only have _the same or fewer_
| properties than the set you started with. Adding marbles to an
| existing set of marbles can only make "they are all red"
| become false (if it was true to begin with).
|
| Union and intersection have the same duality; the union of two
| sets has the intersection of its properties, and the
| intersection of two sets has the union of its properties.
|
| These results come from logic, not TypeScript.
| antihipocrat wrote:
| In your example with marbles, the superset has the property
| of every element being comprised of a set of colors, let's
| say {black, red, blue}.
|
| The subset is {red}.
|
| Can't every possible property we can conceive of a subset be
| constructed in a similar fashion such that the superset
| contains at least the same number of elements and never less?
| yitr wrote:
| maybe a dumb question, but why does wikipedia say typescript
| is a superset of javascript?
|
| https://en.wikipedia.org/wiki/TypeScript
| thoughtspile wrote:
| Because all valid JS code is also valid TS code
| (considering implicit any). Or, put another way, the set of
| all valid JS programs is a subset of all valid TS programs.
| sirmarksalot wrote:
| Because Typescript is designed to accept any valid
| Javascript program, the set of valid statements in a
| Typescript program is a superset of the set of valid
| statements in a Javascript program. Typescript contains all
| the rules of Javascript, and then adds some more, but never
| in a way that contradicts the requirement that a plain
| Javascript program should compile, so that also means the
| language specification itself is a strict superset of
| Javascript.
| hbrn wrote:
| Here are 3 statements that were made in this thread:
|
| - typescript is a superset of javascript
|
| - superset of objects can only have the same or fewer
| properties
|
| - Typescript contains all the rules of Javascript, and
| then _adds some more_
|
| Do you see where the confusion is coming from?
|
| > that also means the language specification itself is a
| strict superset of Javascript
|
| This is where I disagree.
|
| TS _as a language_ has more _properties_ than JS, but
| less _rules_. I.e. you can create Javascript language out
| of Typescript by adding more rules (constraints).
|
| But TS _as a spec_ has more rules than JS spec.
|
| TS as a language is a superset of JS language. TS as a
| spec is a rough subset of JS spec.
| bazoom42 wrote:
| > superset of objects can only have the same or fewer
| properties
|
| This is potentially misleading. A superset will include
| more objects and therefore may include more individual
| properties. But type checking is about what can be safely
| assumed about _all_ members of a set, so more different
| objects in the set will constrain the type more.
|
| Object is a superset of Date because the set of objects
| includes alle Dates but also things which are not dates
| and have different properties. But in the context of type
| checking, object is more constrained because there are
| fewer properties which _all_ members of the set are
| guaranteed to have.
|
| Typescript is a superset of Javascript because all
| Javascript programs are also Typescript programs. There
| is no contradiction.
| hbrn wrote:
| > object is more constrained because there are fewer
| properties which all members of the set are guaranteed to
| have.
|
| In my mind it's the opposite: object is less constrained,
| because there are fewer requirements you need to fulfill
| to be considered an object. Object type is very
| permissive.
|
| The more constrained type is, the fewer objects it's set
| will contain. The more constrained the type is, the more
| rules it enforces. Seems intuitive, isn't it?
| jbirer wrote:
| You are right, the statements are contradictory. It's
| strange to see how nobody questions marketing buzzwords
| from Microsoft.
| eevilspock wrote:
| You're making this harder than it actually is by
| conflating a bunch of things, comparing apples and
| oranges. Sets defined by type vs sets defined by lists of
| properties, specs, rules etc.
|
| For types, just draw the Venn diagrams:
|
| - The set of objects of Type A is entirely within the set
| of objects of Subtype of A. Subtype of A is the superset.
|
| - the set of things that are Dogs (class or real world)
| is entirely within the set of things that are Animals.
|
| - the set of things that are Javascript programs is
| entirely within the set of things that are Typescript
| programs.
| hbrn wrote:
| > Sets defined by type vs sets defined by lists of
| properties, specs, rules etc.
|
| Recursive explanations are useless: "types are just sets
| defined by types". That's why we are trying to define
| them through other means.
|
| Also TS has _structural_ type system, which is literally
| about comparing properties.
| strbean wrote:
| (butting in)
|
| What is recursive about the parent comment?
| hbrn wrote:
| It's recursive in the context of "making sense of TS
| using set theory". If you understand sets, but not types,
| statements about "sets defined by types" are meaningless.
| lhorie wrote:
| > Typescript is designed to accept any valid Javascript
| program
|
| That's not strictly true though. `a<b,c>(d)` is valid
| Javascript but Typescript treats it as a different
| syntactic construct[0].
|
| [0] https://www.typescriptlang.org/play?#code/C4TwDgpgBAR
| lC8UB2B...
| thoughtspile wrote:
| Lol, this is brilliant!
| qayxc wrote:
| It is strictly true. a<b,c>(d) is only valid JavaScript
| iff a, b, c, and d are _values_. The TypeScript
| expression a <b,c>(d) where b and c are types is NOT
| JavaScript, since JavaScript doesn't have type
| expressions. The statement that every JavaScript program
| is a valid TypeScript program does not imply the opposite
| - hence strict superset.
|
| edit: there is indeed an edge case with the parentheses
| that throws the TypeScript parser off even if only values
| are involved.
| lhorie wrote:
| See the sibling comment from oblosys for an example where
| the exact same code can give different results in vanilla
| JS vs after a tsc pass. As you can see there, the problem
| is that an identifier can simultaneously represent a
| value and a type.
|
| This is different than JSX or hashbang, where the set of
| non-JS syntax cannot legally overlap with existing
| syntax/semantics.
| oblosys wrote:
| With these declarations your fragment is valid in both
| JavaScript and TypeScript: class b {}
| class c {} const d = JSON.parse const a =
| Promise.prototype.then.bind(Promise.resolve(1))
| console.log(a<b,c>(d)) // TS output: Promise {
| <state>: "pending" } // JS output: false false
|
| TS playground: https://tsplay.dev/mAdeZN
| thoughtspile wrote:
| You're making the same mistake as I sometimes do, thinking in
| terms of "object shape" or "functionality". Here, I use
| "subset" in a sense of "all values that belong to Sub also
| belong to Super", in line with a set-theoretic view of types in
| the post. Also see subsets on wiki:
| https://en.wikipedia.org/wiki/Subset
|
| Try this one: A is subset of B iff all the values that belong
| to A also belong to B. In your example (and in real life),
| every dog is an animal, so dogs are a subset of animals.
| Koshkin wrote:
| > _4. A_ extends _B ... can be read as "A is subset of B"._
|
| I agree, it is unnatural to think of a subset as "extending"
| the set it is part of.
| epolanski wrote:
| > Subtype of type A is a subset of type A. Supertype is a
| superset. Easy.
|
| I think it is correct.
|
| Example:
|
| type A = { a: number }
|
| type B = { a: number, b: number }
|
| B is not a superset of A, it's a subset and subtype of A. You
| can use B every time you want to use A.
|
| In other words, of all types that can be assigned to A or used
| in functions and types expecting an A, B is one of those
| subsets.
|
| type C = { a: number, c: number }
|
| is another subtype of A.
|
| A "subtype" C can be substituted in place of its "supertype" A.
|
| Both C and B are subsets of A, in other words: in the infinite
| set of values of type A, some can be grouped in a type B or C.
| C itself is a subtype of A.
| david-farr wrote:
| Great article!
|
| Not entirely related to the post, but what app did you use to
| create your diagrams? They look fantastic.
| thoughtspile wrote:
| Thanks!
|
| I use excalidraw: https://excalidraw.com/
|
| I think most web-dev bloggers use it, makes me feel very boring
| maxfurman wrote:
| The difference between `any` and `unknown` is that `any` is an
| escape hatch from the type system. `any` can be used anywhere and
| will satisfy any type constraint. `any` is how the developer says
| to the type system "trust me, I know what I'm doing, don't worry
| about this particular value." Unknown, on the other hand, is for
| untyped code from an imported JS library, JSON data received from
| the network that may or may not match the API spec, etc. Code
| that does have a type, but that type needs to be confirmed at
| runtime and can be narrowed through type guards.
| joshfee wrote:
| `any` should really be called `every` to match the semantics,
| it says "this value is an instance of every type, and therefore
| you can do anything with it".
|
| And you might read that and thing "but that's crazy, its not
| possible for a value to be an instance of everything!" and
| you'd be right - the `any` type in TS is in fact crazy and you
| should not use it.
| consilient wrote:
| The intersection of all typescript types is `never`. `any` is
| approximately equivalent to `unknown` in contravariant
| positions and `never` in covariant ones.
| theonething wrote:
| > I know what I'm doing
|
| `any` can also be an indicator of the exact opposite.
| mrbombastic wrote:
| It certainly is for me :)
| thoughtspile wrote:
| I think "unknown" is more than that! Basically it's a way to
| say you don't care about the type, as in Record<string,
| unknown> or P extends Promise<unknown>
| sirmarksalot wrote:
| This is technically correct, but I suspect it's pretty rare
| that you would choose "unknown" over a generic parameter.
| Even if you're writing an algorithm that doesn't care about
| the data type, it's still probably going to be used by
| application code that does care, and you'll want to support
| that need by passing the type through, otherwise the
| application will be forced to downcast.
| thoughtspile wrote:
| I often use it to infer one generic parameter:
|
| type Output<Fn> = Fn extends ((a: unknown) => infer Out) ?
| Out : never;
| edgyquant wrote:
| But you have to care about the type with unknown? For
| instance calling this on an unknown
| obj.value
|
| Will return a type error that value doesn't exist on unknown.
| While calling it on an ant is valid typing
| _greim_ wrote:
| > But you have to care about the type with unknown?
|
| It's better to say `unknown` is a promise that you won't
| care about the type. When you write `obj.value`, you're
| caring about the type. TypeScript sees that and says "hey,
| you promised you wouldn't care about this type."
|
| > While calling it on an ant is valid typing
|
| It's still invalid, same as if you'd used `unknown`. It
| just suppresses the type error. The presence of `any` in a
| codebase is a very real risk. The only reason it exists is
| to allow incremental porting from JavaScript to TypeScript.
| thoughtspile wrote:
| Here, you expect obj to have a property called "value", so
| I'd say you do care about the type of obj. A valid type
| would be obj: { value: blah }
| jax_the_dog wrote:
| How is unknown better than any in this case? If you do not
| care about the data type, wouldn't you say that "any" data
| type is acceptable? If you say "unknown" that means that
| there is possibly some data type that would break your
| function.
| madeofpalk wrote:
| The problem with using any where you don't care about the
| type is that someone can come along and make unchecked
| assumptions about what type it actually is. Unknown is
| spicier as it'll prevent developers from assuming it's a
| string or object or something.
| jax_the_dog wrote:
| That makes some sense to me.
|
| I'm not a TypeScript dev so I apologize for the stupid
| question. Is there any functional difference between the
| two? I.e. is there a case where using Unknown instead of
| Any will result in some sort of "compile" time error
| opposed to a runtime?
| WorldMaker wrote:
| Yes. `any` really does turn off _all_ type checking. You
| see that offhand mentioned in this article talking about
| some of the paradoxes of `any`. `unknown` is still type
| checked and is arguably "merciless" type-checked that to
| do much of anything with an `unknown` you _have_ to check
| for a more specific type first or the compiler returns an
| error that what you are doing isn 't known to be valid
| for `unknown`.
|
| Some of that happens "automatically" at this point in the
| large number of ways that types can now be narrowed
| implicitly in Typescript (type guards [library
| functions], type asserts, the `typeof` runtime operator,
| the `in` runtime operator [as of recently], etc), so it
| can feel like `unknown`/`any` are the same up to a point,
| that point being where the runtime type is trivially
| known based on if statements and library functions around
| your use of the type.
|
| (Fun fact: `any` predates most type narrowing and
| `unknown` by several major Typescript versions. So `any`
| beyond just being the final "escape hatch" from type
| checking is also something of a legacy tool.)
| thoughtspile wrote:
| Almost every case where you use the value results in an
| error with unknown, but not with any: let
| danger: any; // These all compile: danger(),
| 9 / danger, danger.access, danger.map(x => x \* 2)
| let safe: unknown; // These all explode in TS:
| safe(), 9 / safe, safe.access, safe.map(x => x \* 2)
| madeofpalk wrote:
| Yes - trying to access a property or method on something
| typed as unknown will (almost?) always result in a
| compile time error because it's _unknown_ whether the
| value has that property or not.
|
| https://www.typescriptlang.org/play?#code/GYVwdgxgLglg9mA
| BAd...
| thoughtspile wrote:
| always, because "unknown" includes null / undefined,
| which don't allow property access at all.
| thoughtspile wrote:
| Saying a value is "unknown" means making no assumptions
| about the value. It might be a null, a number, a function,
| you don't care because you aren't going to do anything with
| this value. If you call() it, or read.some.property, TS
| complains because you're making assumptions about the
| object that TS did not ensure.
| piyh wrote:
| I went through my code base and found one use of `any` that was
| worth keeping around, the rest could be changed to `unknown`
| and better code resulted from it.
___________________________________________________________________
(page generated 2023-01-24 23:00 UTC)