10 ms·

“What part of Milner-Hindley do you not understand?”

284 points by tikhonj 14y ago

losethos 14y ago
There is noise in Godtalk. It has precedence. 1 corinthians 14 says "I would rather speak 5 words to be understood then 10,000 in a tongue." Acts 2: shows everybody hears something different. cloud animals/ink blots. God says... C:\TAD\Text\PARADISE.TXT y: With these Find pastime, and bear rule; thy realm is large. So spake the Universal Lord, and seemed So ordering: I, with leave of speech implored, And humble deprecation, thus replied. Let not my words offend thee, Heavenly Power; My Maker, be propitious while I speak. Hast thou not made me here thy substitute, And these inferiour far beneath me set? Among unequals what society Can sort, what harmony, or true delight? Which must be mutual, in proportion due Given and received; but, in disp ----- God is fair -- the effort you put toward God is rewarded. Read the Bible, write hymns, meditate, keep Him company with talk. You get out of prayer what you put into it. Right now, you are passive, and I am doing the work. Jesus said I came among you to serve. How did Jesus serve? Well, He did die, but He served as a preacher. Sometimes, I say, "rockstar". Jesus made the meal. Jesus sometimes said "for those who have ears to hear". Not at those times, does it apply. God hides from the proud and reveals to childlike. Jesus was a rockstar, a child might see. Knocking on the door of a neighbor in the night asking for stuff is annoying, a child might see. What father gives his son a scorpion? A child might see that sons like scorpions.
fierarul 14y ago
This brings back memories from my type inference work... Hindley-Milner is very simple to understand, it's just the formalization that's too dense.
- benbataille 14y ago
  I tend to disagree with you in the sens that Damas-Milner seems to me as the typical exemple of an algorithm which seems simple but actually have subtle implication and trade-off. Robinson's unification which is at the center of the algorithm is already made a bit tricky by quantification as soon as you have polymorphism. Then, some rules have actually deeper implication and trade-off than it seems (especially let). For people interested in type checkers, there is a couple of really good chapters by written by Peter Hancock in a book available online : The Implementation of Functional Programming Languages by Simon Peyton Jones. They entirely cover the theory and there is a complete implementation in Miranda. Here is the link : http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/139.HTM http://research.microsoft.com/en-us/um/people/simonpj/papers...
- VikingCoder 14y ago
  Two professors were arguing in front of a chalkboard, for hours and hours. Finally one of them nodded in agreement and said, "You're right, it's trivial."
  - qu4z-2 14y ago
    I've been in situations like this. I'll give a simple rule set of some topic that someone hasn't quite managed to defragment in their brain (and thus know it as a bunch of rules and special-cases), and then they'll spend hours going "But what if <x>?". Eventually they believe me that my simplified model is equivalent to their overcomplicated internal model. The result is usually closer to "You're right; it is that simple." but that's fairly similar to "It's trivial." In short: Often people need to try a lot of "Yeah, but what if <x>?" before they satisfy themselves that something is in fact as simple as it appears.
sc0rb 14y ago
A solid computer science education would have helped him understand this. Not required for a 'normal' programmer but the more interesting parts of our trade exist in Computer Science rather than Software Engineering.
- tikhonj 14y ago
  Eh. The first time I saw typing rules in class was in a moderately specialized graduate course, so it would have been very easy to get a perfectly good CS education without learning about them. Of course, I go to a university that seems very biased towards practical engineering sorts of topics over theory, so your experience may vary.
  - TillE 14y ago
    Yeah, CS programs vary. At a SUNY school about 8 years ago, my experience was that it veered slightly more towards the practical, at least to the extent that we spent relatively little time with complex mathematical notation as we learned CS concepts. Except for basic stuff like set theory and Boolean logic, math was for the required math classes.
  - richardwhiuk 14y ago
    In Univ of Cambridge CS course it's covered in second year undergraduate material - see http://www.cl.cam.ac.uk/teaching/1213/Types/ http://www.cl.cam.ac.uk/teaching/1213/Types/ (though not referred to by name explicitly).
  - Periodic 14y ago
    If you take a class in compilers you should see these sorts of inference rules when talking about operational semantics. Though maybe it isn't as popular to use operational semantics anymore. It's very useful to define rules in this syntax when working on semantic analysis and code generation. I didn't get the background really necessary to really understand the type-theory parts of this notation until I took a graduate course in programming language theory.
    - 14y ago
