5 ms·

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) yea

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 11y 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.
eric_bullington 11y ago
> 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-hindley-milner-type-inference-implementation-in-python http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind... 1. https://github.com/alehander42/hermetic https://github.com/alehander42/hermetic 2. https://github.com/billpmurphy/hask https://github.com/billpmurphy/hask 3. http://andrej.com/plzoo/ 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.
- igravious 11y ago
  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.
  - eric_bullington 11y ago
    Check out RAML: https://github.com/raml-org/raml-spec 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.
sklogic 11y ago
> an implementation in either a dynamically typed language ML in Lisp and Prolog: https://github.com/combinatorylogic/mbase/tree/master/src/l/lib/ml https://github.com/combinatorylogic/mbase/tree/master/src/l/...

Peaker 11y 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.

eric_bullington 11y ago

> 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-hindley-milner-type-inference-implementation-in-python http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind... 1. https://github.com/alehander42/hermetic https://github.com/alehander42/hermetic 2. https://github.com/billpmurphy/hask https://github.com/billpmurphy/hask 3. http://andrej.com/plzoo/ 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.

igravious 11y ago
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.
- eric_bullington 11y ago
  Check out RAML: https://github.com/raml-org/raml-spec 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.

sklogic 11y ago

> an implementation in either a dynamically typed language ML in Lisp and Prolog: https://github.com/combinatorylogic/mbase/tree/master/src/l/lib/ml https://github.com/combinatorylogic/mbase/tree/master/src/l/...