Live data from Hacker News

Making sense of TypeScript using set theory

blog.thoughtspile.tech

51–60 of 94 posts

Re: Making sense of TypeScript using set theory

#51
post #45

Earlier quoted context omitted.

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…

> Typescript is designed to accept any valid Javascript program That's not strictly true though. `a (d)` is valid Javascript but Typescript treats it as a different syntactic construct[0]. [0] https://www.typescriptlang.org/play?#code/C4TwDgpgBARlC8UB2B...

It is strictly true. a(d) is only valid JavaScript iff a, b, c, and d are values. The TypeScript expression a(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.

Re: Making sense of TypeScript using set theory

#52

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 n…

`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.

Re: Making sense of TypeScript using set theory

#53
post #49
post #48

Earlier quoted context omitted.

> 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.

(butting in) What is recursive about the parent comment?

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.

Re: Making sense of TypeScript using set theory

#54
post #45

Earlier quoted context omitted.

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…

> Typescript is designed to accept any valid Javascript program That's not strictly true though. `a (d)` is valid Javascript but Typescript treats it as a different syntactic construct[0]. [0] https://www.typescriptlang.org/play?#code/C4TwDgpgBARlC8UB2B...

Lol, this is brilliant!

Re: Making sense of TypeScript using set theory

#55
post #52

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 n…

`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.

The intersection of all typescript types is `never`. `any` is approximately equivalent to `unknown` in contravariant positions and `never` in covariant ones.

Re: Making sense of TypeScript using set theory

#56
post #30

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 =…

> 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.

Re: Making sense of TypeScript using set theory

#57
post #45

Earlier quoted context omitted.

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…

> Typescript is designed to accept any valid Javascript program That's not strictly true though. `a (d)` is valid Javascript but Typescript treats it as a different syntactic construct[0]. [0] https://www.typescriptlang.org/play?#code/C4TwDgpgBARlC8UB2B...

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(d))
    // TS output: Promise { : "pending" }
    // JS output: false false
TS playground: https://tsplay.dev/mAdeZN

Re: Making sense of TypeScript using set theory

#58
post #51
post #45

Earlier quoted context omitted.

> Typescript is designed to accept any valid Javascript program That's not strictly true though. `a (d)` is valid Javascript but Typescript treats it as a different syntactic construct[0]. [0] https://www.typescriptlang.org/play?#code/C4TwDgpgBARlC8UB2B...

It is strictly true. a (d) is only valid JavaScript iff a, b, c, and d are values . The TypeScript expression a (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 par…

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.

Re: Making sense of TypeScript using set theory

#59

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…

I think what’s confusing here is that there are two mental models that use the word “type” in an opposing way: if you think of types in terms of set theory, then “subtype of type A is a subset of type A”. But if you think of types in terms of a class hierarchy (like in Java), then by saying “subtype of type A is a superset of type A” you actually mean “an inherited type (class) that is further down in the class hierarchy has the same or more properties than the parent type (class) that is further up”.

So I actually would agree that your original statement is valid, assuming that you refer to “types” as “classes” in the sense of Java class hierarchies.

Post reply on HN