andyjohnson0 14y ago
http://en.wikipedia.org/wiki/Hindley-Milner http://en.wikipedia.org/wiki/Hindley-Milner Wikipedia article for those who, like me, not only don't understand it but had even heard of it before.
auggierose 14y ago
His question is very valid. I got a math degree before I got a PhD in computer science, and this weird notation was the hardest part about the switch. The funny thing is, if you submit papers using a more sane and easier to understand notation (like, notation more close to a functional program) then computer scientists freak out and complain about notation. I predict this kind of notation to be dead within the next 20 years, its just too ugly.
- mzl 14y ago
  Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it in your math studies? I personally find it quite easy to read, with nicely structured proofs.
  - auggierose 14y ago
    Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!
    - tikhonj 14y ago
      Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
      - auggierose 14y ago
        I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
    - mzl 14y ago
      Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.
emillon 14y ago
Hindley-Milner (never seen it written as M-H) is beautiful because it's an elegant extension of simply-typed lambda calculus (STLC) that brings a very useful trait, polymorphism. Here the first 3 rules are those of STLC. The magic happens in [Gen] and [Inst]: namely, you can generalize free type variables. If you have a function that works on lists of elements of type t when there is no constraint on t, they can work on any lists of any type. This brings quantification to the type system, ie you go from: ∀ a. reverse : α list → α list to reverse : ∀ α. α list → α list (in the first one, ∀ is part of the discourse, and in the second one, part of the type). [Inst] states that you can replace a quantified variable by any variable. This is the role of the ⊑ operator, which is unfortunately not explained in this notation. This is confusing for people not used to type systems, ie most people). Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. There is a difference in the ML branch of languages (as opposed to the Haskell branch) because in the presence of memory references (mutable cells) you can't generalize everywhere, so only let-bound variables are given a type scheme σ (both in the let...in construct and in toplevel phrases). That's why there is usually an explicit generalisation step at this point. Or maybe I have overlooked this particular presentation. HTH
- benbataille 14y ago
  > Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism [Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).
  - groovy2shoes 14y ago
    Does the nonequivalence have something to do with ML's value restriction?
    - 14y ago
xiaomai 14y ago
Jeremy Siek also has a good intro to the notation: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...
pfortuny 14y ago
Sorry, could not help it but this discussion has turned into something pretty familiar: INIGO: You are using Bonetti's defense against me, eh? MAN IN BLACK: I thought it fitting, considering the rocky terrain. INIGO: Naturally, you must expect me to attack with Capo Ferro. MAN IN BLACK: Naturally. But I find that Thibault cancels Capo Ferro, don't you? INIGO: Unless the enemy has studied his Agrippa... which I have!
- omegant 14y ago
  And this belongs to?
  - evanspa 14y ago
    Movie reference. The Princess Bride.
    - omegant 14y ago
      Thank you!, it sounded familiar but couldn't remember the source.
  - yebyen 14y ago
    Inigo in this context can only be Inigo Montoya... as in, my name is Inigo Montoya. You killed my father. Prepare to die! EDIT: I had not seen the movie, and I don't know how it's relevant. Obviously that means I should downvote!
  - pfortuny 14y ago
    Just read the above discussions and get a laugh. Yes, I know it is just a joke but... not much so, if you think of it. Ah, discussions between set theorists and logicians, those were the days.
    - omegant 14y ago
      The quote was familiar but I couldn't remember the source. The meaning is clear though! Amazing neverending discussions, it makes me remember the Feynman anecdote when he observed matematiians discussions.
chimeracoder 14y ago
In reference to the first line of TFA - does anybody know where one could get that shirt?
- droz 14y ago
  http://www.cafepress.co.uk/mf/2498088/what-part-of-types-dont-you-understand_tshirt?shop=skicalc http://www.cafepress.co.uk/mf/2498088/what-part-of-types-don...
