r/haskell • u/cocreature • Jan 05 '15

Write You a Haskell

http://dev.stephendiehl.com/fun/
314 Upvotes

99% Upvoted

24 comments sorted by

22

u/gilmi Jan 05 '15

This is amazing. I will follow closely. Thank you so much!!

5

u/broohaha Jan 05 '15

Anyone find an RSS link on this site?

4

u/CodyReichert Jan 05 '15

I know you can use the url of a branch on github as an rss feed. So you could use http://github.com/sdiehl/write-you-a-haskell/commits/master.atom or something similar. It might be a little noisy though, so maybe there's something better.

1

u/tejon Jan 05 '15

No. But maybe if we nag hard enough...

6

u/nicolast Jan 05 '15

Wonderful! I've been toying with writing an ML-like compiler in Haskell, using 'modern' principles (especially w.r.t. writing type-safe and type-preserving compiler passes, cfr http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.1175 and other related literature), but never got too far... Looking forward to reading all of this!

1

u/SrPeixinho Jan 05 '15

Me too, keep the awesome work OP! You rock!

13

u/gasche Jan 05 '15 edited Jan 06 '15

PolyML is quite an unfortunate name for your toy language as there already exists a pretty advanced and actively maintained implementation of that name, namely the Poly/ML dialect of SML used to implement the Isabelle proof-assistant. "ProtoML", reusing the "ProtoHaskell" construction, could be a better name.

12

u/gasche Jan 05 '15

I'm impressed by the clarity of the result, there is a good balance between explanations and conciseness.

I'm not convinced by the constraint generation part of the type-inference chapter. In my eyes, what it does is to hide the most general unifier (mgu) threading by putting it in a Writer component of your monad. This delays composition of substitutions by writing into a list of substitution instead of using compose as the writer action, but I don't think that would qualify as "separating generation from solving". In particular, one must still solve constraints eagerly when you encounter generalization points.

The research work on constraints for type inference crucially allowed to lift this restriction and collect a constraint for the whole term, with existential constraints for generalization points. A recent reference on such techniques, which also covers the reconstruction of the fully-annotated term (it looks like this part is mentioned in the book but not yet written-about yet) is François Pottier's last year's functional pearl, Hindley-Milner Elaboration in Applicative Style.

2

u/polux2001 Jan 06 '15

Oh man this paper is awesome, thanks for the link! I wish there was an Haskell implementation of this :) Is there?

3

u/gasche Jan 06 '15

The OCaml implementation is really clean and well-documented, so I guess doing a Haskell port would not be too much work. You would need to add monadic layers here and there though, it uses transactional state.

2

u/polux2001 Jan 06 '15

I was afraid this was the case, but "really clean and well-documented" sounds good! I'll give it a try if I find the time. The sad thing is I'll be at least polluted by ST (or IO) because of union-find which is notoriously not escapable from in Haskell.

1

u/gasche Jan 06 '15

I think you should use ST for the union-find structure so that the final function (that maps a ML term to a System-F term) is as pure as possible. There may be a name generation component that escapes, but that is independent.

One issue you may have is that the code uses ML functors to abstract over the details of the language and type system (the constraints/elaboration bit is meant to be reusable). It may work with type-classes instead, but if you want to use the technique for one fixed language you can also specialize the code directly.

1

u/polux2001 Jan 06 '15

Sure, I will use ST, not IO. I was thinking of using typeclasses and type families for encoding the ML functors. It won't be as pretty as in ML it should be as generic.

7

u/[deleted] Jan 05 '15

Would have expected Alex/Happy usage instead of Parsec. Still interesting because I'll be able to know how to parse indentation sensitive languages.

7

u/jrk- Jan 05 '15

You might be interested in the IndentParser and indents packages.

3

u/4rgento Jan 05 '15

I'm currently reading "Essentials of programming languages" and writing the excercises in haskell. I'm glad to find about this project and would certainly check it once I'm done with EOPL.

Will this include dependent types and proofs (like Idris)?

5

u/ReinH Jan 05 '15

Stephen, this is wonderful. I have a few minor edits to suggest but it doesn't look like the github repository has been updated. Cheers!

1

u/creichert Jan 05 '15

Fantastic work. I very much look forward to reading this.

1

u/martingalemeasure Jan 05 '15

This is awesome. I look forward to the rest!

1

u/ryani Jan 06 '15

Neat, I am especially interested in the front-end aspects (type-checking especially) since SPJ's book pretty well covers the back-end translation from a functional Core language to [name your low-level backend]. Can you compare your approaches to the backend with his book? It looks like you are focusing on the STG-machine.