10 ms·
So you want to write a type checker (2014)
- alkonaut 9y agoVenn diagram of people who are interested in type theory, and people who like Javascript... OO
- mbrock 9y agoraises hand There are dozens of us!
- kreetx 9y agoliterally :) 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).
- mbrock 9y agoWell, it's kind of like "if you're interested in type theory then bash will not arouse your intellectual curiosity." Sure, but it's still a practical and kind of necessary part of the world, and if you take it for what it is, it's pretty nice.
- kreetx 9y agoI 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.
- mbrock 9y agoThe 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.
- kreetx 9y agoI 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.
- mbrock 9y agoThe 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. :)
- dahauns 9y agoDon't underestimate Typescript. Sure, it's somewhat restricted by the "superset of JS" property, but you still get stuff like ADTs with exhaustiveness checking.
- dmitriid 9y agoTS doesn’t have exhaustiveness checking
- dahauns 9y agoI 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?
- dmitriid 9y ago“exhaustiveness checking”: automatically making sure that we’ve covered all of the possible cases anywhere that we interact with a piece of data [1] Typescript doesn’t do that. There’s a way to manually force exhaustive checking with discriminating unions: https://github.com/basarat/typescript-book/blob/master/docs/types/discriminated-unions.md https://github.com/basarat/typescript-book/blob/master/docs/... However, it’s a manual workaround. [1] Quoted from http://www.adamsolove.com/js/flow/type/2016/04/15/flow-exhaustiveness.html http://www.adamsolove.com/js/flow/type/2016/04/15/flow-exhau...
- dahauns 9y agoHm? Typescript actually uses the same mechanism for exhaustiveness checking as flow (like your link describes).
- dmitriid 9y agoIt 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.
- TeMPOraL 9y agoExactly. On the diagram: OO you're part of the boundary between two O-s that renders on a cleartype-enabled screen! :).
- dunstad 9y agoYou might want to give this a look: https://github.com/Microsoft/TypeScript https://github.com/Microsoft/TypeScript
- vladimir-y 9y agoit's more than just a type checker
- alkonaut 9y agoMy 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.
- spacetexas 9y agomaybe because browsers and backwards compatibility exist and we cant just change the language as we please?
- hasenj 9y agoWhat's wrong with TypeScript?
- alkonaut 9y agoI haven't used it enough to have a detailed opinion but from what I can see it looks like an excellent language.
- CapacitorSet 9y agoEh, there's still TypeScript and Flow. Myself, I'm a fan of the latter.
- alkonaut 9y agoMy 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. Typescript and Flow are two such examples.
- monsieurbanana 9y agoI 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, ...).
- Double_a_92 9y agoDart could have been so beautiful T_T
- alkonaut 9y agoSome 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.
- alkonaut 9y agoBefore 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.
- madeofpalk 9y agoWhy? Why be so elitist and dismissive?
- colejohnson66 9y agoI thought it was a joke
- rexpop 9y ago...at whose expense?
- alkonaut 9y agoIt 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).
- monsieurbanana 9y agoWhat does Coffeescript has to do with typing systems?
- dmitriid 9y agoThese languages exist because: - people want to target browsers - 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
- alkonaut 9y agoRight - 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.
- avodonosov 9y agoNot true
- lhnz 9y agoThis 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.
- alkonaut 9y agoYes the deployment model of js runtimes is second to none. As are the runtimes themselves. The ecosystem is vibrant (though perhaps a bit chaotic) JS the language (ES5 in particular) and its standard library is really all thats laughable about JS.
- erikpukinskis 9y agoYou say that as if the two were unconnected. 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.
- alkonaut 9y ago> You say that as if the two were unconnected. 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.
- deleted 9y ago[deleted]
- sctb 9y agoSnarky 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 https://news.ycombinator.com/newsguidelines.html
- Dylan16807 9y agoIt'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...
- sctb 9y agoOK, that's a good point. We've uncollapsed the thread.
- alkonaut 9y agoI'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.
- amelius 9y agoPerhaps I don't want to just type-check, but I want to do type-inference as well.
- labbekak 9y agoI 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. Implementation in Haskell: https://github.com/ollef/Bidirectional https://github.com/ollef/Bidirectional Implementation in Javascript/Typescript (by me): https://github.com/atennapel/bidirectional.js https://github.com/atennapel/bidirectional.js
- yorwba 9y agoArXiv link for the paper: https://arxiv.org/abs/1306.6032 https://arxiv.org/abs/1306.6032
- cf 9y agoYour 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. My favorite starting point is actually Dunfield's lecture notes on bidirectional type checking, https://people.mpi-sws.org/~joshua/bitype.pdf https://people.mpi-sws.org/~joshua/bitype.pdf The paper you mentioned is great at showing the approach scales well to giving you all the fancy features you might want that are in modern languages.
- psygnisfive 9y agoAhh, 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. :)
- junke 9y ago
- dchasson 9y agoalright hacker news, how did you know what I've been doing for 16 hours?
- AceJohnny2 9y agoHaving a good weekend? :)
- gingerb 9y agoI use types.js (https://www.npmjs.com/package/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.
- seanmcdirmid 9y agoTypescript 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).
- deleted 9y ago[deleted]
- igravious 9y agoFrom (2014) people!
- deleted 9y ago[deleted]
- psygnisfive 9y agoIt was also front page on HN at the beginning of 2015 ;)
- danblick 9y agoPeople 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. https://mitpress.mit.edu/books/types-and-programming-languages 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.
- psygnisfive 9y agoI'd also recommend Practical Foundations for Programming Languages (PFPL). And a bunch of other things, which I outlined here: So You Want To Learn Type Theory (http://purelytheoretical.com/sywtltt.html http://purelytheoretical.com/sywtltt.html)