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

Show HN: Hindley-Milner Type Inference Algorithm in OCaml

github.com

Post reply on HN
Print view View original

21–30 of 30 posts

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#21

Post by eric_bullington »

krat0sprakhar wrote: post #3
kragen wrote: post #2

This is cool! It's nice to have a bite-sized runnable illustration of HM. Maybe I will finally be able to understand it — both the code and the linked lecture notes ( http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec... ) look pretty informative. I don't think I can digest it in time to comment before it scrolls off the HN front page. It's a little unfortunate that this version doesn't include let-polymorp…

Thanks for the feedback! This is actually a smaller part of a much bigger full-blown type-inferred programming language[0], we've been working on as a part of course in school. Our plan was to directly add type-inference in the language but after reading through Stephen Diehl's tutorial[1] we were intimidated and wanted to have a working version on a bite-sized language. I'm assuming a lot developers like me would be…

> Would you be interested in something along those lines?

Yes! That would be very cool to read.

I've been working on an implementation of Mini-ML in Python using Robert Small's Hindley-Milner in Python [0] (and also eagerly awaiting the rest of Diehl's series on writing a Haskell).

I understand the fundamentals of the algorithm, but even now I don't think I could yet implement it from scratch. I'd love to read a detailed tutorial.

By the way, those Cornell lecture notes you referenced have also been very helpful to me.

0. http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind...

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#23

Post by eric_bullington »

igravious wrote: post #17
kragen wrote: post #12

Earlier quoted context omitted.

I don't know if I understand unification well or not; I feel like the control flow in Algorithm W is still a bit of a mystery to me, but I suspect that this is more a function of the effort I've put into understanding it than of the adequacy of the explanations I've found. http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my underst…

I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous…

> I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/…

I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon.

As such, I've come across a few good resources:

check out Robert Small's Hindley-Milner in Python[0], as well as alehander42's Hermetic language in Python[1].

I also just found out about Hask, an implementation of many Haskell language features in Python. Looking at the source code, it's well-commented and clear, so I suspect I'll learn a lot from it as well [2].

Finally, even though it's not in a dynamic or non-functional language like you request, I highly recommend Andrej Bauer's Programming Language Zoo[3], which contains very simple and easy-to-understand implementations of various type systems in OCaml. Very elucidating.

0. http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind...

1. https://github.com/alehander42/hermetic

2. https://github.com/billpmurphy/hask

3. http://andrej.com/plzoo/

Edit: Oh, and one more resource that's been extremely helpful has been "Introduction to Functional Programming through Lambda Calculus" by Michaelson. Well worth the cost of the book.

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#24

Post by igravious »

eric_bullington wrote: post #23
igravious wrote: post #17

Earlier quoted context omitted.

I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous…

> I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/… I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon. As such, I've come…

Brilliant, I'm attempting something very similar in Ruby :)

Will check out those links.

When I have something workable, I'll post it to Github as well and then we can see about creating some kind of umbrella structure?

A related idea I have is that what is needed is some kind of grammar interchange format, or typing-relation interchange format -- kind of like JSON (or Amazon's ION) but for this sort of work. In some ways that is what S-expressions are, maybe there is no need to reinvent the wheel but my hunch is that a domain specific format is needed. Apologies if this is a bit vague, it's a hunch, and I'm going by intuition.

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#25

Post by eric_bullington »

igravious wrote: post #24
eric_bullington wrote: post #23

Earlier quoted context omitted.

> I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/… I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon. As such, I've come…

Brilliant, I'm attempting something very similar in Ruby :) Will check out those links. When I have something workable, I'll post it to Github as well and then we can see about creating some kind of umbrella structure? A related idea I have is that what is needed is some kind of grammar interchange format, or typing-relation interchange format -- kind of like JSON (or Amazon's ION) but for this sort of work. In some…

Check out RAML: https://github.com/raml-org/raml-spec Maybe it will fit the bill? It can even encode sum types. But I'm not sure if that's what you're looking for.

I'll ping you when I put my mini-ml in Python on Github.

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#26

Post by sklogic »

igravious wrote: post #17
kragen wrote: post #12

Earlier quoted context omitted.

I don't know if I understand unification well or not; I feel like the control flow in Algorithm W is still a bit of a mystery to me, but I suspect that this is more a function of the effort I've put into understanding it than of the adequacy of the explanations I've found. http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my underst…

I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous…

> an implementation in either a dynamically typed language

ML in Lisp and Prolog:

https://github.com/combinatorylogic/mbase/tree/master/src/l/...

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#27

Post by igravious »

eric_bullington wrote: post #25
igravious wrote: post #24

Earlier quoted context omitted.

Brilliant, I'm attempting something very similar in Ruby :) Will check out those links. When I have something workable, I'll post it to Github as well and then we can see about creating some kind of umbrella structure? A related idea I have is that what is needed is some kind of grammar interchange format, or typing-relation interchange format -- kind of like JSON (or Amazon's ION) but for this sort of work. In some…

Check out RAML: https://github.com/raml-org/raml-spec Maybe it will fit the bill? It can even encode sum types. But I'm not sure if that's what you're looking for. I'll ping you when I put my mini-ml in Python on Github.

That's not really what I mean. Take the file `parser.mly` from http://andrej.com/plzoo/html/miniml.html . See how it has it's own format for describing grammars. So does Yacc, so does X, Y, and Z. Is there an interchange format for parser generators?

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#28

Post by igravious »

eric_bullington wrote: post #23
igravious wrote: post #17

Earlier quoted context omitted.

I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous…

> I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/… I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon. As such, I've come…

Hermetic is amusing. Hask is very like what I'm aiming towards, not PLZoo. I'm starting with a PEG library (https://kschiess.github.io/parslet/) and working my way up. I'd prefer to start with a GLL parser which could handle mildly context-sensitive grammars and work my way up but I think creating a PEG version as a proof of concept is the way to go first.

Thanks for the book reference!

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#29

Post by mattydoincode »

I actually did a school project that was very similar for a compilers class! It was also Hindley-Minler in Ocaml and we tried to basically stuff any random features of a programming language we could into one language, and just compile it to java (because you can do anything with java).

Here is the paper we did: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... and the full information is available here: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... our project was called "pubCrawl".

Re: Show HN: Hindley-Milner Type Inference Algorithm in OCaml

#30

Post by kragen »

igravious wrote: post #27
eric_bullington wrote: post #25

Earlier quoted context omitted.

Check out RAML: https://github.com/raml-org/raml-spec Maybe it will fit the bill? It can even encode sum types. But I'm not sure if that's what you're looking for. I'll ping you when I put my mini-ml in Python on Github.

That's not really what I mean. Take the file `parser.mly` from http://andrej.com/plzoo/html/miniml.html . See how it has it's own format for describing grammars. So does Yacc, so does X, Y, and Z. Is there an interchange format for parser generators?

There's BNF, and there's DFDL, and there's just plain lists of productions without the extra decorations in BNF, but basically no. The issue is that each parser generator in current wide use has its particular funky set of limitations that you have to hack around one way or another when you write the grammar for it: it can't handle left recursion, or right recursion, or ambiguity, except in certain special cases (maybe if it doesn't continue for more than one token, or two syntax-tree levels), or it can handle them but has potentially exponential runtime, or it just arbitrarily resolves them in a certain way which may be adequate for your needs or may require you to restructure the grammar, or whatever. And then there are lots of ways that our languages aren't quite context-free, and different parsing systems have different ways to shoehorn that into a basically context-free framework.

I think it's maybe a solvable problem, but I haven't seen anyone try to solve it.

Post reply on HN