People sometimes ask on HN about good books on implementing programming languages.
One of the best textbooks I know on type theory is also a pretty good book for getting a programming language up and running: Types and Programming Languages by Ben Pierce.
The book starts off implementing the untyped lambda calculus and then adds more and more interesting kinds of types. There's a tarball somewhere on the course website that has all the code from the book, and it's kind of fun to play with all the systems it covers.
I recommend the paper "Complete and Easy Bidirectional Typechecking
for Higher-Rank Polymorphism" by Dunfield and Krishnaswami. It describes an easy to implement algorithm for type inference for higher ranked types that can subsume Hindley-Milner.
Your comment expanded out is what I had hoped that blogpost would have been. Thank you for posting this. It's hard to overstate how much easier bidirectional typechecking is compared to other approaches.
Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)
Indeed! Tho this is only half the problem, because `T` there includes metavariables, so it's not a type but rather a schema at the meta-level for types. What we'd like is something like `forall a b c. (b -> c) -> (a -> b) -> a -> c` so that composition can be used at arbitrary choices of the types. So like, while we can use this composition function at any particular place we need composition, we can't define `compose` to have this type because the first use site will force the metavars to have a particular value and then we get a nasty global monomorphism. We need to explicitly have metavariables in the language itself, rather than at the metalevel of doing the synthesis/checking.
mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!
That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate the quantification, I then just add that list in front of the term with the ^ operator (which has no semantics, it is just the traditional constructor for these things).
So for `_G947 -> _G947` I get the variable list `[_G947]` and use it to represent the universally quantified term as `[_G947]^(_G947 -> _G947)`. If you want to display this with nicer variable names, just substitute names of your choice for the variables in the quantifier list.
I use types.js (https://www.npmjs.com/package/types.js) dynamic type checker already for years in production without any issues. I simply don't want yet another JS syntax or transpiler only for type checking like Typescript, Flow etc.. For me that's way over the top.
Typescript was designed in such a way that the transpired mostly merely removes type annotations from the TS file to the JS one. They also went with a loose optional structural type system to be as non invasive as possible (ironically enough, it can be less strict than a nominal dynamic type system).
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.
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.
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...
My point exactly. If people who liked type systems could stand to use the JS type system (and I only barely managed to write type system without scare quotes), we wouldn't have TypeScript. Or Cofeescript. Or Purescript. Or Elm. Or Fable. Or Flow. Or even ES6.
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.
> 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.
I don't think that's a particularly good way to judge the problem though. Sure, the JavaScript example might be shorter, but which implementation is safer? Which is going to be easier to work with in the future? I'd make the assertion that the JavaScript version will have a lot more edge cases that could have been caught sooner with a more robust type system.
> 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 <languages>". This is different than "programmers generally dislike JS, as evidenced by <languages>"; 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.
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?
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 generic type.
When it comes to function parameters, typescript lets you use either. You can replace any type with any related type, even if you're going in the wrong direction. They did this to make certain use cases simpler, at the cost of weaker typing.
If a function takes an array of Animal as an argument, the "intuitive" assumption is that you can pass in a Cat[] to it since it's probably processing the array items and a Cat is an Animal.
In usual Javascript patterns, this intuition works, but it's not sound, since arrays are mutable; the function could write to the array, appending a Dog or a Potoo or a Jellyfish- valid for an Animal[] argument, but not sound for a Cat[].
In practice, in most JS code I've seen, arrays are constructed once and then are passed around as immutable collections, so Typescript's unsoundness saves a lot more casting than it introduces errors.
The real problem here is that mutable data structures aren’t entirely type sound. The solution here is to split collections into read only and mutable types, but people balk at this.
At one point long ago I did some experiments with this, and found that the most of the unique method signatures necessary to represent the data structures we are familiar with are concentrated in the mutators.
That is, the interface differences between read only data structures are pretty small. So you don’t double the surface area by splitting read from write. It’s more like 25%, and this might be partially offset by simplifications in code that has to scan multiple types of collections.
There's nothing wrong with mutable data structures from a type soundness perspective. We know how to do it properly. But you need to get the type system right in order to include mutable data structures; often people get this wrong, and it leads to all sorts of frustration...
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.
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.
It was a bit tounge in cheek. Considering that half the languages and typecheckers invented in the last decade were invented simply because the JS type system isn't what it should. Coffeescript, TypeScript, Fable, PureScript (And countless others).
- everyone’s idea of a perfect language is different
- javascript is the only viable compilation/transpilation target
Even if Javascript had the combined typing capabilities of Haskell, Agda, and Coq, there would still be people inventing/porting other languages to support client-side web development
Right - the only two things people seem to agree on is that 1) JavaScript as a target isn't going anywhere and 2) it's often nicer to not use it directly.
That's why these languages exist. Because people need to produce JavaScript and keep getting sick of writing it.
There would exist some languages that compile to javascript. But look at typescript specifically. Its compilation stage is mostly "remove the type annotations, so the browser doesn't get confused". The lack of typing is so bad that notable languages get made just to tackle that single issue.
EDIT: Oh, the hard earned karma is leaving me. :) I apologize for the irony!
In a nicer way: if you're interested in type theory then javascript is not the language to look at. I'm not even sure if typescript helps here, since the typing mechanism is fairly simple (and I don't mean it's not useful -- just not very advanced).
I know TS discriminated unions may not be the most elegant construct in the world, but in what way is the check via the never type (as a return or assertion parameter after the switch) not an exhaustiveness check?
It does. And, like in the article, Typescript is “saved by a hack”.
Compare that to Elm, where it will automatically fail compilation if you don’t include all required types in a switch statement. Without any hacks or manual intervention.
Thing is, it only works in if and switch statements, you have to be aware of it (I don’t think you can deduce it from docs), and you have to manually trigger it.
It’s ”poor man’s exhaustiveness” and TS will hopefully get better at this
I can't really agree with you. Yes, javascript is "good for what it is", but this kind of positive evaluation is only the result of that it (the language) pretty much can't be avoided when doing web development. Many things appear in a more positive light if they have been around you long enough, and you've gotten use to the experience.
I.e yes, bash is nice, but if it weren't the default shell in most systems I wouldn't ever think about switching to it voluntarily, nor be interested in learning it. It is useful because its so widely spread.
The reasons why people accuse JavaScript of being a terrible hack just never really resonated with me.
The "wat" video is funny, but that stuff just isn't a problem in my experience. Sure, I've been confused by "array.map(parseInt)" and other oddities, but overall, I think weird semantic edge cases are mostly an easy thing to nitpick about.
So as I see it, JavaScript is a nice little language with good syntax for literals (JSON, which conquered the world), a familiar brace notation, first class functions, high quality implementations, etc.
Bash's oddities are weirder, but it's also a fun and extremely useful language, and I like it a lot. Many of my coding and administration tasks involve calling programs, running background processes, piping streams around, making temporary files, globbing, etc etc, and shell scripting is still unsurpassed in convenience for these things.
I don't think js it's a hack. Yes, in the beginning there were some strange things, like objects based on prototype, referring to this, and probably more. Much of this has been worked on, and fixed (unfortunately-but-understandably keeping the old behaviors as well).
But nowdays there are many who want more-- they want types --and not only simple types, but some advanced type system. This is where it's hard to see the intersection of js "likers" and type theory "likers" -- they must have really different reasons for liking these things.
As for where the criticism towards js probably stems from is the lack of freedom -- it's the only language that runs in browser. On the server people are free to choose what to use. And yes, you can now compile other languages to js too, but reaching an agreement to use such a setup can be challenging in many workplaces.
The overlap between people who love Haskell and people who love Nix is huge, yet Nix has no static typing!
Sure, people recognize that a good static type system could improve Nix, but they also recognize that making such a thing isn't easy and that advanced type systems steepen language learning curves.
I just try to counter the meme that people have to take a side and can't simultaneously appreciate very different languages. :)
I think it's more about where are we coming from and where are we going. I have no nix experience (but know bits from reading stuff on the internet :-), but maybe the pro-nix attitude among haskellers is from a few factors: (1) referentially transparent definitions, and (2) it's better than things that have come before. I.e even with other devops/deployment scripting tools nix adds new value, and is in this sense "on it's way somewhere" (perhaps haskellization, but we'll see). So the nix people might move to the typed version when that happens.
But for languages the typed ones are already here, and have been for quite some time. So if one has stuck around with javascript then my question is why (apart from the practicality reasons).
Yeah, agreed. JavaScript doesn't really have any impressive redeeming features. I like it because it's kind of minimally viable and accidentally really useful for dealing with APIs full of duck typed nested records.
It's really hard to be both minimally viable and have a sound and expressive static type system.
Simply typed lambda calculus isn't even Turing complete, and the fate of Haskell's endless extensions indicates an inherent rabbit hole...
Haskell itself has somewhat horrible issues dealing with extensible records, and the solutions are all complex and hard to understand.
Dealing with JSON in Haskell in a quick and easy way is nowadays quite nice, but it took the invention of van Laarhoven lenses and the aeson-lens module...
I greatly prefer JavaScript to Java because I prefer no static type checking over inexpressive static type checking! And expressive type systems are hard to get right, so it's a very classic "worse is better" situation.
This is probably generally true in terms of the language itself, but one assumes that there are people that love type-theory yet also like JavaScript for its ecosystem, environment-reach and hackability.
And perhaps there are people that enjoy the difficulties in trying to type a language which is very dynamic.
They are only connected historically. But since it's obviously possible to use JS as a compilation target and only use its deployment model but none of its language quirks, they are unconnected now at least.
> It tackled the security and distribution model first, and everything else second
This is probably true. And it was also as far as I know not really "designed" to be a large scale general purpose language. It was basically invented in a short period of time to perform simple frontend tasks. Things like scoping, function resolution, module system, representation of integers etc were perhaps not the biggest concern at the time. And I'm not saying the design decisions were inherently BAD, they were probably right at the time! I'm saying the tasks we use JS for now would warrant a more thuroughly designed language. And of course ES6 is that, to a large degree - so that's good.
ES5 isn't the only language that ever outgrew it's costume. Every language that reaches enough success so it sticks around will do that eventually. Php, C etc are prime examples of languages that are used in way more places than their creators could have imagined, and as we all know a lot of times C is used because of its portability/deployment model, despite being a very flawed tool for the task.
> And I’m a little hurt that you think my code is laughable. I write exclusively in ES5. Maybe read my code first and then insult me.
I don't think anyones code is laughable, and I haven't seen yours so can't comment on it. I said there are aspects of ES5 the language that make me laugh (and cry). Function resolution, scoping rules, integer representation, equality rules, ...
> Don’t just laugh at us like an asshole.
> I’m not trying to insult your code without having read it.
I hope not, but you are free to bash any language I use to write my code all you want and I won't upset about it, and I definitely won't think you are an asshole if you do. I hate tons of aspects of my 9-5 lanugage (C#) and I'd be delighted to discuss it.
The simplicity of ES5 is exactly why it is everywhere. It tackled the security and distribution model first, and everything else second.
And I’m a little hurt that you think my code is laughable. I write exclusively in ES5. Maybe read my code first and then insult me. But do it in a substantive way. Don’t just laugh at us like an asshole.
I’m not trying to insult your code without having read it.
My point was: all those typecheckers and languages are there because the people who like types and javascript go off and write a typechecker or language. So they don't have to deal with javascript types.
I understand your point, it's simply wrong. If those people didn't want to use javascript, they could have migrated to something else altogether. Clojurescript, Elm, Dart, RustJs, ...
Instead they kept Javascript with a type system on the top (typescript, purescript, flow, ...).
Some are supersets of JS, some are not. Elm, Fable, etc are examples of languages not just extensions.
The reason for using an extension/superset is usually not because JS is terrific but because gradual/partial migration and interop are more important than a better language.
Before anyone points it out: Fable isn't a lanugage, it's an F#->JS compiler. It's "programming JS without programming in JS" though, so it's another language used in that sense.
One of the best textbooks I know on type theory is also a pretty good book for getting a programming language up and running: Types and Programming Languages by Ben Pierce.
https://mitpress.mit.edu/books/types-and-programming-languag...
The book starts off implementing the untyped lambda calculus and then adds more and more interesting kinds of types. There's a tarball somewhere on the course website that has all the code from the book, and it's kind of fun to play with all the systems it covers.