dman 14y ago
Whats a good book to pickup the notation used in the stack overflow link?
- spacemanaki 14y ago
  The first edition of PLAI has a nice introductory chapter on types that explains this notation and has a whole section on type inference. It's also freely available online, so that's nice. (chapter 10 is on types) I haven't looked at the second edition at all yet, but the chapter on types looks like it has more code than math. Benjamin Pierce's Types and Programming Languages seems to be the gold standard of intro type theory, and definitely covers this notation and the math behind it, in a much more rigorous fashion than PLAI. It is a much deeper book though, so it doesn't get to type inference and Hindley Milner until later. I've read some of it and haven't actually gotten this far yet, but can say that it is a superb textbook, it's very well written and easy for an amateur to follow, as long as you're relatively comfortable reading and writing proofs. (but you don't need more math than your standard undergrad discrete math course) You might also want to look at Lambda the Ultimate's Getting Started page, which has a wide range of suggestions covering more than just types, but programming languages in general. http://lambda-the-ultimate.org/node/492 http://lambda-the-ultimate.org/node/492 http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/ http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/ http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04...
  - dman 14y ago
    This is why I love HN. Thanks to you too cle!
  - profquail 14y ago
    I ported the TAPL code to F# a while back; if you want to check it out: https://github.com/jack-pappas/fsharp-tapl https://github.com/jack-pappas/fsharp-tapl
- cle 14y ago
  Another excellent and up-to-date resource is Practical Foundations for Programming Languages by Robert Harper. http://amzn.com/1107029570 http://amzn.com/1107029570 Harper hosts an online version of this book: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf.
