Live data from Hacker News

So you want to write a type checker (2014)

languagengine.co

61–70 of 103 posts

Re: So you want to write a type checker (2014)

#61

Earlier quoted context omitted.

TypeScript, the language which only just this month added a flag to turn off their completely incorrect subtyping rules for functions! A flag! I remember reporting this bug years ago, and they said it was "by design, since JS programmers prefer to think of functions as covariant in their input". Well, I prefer to think of 2+2 as equalling 5.

I don't know nearly enough about type systems to understand this. Can you explain what subtyping rules are, and how TypeScript's are wrong? And can you explain what "covariant in their input" means?

Suppose you have a type hierarchy where a Tabby is a type of Cat that is a type of Animal.

Now, say you have a function that takes a Cat as an argument and returns a Cat. What types can you use instead of the Cats and still remain type safe? Well, you could pass in a Tabby or return a Tabby and everything would be fine. This is a subtype rule that the compiler can check.

What about something a little trickier? Say you have a map function that maps from a list of Cats to another list of Cats. The map function takes two arguments: a list of Cats and an arbitrary function that takes a Cat and returns a Cat. For each item in the input list, the function is called on it and the returned Cat is added to the output list.

Now, can we replace the Cat to Cat input function with a function that has different types and still have the types make sense?

Let's try a function that takes a Tabby as an argument and returns a Cat (usually denoted Tabby->Cat). This won't work as we could have something that isn't a Tabby in the input list. What about a function Animal->Cat? This would work OK as every Cat in the input list is also an Animal.

Similarly, what if we try a Cat->Tabby function? This would work too as a Tabby is always a Cat. What about Cat->Animal? No, as it might produce a Dog and we only want Cats.

Notice the difference between the arguments and return types? For arguments we can replace a Cat with an Animal but, for returns, we can only go the other way. We say that we are contravariant in the argument type but covariant in the return type.

There are other forms. We say we are invariant if we can't change the type from the original stated type. We say we are bivariant if we can replace Cat with either Animal or Tabby.

So, what did Typescript do wrong? As I understand it, Typescript was (is?) bivariant in both argument and return types. This means that the type system would, say, accept a Tabby->Cat function for a Cat->Cat function argument and then fail at runtime.

Is this a heinous crime? A matter of opinion I guess. It's definitely wrong from a type system perspective but plenty of type systems let this sort of thing pass and are successful.

BTW this subtyping complexity isn't just for function arguments. It's also an issue with collection types e.g. what can yuo replace a list of Cats with? But this comment is way too long already.

Re: So you want to write a type checker (2014)

#62
post #41
post #23

Earlier quoted context omitted.

What's wrong with TypeScript?

I'm having a hard time discerning his point based on the languages he listed. I think his point was that the type theorists weren't fans of JS so they built languages that compiled to it, but CoffeeScript and ES6 don't have type systems either, so either he isn't very familiar with the languages he listed or he's making a different point.

> CoffeeScript and ES6 don't have type systems either

All languages have type systems. Including ES5, ES6 and CoffeeScript. They might be weak and dynamic but they are type systems none the less.

> I think his point was that the type theorists weren't fans of JS

I'm fairly sure that's the case (no data though)

> or he's making a different point.

My point was (a bit toungue in cheek) that seeing how many alternatives that keep popping up for avoiding JS (the language), it seems that a lot of people who like programming languages to the point where they can create one, do not like JS.

Re: So you want to write a type checker (2014)

#63

Earlier quoted context omitted.

Covariant: A variable needs to have an Animal. You can put a Cat in the variable. Contravariant: A variable needs to have a function that accepts Animals. You can't put a function that accepts only Cats, or it will crash on other kinds of animal. But you can put a function that accepts all LivingThings. So when something is covariant you can use a more specific type, and when it's contravariant you can use a more gen…

That helps, thanks. Can you explain the naming? What sort of variance is the second case contra?

The first one is the more natural one, and so the opposite gets to be "contra", I think.

Re: So you want to write a type checker (2014)

#64
post #41

Earlier quoted context omitted.

I'm having a hard time discerning his point based on the languages he listed. I think his point was that the type theorists weren't fans of JS so they built languages that compiled to it, but CoffeeScript and ES6 don't have type systems either, so either he isn't very familiar with the languages he listed or he's making a different point.

> CoffeeScript and ES6 don't have type systems either All languages have type systems. Including ES5, ES6 and CoffeeScript. They might be weak and dynamic but they are type systems none the less. > I think his point was that the type theorists weren't fans of JS I'm fairly sure that's the case (no data though) > or he's making a different point. My point was (a bit toungue in cheek) that seeing how many alternatives…

Hi. I'm interested in type theory, and I'm a big fan of JS.

shrug

Is it really so hard to believe? Imagine if the browser's scripting language didn't have closures or prototypical inheritance. It was possible.

JS was a pretty good compromise between power and simplicity.

Re: So you want to write a type checker (2014)

#65

Earlier quoted context omitted.

Covariant: A variable needs to have an Animal. You can put a Cat in the variable. Contravariant: A variable needs to have a function that accepts Animals. You can't put a function that accepts only Cats, or it will crash on other kinds of animal. But you can put a function that accepts all LivingThings. So when something is covariant you can use a more specific type, and when it's contravariant you can use a more gen…

