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

So you want to write a type checker (2014)

languagengine.co

Post reply on HN
Print view View original

31–40 of 103 posts

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

#31

Post by yorwba »

labbekak wrote: post #16
amelius wrote: post #7

Perhaps I don't want to just type-check, but I want to do type-inference as well.

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. Implementation in Haskell: https://github.com/ollef/Bidirectional Implementation in Javascript/Typescript (by me): https://github.com/atennapel/bidirectional.js

ArXiv link for the paper: https://arxiv.org/abs/1306.6032

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

#32

Post by cf »

labbekak wrote: post #16
amelius wrote: post #7

Perhaps I don't want to just type-check, but I want to do type-inference as well.

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. Implementation in Haskell: https://github.com/ollef/Bidirectional Implementation in Javascript/Typescript (by me): https://github.com/atennapel/bidirectional.js

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.

My favorite starting point is actually Dunfield's lecture notes on bidirectional type checking, 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.

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

#33

Post by Cyph0n »

alkonaut wrote: post #15
dunstad wrote: post #4

Earlier quoted context omitted.

You might want to give this a look: https://github.com/Microsoft/TypeScript

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.

Why is everyone forgetting Scala.js?

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

#34

Post by dmitriid »

alkonaut wrote: post #13
madeofpalk wrote: post #9

Earlier quoted context omitted.

Why? Why be so elitist and dismissive?

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

These 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

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

#35

Post by dmitriid »

dahauns wrote: post #30
kreetx wrote: post #5

Earlier quoted context omitted.

literally :) 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).

Don't underestimate Typescript. Sure, it's somewhat restricted by the "superset of JS" property, but you still get stuff like ADTs with exhaustiveness checking.

TS doesn’t have exhaustiveness checking

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

#37

Post by alkonaut »

dmitriid wrote: post #34
alkonaut wrote: post #13

Earlier quoted context omitted.

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

These 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

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.

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

#38

Post by seanmcdirmid »

gingerb wrote: post #36

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

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

#39

Post by [deleted] »

gingerb wrote: post #36

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.

[deleted]
Post reply on HN