4 ms·

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 dynami

by jnbiche 13y ago

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

m_mueller 13y ago
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.
- jnbiche 13y ago
  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.
  - m_mueller 13y ago
    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.
tomp 13y ago
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 https://github.com/typeclassy/plzoo
- jnbiche 13y ago
  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.
gmfawcett 13y ago
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-concatenative-languages.html http://alaska-kamtchatka.blogspot.ca/2009/01/essence-of-conc...
mcmillhj 13y ago
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.
- jnbiche 13y ago
  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.
Nav_Panel 13y ago
Here's a different book you might be interested in ("Practical Foundations for Programming Languages": http://www.cs.cmu.edu/~rwh/plbook/book.pdf 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 http://www.cs.cmu.edu/~rjsimmon/15312-s14/index.html if you want to check out what we're working on.
- oggy 13y ago
  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?
  - notthemessiah 13y ago
    Pierce will get you working in Coq ASAP, but Harper will provide you with a much richer context.
    - me2i81 13y ago
      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 http://www.cis.upenn.edu/~bcpierce/sf/index.html
  - tel 13y ago
    I'd be interested in this as well. I'm about halfway through TaPL and have often considered reading Harper's book instead.
jbclements 13y ago
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/ 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.

by jnbiche 13y ago

m_mueller 13y ago

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.

jnbiche 13y ago
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.
- m_mueller 13y ago
  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.

tomp 13y ago

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 https://github.com/typeclassy/plzoo

jnbiche 13y ago
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.

gmfawcett 13y ago

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-concatenative-languages.html http://alaska-kamtchatka.blogspot.ca/2009/01/essence-of-conc...

mcmillhj 13y ago

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.

jnbiche 13y ago
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.

Nav_Panel 13y ago

Here's a different book you might be interested in ("Practical Foundations for Programming Languages": http://www.cs.cmu.edu/~rwh/plbook/book.pdf 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 http://www.cs.cmu.edu/~rjsimmon/15312-s14/index.html if you want to check out what we're working on.

oggy 13y ago
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?
- notthemessiah 13y ago
  Pierce will get you working in Coq ASAP, but Harper will provide you with a much richer context.
  - me2i81 13y ago
    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 http://www.cis.upenn.edu/~bcpierce/sf/index.html
- tel 13y ago
  I'd be interested in this as well. I'm about halfway through TaPL and have often considered reading Harper's book instead.

jbclements 13y ago

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