Which use cases are those?? Are any of them actually real life, practical use cases?

https://github.com/Microsoft/TypeScript-Handbook/blob/master...

The example seems like a valid case. The type of event is expressed in a separate parameter, so being strict here requires pointless casting and doesn't actually make things safer.

Whether you think this type weakness is worth the downsides is up to you.

Re: So you want to write a type checker (2014)

#66
post #2

Venn diagram of people who are interested in type theory, and people who like Javascript... OO

Snarky one-liners aren't good comments for Hacker News. You can always say something substantive instead, and then we have a much higher chance of an insightful discussion.

https://news.ycombinator.com/newsguidelines.html

Re: So you want to write a type checker (2014)

#67
post #66
post #2

Venn diagram of people who are interested in type theory, and people who like Javascript... OO

Snarky one-liners aren't good comments for Hacker News. You can always say something substantive instead, and then we have a much higher chance of an insightful discussion. https://news.ycombinator.com/newsguidelines.html

It's snarky but I think the replies constitute a perfectly good discussion and there's no reason to collapse all of it by default. It's a bit off-topic but out of the five current top-level comments only one is addressing the contents of the article anyway...

Re: So you want to write a type checker (2014)

#68
post #66
post #2

Venn diagram of people who are interested in type theory, and people who like Javascript... OO

Snarky one-liners aren't good comments for Hacker News. You can always say something substantive instead, and then we have a much higher chance of an insightful discussion. https://news.ycombinator.com/newsguidelines.html

I'm sorry for not meeting the standards. I think it did spark insightful discussion. I thought it was going to cost a few dozen in karma but apparently didn't. So not everyone thought it was terrible I guess.

In my experience the amount of insightful discussion is often inversely proportional to the quality of the initial post. Have no data to back that up.

There is a fine line between flamebait and discussion-bait.

Re: So you want to write a type checker (2014)

#69
post #41

Earlier quoted context omitted.

I'm having a hard time discerning his point based on the languages he listed. I think his point was that the type theorists weren't fans of JS so they built languages that compiled to it, but CoffeeScript and ES6 don't have type systems either, so either he isn't very familiar with the languages he listed or he's making a different point.

> CoffeeScript and ES6 don't have type systems either All languages have type systems. Including ES5, ES6 and CoffeeScript. They might be weak and dynamic but they are type systems none the less. > I think his point was that the type theorists weren't fans of JS I'm fairly sure that's the case (no data though) > or he's making a different point. My point was (a bit toungue in cheek) that seeing how many alternatives…

> All languages have type systems. Including ES5, ES6 and CoffeeScript. They might be weak and dynamic but they are type systems none the less.

I understand; I was speaking colloquially. No need to be pedantic.

> My point was (a bit toungue in cheek) that seeing how many alternatives that keep popping up for avoiding JS (the language), it seems that a lot of people who like programming languages to the point where they can create one, do not like JS.

Your original post focused on type systems specifically. It seemed something like "type theorists dislike JS, as evidenced by ". This is different than "programmers generally dislike JS, as evidenced by "; however, to focus on your latter claim, I don't think your claim follows the evidence--the most we can say is that many programmers dislike JS; however, I don't think this is a particularly useful observation, since every domain has many candidate languages, and relatively few domains are trending toward consensus. It seems like the most meaningful conclusion is "programmers have diverse tastes, projects have diverse priorities, and many of those tastes/priorities are mutually exclusive (there are no languages that are good for learning curve and maximizing performance, for example). This conclusion is not necessarily surprising, but I think it's the most interesting claim we can derive from the stated evidence.

Re: So you want to write a type checker (2014)

#70

Earlier quoted context omitted.

> CoffeeScript and ES6 don't have type systems either All languages have type systems. Including ES5, ES6 and CoffeeScript. They might be weak and dynamic but they are type systems none the less. > I think his point was that the type theorists weren't fans of JS I'm fairly sure that's the case (no data though) > or he's making a different point. My point was (a bit toungue in cheek) that seeing how many alternatives…

Hi. I'm interested in type theory, and I'm a big fan of JS. shrug Is it really so hard to believe? Imagine if the browser's scripting language didn't have closures or prototypical inheritance. It was possible. JS was a pretty good compromise between power and simplicity.

> Hi. I'm interested in type theory, and I'm a big fan of JS.

fan of JS as a whole package (Language, ecosystem, ...) or JS only as a language? The whole package is very attractive, and I can see how people accept ES5 (the language) for the opportunity to work with JS the ecosystem.

JS the language I think has some cool features and with ES6 it's even an acceptable language to work with, but I just fail to come to terms with some of the smaller warts. The feeling I'm looking for in a language is "this is carefully designed to be consistent, simple and free of idiosyncraces and suprises". With equality, scoping, coercions etc in ES5 that realy is NOT the feeling. ES6 is so much better, but once you pick an ES5 alternative there are so many other choices.

> JS was a pretty good compromise between power and simplicity.

I really don't get why people think JS is "simple" though. It's fantastically complicated. Mostly accidentally though., because of the little warts in scoping/equality/coercion etc. Again, ES6 is a lot better - but still very very not simple compared to e.g. Java.

Post reply on HN