Hacker News Reader

Comment by tomp | Hacker News Reader

In the last chapter, Bonus Projects, the author mentions Static Typing & type systems. If anyone's interested in learning more:

I've implemented a few simple implementations of basic (and not so basic) type systems[1]. Currently, only 3 type systems are finished (Hindley Milner's Algorithm W, and Daan Leijen's extensible rows and first-class polymorphism), while gradual typing is almost done (based on [2], in branch 'dev').

[1] https://github.com/tomprimozic/type-systems

[2] Jeremy G. Siek, Manish Vachharajani - Gradual Typing with Unication-based Inference - http://ecee.colorado.edu/~siek/dls08igtlc.pdf

View on HN

Oh wow! This is extremely useful, thank you. I've been wanting to develop my own statically-typed language, but almost all tutorials on the web are for dynamic languages with little mention given to type systems. I've already started a toy dynamically-typed language, but the step up from that to a static language seems significant, particularly given the dearth of information I can find on the web (aside from dense academic papers).

I know the dragon book probably covers this, but I can't justify spending 130 USD on a book at the moment.

And I'm working in OCaml, so this is perfect.

Please consider putting out a donation link so people can support your work (Bitcoin would be most convenient for me, but I'll definitely try to donate regardless).

Also, some kind of open source license would be great (MIT or BSD, maybe?).

Something that might be useful for you: I've heard a talk where the speaker described how F# allows defining one's own type system as an input to the compiler. The language is apparently very extendible this way. It's also open source but I can't find information about its license just now. If I were to build a custom type system that's probably where I'd start to look at, even though I'm not a .NET developer.

Hmm, maybe he was talking about type providers? These let you "customize" F# (kind of like macros) but not really implement a new language.

But I'd definitely be interested in that talk if you can remember the name of the speaker or the venue/conference so I can try to Google it.

It was "S4174 - How to Design a Language Integrated CUDA Compiler with LLVM" at the GTC 2014. Videos should be up in a month or so.

Well, the purpose of this project is purely to experiment with type systems, so this is far from a programming language (e.g. in a real compiler, you would want to save file/line information for AST nodes, so that the type-checker can report an error, not simply abort. Also, a compiler would not just type-infer/check the AST, but would annotate the AST with inferred types, so that they can be used in later stages (optimization, ...)). Shoot me an email if you need help with something. Also, check out [1].

> Please consider putting out a donation link so people can support your work (Bitcoin would be most convenient for me, but I'll definitely try to donate regardless).

I'd prefer comments/bugs/interesting discussion.

> Also, some kind of open source license would be great (MIT or BSD, maybe?).

I'll do that ASAP, in the meantime, it's public domain/CC-whatever, with the exception of file first_class_polymorphism/propagate.ml and propagation of types tests in first_class_polymorphism/test_infer.ml and first_class_polymorphism/test_infer.ml, which are heavily inspired by Daan Leijen's reference implementation.

[1] https://github.com/typeclassy/plzoo

Oh, I know this project wasn't to create an entire compiler. But it's a great explanation of a missing puzzle piece in my own project.

Hope I didn't offend by suggesting donations -- wasn't my intent.

Anyway, thanks again for putting this out there. It will be a big help.

Edit: Wow, plzoo is another great resource, thank you. I found a reference to the plzoo project and website at one point but the site itself no longer seems operational ("no one here but us chickens", it says) and I didn't think the source code would be available anywhere. Very happy to see it's up on github.

You might also enjoy Matías Giovannini's write-up of a typed concatenative language in Ocaml:

http://alaska-kamtchatka.blogspot.ca/2009/01/essence-of-conc...

You can get a used copy of the Dragon book for relatively cheap. The PDF is probably floating around on the internet somewhere as well.

Yeah, I'm always cautious about pirated pdf's floating around the net, since they frequently carry malware. Probably not an issue for Linux systems, but I prefer not to take a chance.

I'd definitely pick up a used copy of the Dragon book if I could find one for a reasonable price. Unfortunately, this book is used frequently in college CS courses, so the demand for used copies stays high, and so does the price.

Here's a different book you might be interested in ("Practical Foundations for Programming Languages":

http://www.cs.cmu.edu/~rwh/plbook/book.pdf

It gets pretty math-heavy at times, at least in the beginning (you can probably skip the first chapter if it's too rough), but ultimately the book is about programming language design and different ways of designing and evaluating typed (or un(i)typed) languages. It also looks at a large number of important languages including PCF, Typed/Untyped Lambda Calculus, System F, Gödel's T and ALGOL (the last of which is interesting because it uses what we now call the IO Monad).

I'm taking the class (15-312) right now, and as homework we typically implement an interpreter for some language using SML (OCaml would likely work fine for the general use case), and then prove a few things about the language. Our languages rely on our Abstract Binding Tree (ABT) infrastructure that we developed early on in the course. You can find the course page at http://www.cs.cmu.edu/~rjsimmon/15312-s14/index.html if you want to check out what we're working on.

I've been wanting to read that for a while. Another candidate is Pierce's "Types and Programming Languages". Has anybody by any chance read both an can compare them?

I'd be interested in this as well. I'm about halfway through TaPL and have often considered reading Harper's book instead.

I've read both and Pierce is much better. I have nothing but respect for Robert Harper, a great thinker in this space, but Pierce is a better writer.

Pierce will get you working in Coq ASAP, but Harper will provide you with a much richer context.

TAPL isn't Coq-focused. Pierce and his collaborators have another book available online, Software Foundations, which is written as a Coq literate program: http://www.cis.upenn.edu/~bcpierce/sf/index.html

PFfPL is a great book. It manages to present many seemingly different language features in a surprisingly unified way.

It's very opinionated at times (usually against anything "dynamic", eg. typing and binding ;) ) but I think it's worth it for the clarity that it allows. Of course, Bob Harper has the clout to back up those opinions!

I try to take a break from proving progress and preservation by reading hackernews and of course I find someone talking about 15-312 :/ Either way, I would agree with you in recommending the text.

Looks like no one's mentioned Benjamin Pierce's authoritative book on this, "Types and Programming Languages" (TAPL). I would certainly put it way, way above the Dragon Book. Bob Harper can certainly defend his opinions as well as anyone, but I think Pierce is currently the standard text here.

Also, if you're looking to add a static type system to a Lisp-like language, you should take a look at Shriram Krishnamurthi's Programming Languages and Interpretation, second edition, at http://cs.brown.edu/courses/cs173/2012/book/ . It's a free online book, and I'm currently using it as the text in my programming languages class.

Holy shit. I've been looking for something like this! I had a difficult time understanding Siek's gradual typing papers without any code.

Yeah, me too... it's not an easy paper, the algorithm is quite convoluted, and it took me a while to understand... I'll add some explanation of the basic idea and my version of the algorithm.

Thanks for that paper, I'm currently designing a language and I'm wondering if I should use static or gradual typing. I'm currently doing static, but I want to investigate gradual. Anyway thanks! And I'll check out your code too...

I hope you find it useful. Also, I don't know what kind of language you're designing, but if it's an object oriented language, you might be more interested in some other papers on gradual typing, for example:

[1] J Siek, W Taha - Gradual Typing for Objects - http://www.cs.colorado.edu/~siek/gradual-obj.pdf [2] T Wrigstad, FZ Nardelli, S Lebresne, J Östlund, J Vitek - Integrating Typed and Untyped Code in a Scripting Language - https://www.cs.purdue.edu/homes/jv/pubs/popl10.pdf [3] A Rastogi, A Chaudhuri, B Hosmer - The Ins and Outs of Gradual Type Inference - http://www.cs.umd.edu/~avik/papers/iogti.pdf

Reply on news.ycombinator.com