Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Making sense of TypeScript using set theory

blog.thoughtspile.tech

Post reply on HN
Print view View original

81–90 of 94 posts

Re: Making sense of TypeScript using set theory

#81

Post by nequo »

clord wrote: 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 =…

LiquidHaskell[1] implements refinement types for Haskell. Would that do what you'd like?

[1] https://ucsd-progsys.github.io/liquidhaskell/

Re: Making sense of TypeScript using set theory

#82

Post by [deleted] »

Tainnor wrote: post #78
RyanCavanaugh wrote: post #23

Earlier quoted context omitted.

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…

This depends on what you mean by "property". Universal properties are preserved "downwards" i.e. in subsets (more properly, substructures). Existential properties are preserved upwards, i.e. in supersets (extensions). For example, the property "there exists an element that equals itself when added to itself" is preserved in a superset. If you have sentences that mix quantifiers (e.g. "for all epsilon, there is a delt…

[deleted]

Re: Making sense of TypeScript using set theory

#83

Post by hot_gril »

goodoldneon wrote: post #61
hot_gril wrote: post #60

Unrelated set theory thing: They say Typescript is a "superset" of Javascript, but plenty of valid JS code won't work in TS. For example, `let foo = 4; foo = "4";`

That isn't what "TS is a superset of JavaScript" means. That phrase means "TS syntax is a superset of JavaScript syntax". Your example is syntactically valid in TS -- it just fails a type checking

I see what you're saying about syntax and type-checking being separate stages, but they're both compile-time (or do we call it transpile-time?) errors enforced by the language. Either way, I can't copy-paste working JS code into TS, which is what matters.

There's probably another "asterisk" for this, but the other thing is how TS in Node by default won't allow `require` (vanilla NodeJS), only `import` (ESM).

Re: Making sense of TypeScript using set theory

#84

Post by consilient »

Tainnor wrote: post #80
consilient wrote: post #56

Earlier quoted context omitted.

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

> Haskell has far better type inference than Typescript in large part because it doesn't have subtyping. That's a bit like saying "Go has a faster compiler because the language is so simple". It's true, but there's a genuine tradeoff here. Haskellers have convinced themselves that subtypes are not worth it - and they may be right in many cases - but subtyping is a quite natural way of modeling many concepts (for exam…

That's my point. Haskell hasn't failed to "learn" from Typescript, it's picked a different point on the same frontier. There's no strictly improved structurally typed Haskell out there waiting to be written; there are fundamental obstacles in the way.

Re: Making sense of TypeScript using set theory

#85

Post by hbrn »

goto11 wrote: post #76
hbrn wrote: post #41

Earlier quoted context omitted.

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…

TypeScript is a superset of JavaScript because any JavaScript program is also a Typescript program but not vice versa. There is no contradiction. > TS as a language is a superset of JS language. TS as a spec is a rough subset of JS spec. This does not make any sense. A spec which fully describes TypeScript including runtime behavior would include the JavaScript spec and therefore be a superset. The TypeScript spec it…

This is how you should think about it: Spec > Language > Code.

Code is an instance of Language (and in structural typing land it can be compatible with multiple languages). Language is an instance (implementation) of Spec.

> sine it descries features and syntax which does not exist in vanilla JavaScript

That's exactly why TS spec is a subset. Take example from the article:

  type B = true extends boolean ? 1 : 0; // 1
Type B is a subset of boolean, meaning there are less objects in the world that satisfy type B.

There are less language implementations in the world that satisfy TS spec than JS spec. Every language that satisfies TS spec also satisfies JS spec. TS spec adds more constraints (requirements) to language implementation compared to JS spec, it is more strict, therefore it's a subset.

Re: Making sense of TypeScript using set theory

#86

Post by sirmarksalot »

lhorie wrote: post #45
sirmarksalot wrote: post #32

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

I guess this is a distinction between intent and results. Typescript is intended to be a strict superset of Javascript. In practice, there are edge cases like these.

Re: Making sense of TypeScript using set theory

#87

Post by goodoldneon »

hot_gril wrote: post #83
goodoldneon wrote: post #61

Earlier quoted context omitted.

That isn't what "TS is a superset of JavaScript" means. That phrase means "TS syntax is a superset of JavaScript syntax". Your example is syntactically valid in TS -- it just fails a type checking

I see what you're saying about syntax and type-checking being separate stages, but they're both compile-time (or do we call it transpile-time?) errors enforced by the language. Either way, I can't copy-paste working JS code into TS, which is what matters. There's probably another "asterisk" for this, but the other thing is how TS in Node by default won't allow `require` (vanilla NodeJS), only `import` (ESM).

Importing with `require` is CommonJS, not part of JavaScript’s spec. CommonJS is a Node-only thing so supporting it isn’t required in a JS superset

Re: Making sense of TypeScript using set theory

#88

Post by dclowd9901 »

maxfurman wrote: post #3

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…

That’s a convenient way of thinking about it. A more logically correct way of thinking about it is:

“any” can be any possible type

“unknown” is a specific stand-in type. It does not represent all types but is a subset of all types, which allows you to narrow its definition from nothing.

Unknown in practice is closer to a generic in terms of usage and semantics than “any”. It’s like a generic generic except it’s not useful until you direct it. It basically lets you kick the can down the road in your code of having to make a type decision, which is very useful for writing composable and uncoupled code.

Re: Making sense of TypeScript using set theory

#89

Post by goto11 »

hbrn wrote: post #85
goto11 wrote: post #76

Earlier quoted context omitted.

TypeScript is a superset of JavaScript because any JavaScript program is also a Typescript program but not vice versa. There is no contradiction. > TS as a language is a superset of JS language. TS as a spec is a rough subset of JS spec. This does not make any sense. A spec which fully describes TypeScript including runtime behavior would include the JavaScript spec and therefore be a superset. The TypeScript spec it…

This is how you should think about it: Spec > Language > Code. Code is an instance of Language (and in structural typing land it can be compatible with multiple languages). Language is an instance (implementation) of Spec. > sine it descries features and syntax which does not exist in vanilla JavaScript That's exactly why TS spec is a subset. Take example from the article: type B = true extends boolean ? 1 : 0; // 1…

So you are saying the implementation of the Typescript language are a subset of all JavaScript implementations? I guess that is true in a certain sense. But this does not contradict the fact that TypeScript as a language is a superset of JavaScript - rather it follows logically.

(Although in reality the Typescript implementation is a preprocessor, intended to use together with a regular JavaScript engine.)

Re: Making sense of TypeScript using set theory

#90

Post by hbrn »

goto11 wrote: post #89
hbrn wrote: post #85

Earlier quoted context omitted.

This is how you should think about it: Spec > Language > Code. Code is an instance of Language (and in structural typing land it can be compatible with multiple languages). Language is an instance (implementation) of Spec. > sine it descries features and syntax which does not exist in vanilla JavaScript That's exactly why TS spec is a subset. Take example from the article: type B = true extends boolean ? 1 : 0; // 1…

So you are saying the implementation of the Typescript language are a subset of all JavaScript implementations? I guess that is true in a certain sense. But this does not contradict the fact that TypeScript as a language is a superset of JavaScript - rather it follows logically. (Although in reality the Typescript implementation is a preprocessor, intended to use together with a regular JavaScript engine.)

Kind of. The language gets confusing because we use subset and superset next to each other, but we put different meaning on them.

{foo: number, bar: string} as type is a subset of both {foo: number} and {bar: string}. It requires it's members to have both properties. You can construct this type using intersection:

  type Foo = {foo: number}
  type Bar = {bar: string}
  type FooBar = foo & bar
{foo: 1, bar: 'hello'} as object is a superset of {foo: 1} and {bar: 'hello'}. It contains both properties. We can construct this object using union (I use pipe instead of spread to illustrate the idea):

  let foo = {foo: 1}
  let bar = {bar: 'hello'}
  let foobar = foo | bar
When I'm saying TS is a superset of JS, I mean it in the object sense. It has all the properties of JS, and some more. All JS programs are also TS programs, but not vice versa. There's more JS programs in the world than TS programs.

When I'm saying TS spec is a subset of JS spec, I mean it in a type sense. Language is an instance of a spec. TS spec has all of the requirements of JS spec, and some more. All TS implementations (languages) will contain JS implementations, but not vice versa. There's more JS implementations in the world, than TS implementations (assuming you can build TS as compiler/interpreter instead of transpiler).

Post reply on HN