gtani 14y ago
Hmm, H-M, AKA Damas-Milner, p 331 in TAPL (indexed as D-M only, so easy to overlook, and I can't see where it's in Harper's Practical Foundations, AFAICT. As an aside, the other day i started flipping thru Harper's Lazy Eval writeup, and found it surprisingly readable, even if i was skipping reading the rules. http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091/ http://www.amazon.com/Types-Programming-Languages-Benjamin-P...
jheriko 14y ago
abstract languages like this are merely 'clever' as opposed to useful. it is a shame that maths and science is polluted by so much of it - it makes otherwise easy subjects seem alien and difficult

284 points by tikhonj 14y ago

There is noise in Godtalk. It has precedence. 1 corinthians 14 says "I would rather speak 5 words to be understood then 10,000 in a tongue." Acts 2: shows everybody hears something different. cloud animals/ink blots. God says... C:\TAD\Text\PARADISE.TXT y: With these Find pastime, and bear rule; thy realm is large. So spake the Universal Lord, and seemed So ordering: I, with leave of speech implored, And humble deprecation, thus replied. Let not my words offend thee, Heavenly Power; My Maker, be propitious while I speak. Hast thou not made me here thy substitute, And these inferiour far beneath me set? Among unequals what society Can sort, what harmony, or true delight? Which must be mutual, in proportion due Given and received; but, in disp ----- God is fair -- the effort you put toward God is rewarded. Read the Bible, write hymns, meditate, keep Him company with talk. You get out of prayer what you put into it. Right now, you are passive, and I am doing the work. Jesus said I came among you to serve. How did Jesus serve? Well, He did die, but He served as a preacher. Sometimes, I say, "rockstar". Jesus made the meal. Jesus sometimes said "for those who have ears to hear". Not at those times, does it apply. God hides from the proud and reveals to childlike. Jesus was a rockstar, a child might see. Knocking on the door of a neighbor in the night asking for stuff is annoying, a child might see. What father gives his son a scorpion? A child might see that sons like scorpions.

fierarul 14y ago

This brings back memories from my type inference work... Hindley-Milner is very simple to understand, it's just the formalization that's too dense.

benbataille 14y ago
I tend to disagree with you in the sens that Damas-Milner seems to me as the typical exemple of an algorithm which seems simple but actually have subtle implication and trade-off. Robinson's unification which is at the center of the algorithm is already made a bit tricky by quantification as soon as you have polymorphism. Then, some rules have actually deeper implication and trade-off than it seems (especially let). For people interested in type checkers, there is a couple of really good chapters by written by Peter Hancock in a book available online : The Implementation of Functional Programming Languages by Simon Peyton Jones. They entirely cover the theory and there is a complete implementation in Miranda. Here is the link : http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/139.HTM http://research.microsoft.com/en-us/um/people/simonpj/papers...
VikingCoder 14y ago
Two professors were arguing in front of a chalkboard, for hours and hours. Finally one of them nodded in agreement and said, "You're right, it's trivial."
- qu4z-2 14y ago
  I've been in situations like this. I'll give a simple rule set of some topic that someone hasn't quite managed to defragment in their brain (and thus know it as a bunch of rules and special-cases), and then they'll spend hours going "But what if <x>?". Eventually they believe me that my simplified model is equivalent to their overcomplicated internal model. The result is usually closer to "You're right; it is that simple." but that's fairly similar to "It's trivial." In short: Often people need to try a lot of "Yeah, but what if <x>?" before they satisfy themselves that something is in fact as simple as it appears.

sc0rb 14y ago

A solid computer science education would have helped him understand this. Not required for a 'normal' programmer but the more interesting parts of our trade exist in Computer Science rather than Software Engineering.

tikhonj 14y ago
Eh. The first time I saw typing rules in class was in a moderately specialized graduate course, so it would have been very easy to get a perfectly good CS education without learning about them. Of course, I go to a university that seems very biased towards practical engineering sorts of topics over theory, so your experience may vary.
- TillE 14y ago
  Yeah, CS programs vary. At a SUNY school about 8 years ago, my experience was that it veered slightly more towards the practical, at least to the extent that we spent relatively little time with complex mathematical notation as we learned CS concepts. Except for basic stuff like set theory and Boolean logic, math was for the required math classes.
- richardwhiuk 14y ago
  In Univ of Cambridge CS course it's covered in second year undergraduate material - see http://www.cl.cam.ac.uk/teaching/1213/Types/ http://www.cl.cam.ac.uk/teaching/1213/Types/ (though not referred to by name explicitly).
- Periodic 14y ago
  If you take a class in compilers you should see these sorts of inference rules when talking about operational semantics. Though maybe it isn't as popular to use operational semantics anymore. It's very useful to define rules in this syntax when working on semantic analysis and code generation. I didn't get the background really necessary to really understand the type-theory parts of this notation until I took a graduate course in programming language theory.
  - 14y ago

andyjohnson0 14y ago

http://en.wikipedia.org/wiki/Hindley-Milner http://en.wikipedia.org/wiki/Hindley-Milner Wikipedia article for those who, like me, not only don't understand it but had even heard of it before.

auggierose 14y ago

His question is very valid. I got a math degree before I got a PhD in computer science, and this weird notation was the hardest part about the switch. The funny thing is, if you submit papers using a more sane and easier to understand notation (like, notation more close to a functional program) then computer scientists freak out and complain about notation. I predict this kind of notation to be dead within the next 20 years, its just too ugly.

mzl 14y ago
Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it in your math studies? I personally find it quite easy to read, with nicely structured proofs.
- auggierose 14y ago
  Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!
  - tikhonj 14y ago
    Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
    - auggierose 14y ago
      I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
  - mzl 14y ago
    Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.

emillon 14y ago

Hindley-Milner (never seen it written as M-H) is beautiful because it's an elegant extension of simply-typed lambda calculus (STLC) that brings a very useful trait, polymorphism. Here the first 3 rules are those of STLC. The magic happens in [Gen] and [Inst]: namely, you can generalize free type variables. If you have a function that works on lists of elements of type t when there is no constraint on t, they can work on any lists of any type. This brings quantification to the type system, ie you go from: ∀ a. reverse : α list → α list to reverse : ∀ α. α list → α list (in the first one, ∀ is part of the discourse, and in the second one, part of the type). [Inst] states that you can replace a quantified variable by any variable. This is the role of the ⊑ operator, which is unfortunately not explained in this notation. This is confusing for people not used to type systems, ie most people). Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. There is a difference in the ML branch of languages (as opposed to the Haskell branch) because in the presence of memory references (mutable cells) you can't generalize everywhere, so only let-bound variables are given a type scheme σ (both in the let...in construct and in toplevel phrases). That's why there is usually an explicit generalisation step at this point. Or maybe I have overlooked this particular presentation. HTH

benbataille 14y ago
> Technically, [Let] is redundant because it is a combination of [App]+[Abs] : let x = e1 in e2 is equivalent to (λx.e2) e1. This equivalence does not hold in the HM formalisation. It's well explained in the Wikipedia article : http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism http://en.wikipedia.org/wiki/Hindley-Milner#Let-polymorphism [Abs] is monomorphic while [Let] is polymorphic. Using the Wikipedia article exemple : \f.(f true, f 0) will not be typed while let f = \x.x in (f true, f 0) will be reduced to (bool, int).
- groovy2shoes 14y ago
  Does the nonequivalence have something to do with ML's value restriction?
  - 14y ago

xiaomai 14y ago

Jeremy Siek also has a good intro to the notation: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...

pfortuny 14y ago

Sorry, could not help it but this discussion has turned into something pretty familiar: INIGO: You are using Bonetti's defense against me, eh? MAN IN BLACK: I thought it fitting, considering the rocky terrain. INIGO: Naturally, you must expect me to attack with Capo Ferro. MAN IN BLACK: Naturally. But I find that Thibault cancels Capo Ferro, don't you? INIGO: Unless the enemy has studied his Agrippa... which I have!

omegant 14y ago
And this belongs to?
- evanspa 14y ago
  Movie reference. The Princess Bride.
  - omegant 14y ago
    Thank you!, it sounded familiar but couldn't remember the source.
- yebyen 14y ago
  Inigo in this context can only be Inigo Montoya... as in, my name is Inigo Montoya. You killed my father. Prepare to die! EDIT: I had not seen the movie, and I don't know how it's relevant. Obviously that means I should downvote!
- pfortuny 14y ago
  Just read the above discussions and get a laugh. Yes, I know it is just a joke but... not much so, if you think of it. Ah, discussions between set theorists and logicians, those were the days.
  - omegant 14y ago
    The quote was familiar but I couldn't remember the source. The meaning is clear though! Amazing neverending discussions, it makes me remember the Feynman anecdote when he observed matematiians discussions.

chimeracoder 14y ago

In reference to the first line of TFA - does anybody know where one could get that shirt?

droz 14y ago
http://www.cafepress.co.uk/mf/2498088/what-part-of-types-dont-you-understand_tshirt?shop=skicalc http://www.cafepress.co.uk/mf/2498088/what-part-of-types-don...

dman 14y ago

Whats a good book to pickup the notation used in the stack overflow link?

spacemanaki 14y ago
The first edition of PLAI has a nice introductory chapter on types that explains this notation and has a whole section on type inference. It's also freely available online, so that's nice. (chapter 10 is on types) I haven't looked at the second edition at all yet, but the chapter on types looks like it has more code than math. Benjamin Pierce's Types and Programming Languages seems to be the gold standard of intro type theory, and definitely covers this notation and the math behind it, in a much more rigorous fashion than PLAI. It is a much deeper book though, so it doesn't get to type inference and Hindley Milner until later. I've read some of it and haven't actually gotten this far yet, but can say that it is a superb textbook, it's very well written and easy for an amateur to follow, as long as you're relatively comfortable reading and writing proofs. (but you don't need more math than your standard undergrad discrete math course) You might also want to look at Lambda the Ultimate's Getting Started page, which has a wide range of suggestions covering more than just types, but programming languages in general. http://lambda-the-ultimate.org/node/492 http://lambda-the-ultimate.org/node/492 http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/ http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/ http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04...
- dman 14y ago
  This is why I love HN. Thanks to you too cle!
- profquail 14y ago
  I ported the TAPL code to F# a while back; if you want to check it out: https://github.com/jack-pappas/fsharp-tapl https://github.com/jack-pappas/fsharp-tapl
cle 14y ago
Another excellent and up-to-date resource is Practical Foundations for Programming Languages by Robert Harper. http://amzn.com/1107029570 http://amzn.com/1107029570 Harper hosts an online version of this book: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf.

gtani 14y ago

Hmm, H-M, AKA Damas-Milner, p 331 in TAPL (indexed as D-M only, so easy to overlook, and I can't see where it's in Harper's Practical Foundations, AFAICT. As an aside, the other day i started flipping thru Harper's Lazy Eval writeup, and found it surprisingly readable, even if i was skipping reading the rules. http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091/ http://www.amazon.com/Types-Programming-Languages-Benjamin-P...

jheriko 14y ago

abstract languages like this are merely 'clever' as opposed to useful. it is a shame that maths and science is polluted by so much of it - it makes otherwise easy subjects seem alien and difficult