4 ms·

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 c

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 keen to understand how HM works, so I was considering writing a detailed tutorial of the unification algorithm step-by-step. Would you be interested in something along those lines? [0] - http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/proposals/JSJS.pdf http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin... [1] - http://dev.stephendiehl.com/fun/006_hindley_milner.html http://dev.stephendiehl.com/fun/006_hindley_milner.html

BhavdeepSethi 10y ago
No link to Columbia's PLT lectures? :)
- edmob 10y ago
  Link to the PLT course home page: http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/ http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin...
kragen 10y ago
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 http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my understanding of unification at the time — but looking at it now, I see that it only does pattern-matching, which is really only kind of half of unification. I think I did a more general first-order vaguely unificationy thing for queries on triple stores some years back, but the details are now fuzzy in this thing of mine that I flatter by calling it a mind. So, yes! I'd love a detailed tutorial of unification step-by-step (or perhaps recursive function by recursive function, if that turns out to be simpler). Maybe it already exists somewhere, perhaps in a textbook, and I just haven't found it. Or maybe I got intimidated and need to calm down and work some exercises instead of going off to read Facebook and HN.
- igravious 10y ago
  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 with relational programming but is that all there is to it? The second thing I would like to say. And I've said this before. Languages like Ocaml and Haskell (never mind Agda, Coq, what have you) already have too much typing 'smarts' built into them. 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/… What think ye?
  - Peaker 10y ago
    I can try to explain why HM type inference and unification are related. If you take just the lambda calculus where you have: 1) Lambdas that bind variables 2) Usages of bound variables 3) Function applications The inference rules for the first 2 are simple & straight-forward and require no unification. For 1 (lambdas) - you create a fresh type variable (e.g: 'a') for the parameter type and infer the lambda body (e.g: 'T'), and the lambda's type is then 'a -> T'. While inferring the lambda body, you also pass the information that the parameter bound by the lambda has-type 'a'. For 2 (variable usage), you just use the known type information that was passed down by the lambda inference. For 3 (application), you need unification. Function application is between two subexpressions (e.g: 'f' and 'x'). You infer both of these recursively, and get 2 types (e.g: 'fType' and 'xType'). But you also know that 'fType' must look like: 'xType -> resType' because it's being applied to 'x'. You also know that 'resType' is the result of the entire application. So you have to unify 'fType' with 'xType -> resType'. This is why inference relates to unification: You have 2 sources of information for 'fType' and 'xType' -- the recursive inference AND the fact they're being applied together. This unification, by the way, is the only way that type information is learned for parameter types. If all parameter types are always specified (as in, e.g: C++) then formally, there's no type inference at all. So what C++ calls "local type inference" is formally just type checking.
deleted 10y ago
[deleted]
eric_bullington 10y ago
> 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-hindley-milner-type-inference-implementation-in-python/comment-page-1/ http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind...

BhavdeepSethi 10y ago

No link to Columbia's PLT lectures? :)

edmob 10y ago
Link to the PLT course home page: http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/ http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin...

kragen 10y ago

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 http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my understanding of unification at the time — but looking at it now, I see that it only does pattern-matching, which is really only kind of half of unification. I think I did a more general first-order vaguely unificationy thing for queries on triple stores some years back, but the details are now fuzzy in this thing of mine that I flatter by calling it a mind. So, yes! I'd love a detailed tutorial of unification step-by-step (or perhaps recursive function by recursive function, if that turns out to be simpler). Maybe it already exists somewhere, perhaps in a textbook, and I just haven't found it. Or maybe I got intimidated and need to calm down and work some exercises instead of going off to read Facebook and HN.

igravious 10y ago
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 with relational programming but is that all there is to it? The second thing I would like to say. And I've said this before. Languages like Ocaml and Haskell (never mind Agda, Coq, what have you) already have too much typing 'smarts' built into them. 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/… What think ye?
- Peaker 10y ago
  I can try to explain why HM type inference and unification are related. If you take just the lambda calculus where you have: 1) Lambdas that bind variables 2) Usages of bound variables 3) Function applications The inference rules for the first 2 are simple & straight-forward and require no unification. For 1 (lambdas) - you create a fresh type variable (e.g: 'a') for the parameter type and infer the lambda body (e.g: 'T'), and the lambda's type is then 'a -> T'. While inferring the lambda body, you also pass the information that the parameter bound by the lambda has-type 'a'. For 2 (variable usage), you just use the known type information that was passed down by the lambda inference. For 3 (application), you need unification. Function application is between two subexpressions (e.g: 'f' and 'x'). You infer both of these recursively, and get 2 types (e.g: 'fType' and 'xType'). But you also know that 'fType' must look like: 'xType -> resType' because it's being applied to 'x'. You also know that 'resType' is the result of the entire application. So you have to unify 'fType' with 'xType -> resType'. This is why inference relates to unification: You have 2 sources of information for 'fType' and 'xType' -- the recursive inference AND the fact they're being applied together. This unification, by the way, is the only way that type information is learned for parameter types. If all parameter types are always specified (as in, e.g: C++) then formally, there's no type inference at all. So what C++ calls "local type inference" is formally just type checking.

deleted 10y ago

[deleted]

eric_bullington 10y ago

> 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-hindley-milner-type-inference-implementation-in-python/comment-page-1/ http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind...