6 ms·

My feeling is that there's a relatively small subset of programmers who adapt well to unification inference, and they think the way you do - they grok the logic

by urbit 13y ago

My feeling is that there's a relatively small subset of programmers who adapt well to unification inference, and they think the way you do - they grok the logical problem the inference engine is trying to solve, and don't worry at all about how it does it. There is a larger set of programmers who try to understand it and run into, well, stuff like this: http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner I hope you're not seriously suggesting that this content is on the same intellectual level as, say, a good RFC. A good RFC in fact works very hard to be as stupid as possible, and one source of irritation from the RFC-producing world to the PDF-producing world - so to speak - is that the PDF-producing world doesn't seem to even understand that they have this job, much less are making any particular effort to do it. The way people should understand the Hoon type inference engine is to think about the concrete reality of what it's doing, not the abstract mathematical problem it's trying to solve. This is simply because human beings aren't very good as a species at mathematics. Hate that that's true, but that it is true I don't think anyone can deny.

colanderman 13y ago
But you don't need to understand any of the H-M algorithm to understand how to use a language with a H-M type system. You just need to understand that every expression in your program must be able to be statically assigned a non-union non-dependent type. If an expression can't be assigned such a type (e.g. it's sometimes an integer and sometimes a string (in the same function call); or it's a non-empty list, etc.) then your program won't type. Otherwise it will. Importantly: it doesn't matter how you come to this conclusion; the compiler will use the H-M algorithm, but that doesn't mean you need to. You can just look at your "if" expression and realize that you're returning an integer in one branch and a string in the other and that that violates the "non-union non-dependent" requirement above. (This, BTW, is an example of the difference between a spec (what I outlined above) and an implementation (what the H-M algorithm says to do).)
- urbit 13y ago
  This is an excellent point, and we're in vehement agreement. Or almost vehement agreement. The thing is, as a programmer, I have to understand what result the algorithm will produce. I have to understand what type my variable will be. If I have to look and see what the compiler came up with, I have way too much work to do. There are two ways to solve this problem. One is to build an abstract mathematical model which you can emulate in your head - not using the same methods, maybe, but getting the same results. The other is to build a concrete, mechanical model which you don't emulate, but rather simulate. Your brain computes not the goal of the algorithm, but the mechanism by which the algorithm is implemented. Same result - you know what type the variable will be. From my perspective, it's one problem, it has to get solved, and the right way to solve it is the way that's the easiest for the people who will actually use the language. For my kind of people, I feel math guys are far too enamored of doing it the emulation way instead of the simulation way. But this is basically an aesthetic opinion about user interface design, so we may be at the end of Hume's is-ought question here...
  - mietek 13y ago
    In practice, using a language with Hindley-Milner type inference is massively more simple than you appear to think it is. There are countless other warts, but this ain't it.
    - dgreensp 13y ago
      I sense a fallacy lurking here. Sure, a type system like Haskell's or even Scala's is magic (and can be used without understanding it) as long as it can "Do What You Mean," but when it can't, you have to understand its workings. We can't sweep that fact under the rug by calling any failure to "Do What You Mean" a bug, a wart to be fixed -- a deviation from correct DWYM behavior. There is no actual DWYM type system, or at least no one's ever come up with one. What type system doesn't have warts? Haskell's probably has both more and fewer than most, depending on how you count them, because so much emphasis is put on the type system. When you use any language long enough, you end up needing to simulate pretty much every observable aspect of it yourself -- not including, for example, the garbage collector, the JVM bytecode verifier, or the GCC code optimizer, which are supposed to be transparent, but including the type inferencer, the JVM threading model, and the JavaScript semicolon insertion rules, which are not. Some of these things you can steer clear of for a long time or even avoid forever by staying on the beaten path, but they lurk, waiting for the thousands of people who have run into bugs or compiler errors and needed to understand them. I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.
tikhonj 13y ago
I think you're just projecting your familiarity with things like RFCs as somehow more intuitive. People have plenty of problems with the network stack and its associated abstractions! TCP/IP or even just HTTP lead to plenty of confusion. In a vacuum, I am not convinced the RFC would be any easier than a paper on Hindley Milner. (Wikipedia is not a good replacement for either.) "Intellectual level" isn't exactly a well-defined term. It inevitably conflates the inherent complexity of something with the background needed to quickly understand it. The difference in the two articles is not in how accessible they are to somebody with no relevant background--both the RFCs and H-M would make no sense to a layperson!--but in the fact that they target different audiences. Both are very stupid in the same way: they are very explicit about every little detail. It's just where an RFC uses technical terminology mixed with a legalese-like language (SHOULD and MUST and so on), H-M uses mathematical notation and inference rules. I do not believe that one of these is so much more inherently difficult to understand than another; it's much more a matter of experience and background knowledge. Without that, reading either is going to be relatively slow and laborious. Having gone through both RFCs and type theory, I've found both similarly slow in terms of content; the main difference is that the mathematical notation happens to be much more dense. So perhaps it takes me five times longer to get through a page about type theory as a page of an RFC, but that single page contains the same amount of information, just encoded differently. Also, I don't buy that you have to understand how the inference works to use it, any more than you have to understand or think about the OSI model to write networking code. You can use both perfectly well--and most people do--without needing to think about or understand everything. Moreover, you won't be able to learn either without a good deal of work and the relevant background. I suspect that it just happens that the background for one matches much more closely with yours than the background for the other. Sure, humans as a species are not very good at mathematics. But they aren't very good at engineering either! They are really bad at keeping a bunch of details in memory and running (even simple) algorithms in their heads. All told, it's better to avoid it.
- urbit 13y ago
  For the source of my bias, I have actually spent a considerable amount of time working with people in the "RFC world." For example, I wrote the kernel of the Openwave WAP browser, which shipped about a billion units, even if it sucked and no one used it. I have spent just about no time in the PDF world, and even when I was in grad school I was an OS guy. (Here's a fun old paper of mine: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7414 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7...). So, zero time in the "PL theory" world. I can tell you how this world sees the "PL theory" world. They say: look, you have your own way of formalizing computing, there are infinitely many ways of formalizing computing, the one we use seems to work just fine, so why should we learn yours? Whether they won't, or they can't, or they are too pigheaded to - the answer is, they aren't. I don't view language design as an opportunity to change the world to this extent. And I think many, many good ideas are getting lost in the PL theory world. So, my goal was to replicate these ideas, as best as I can, for programmers who think about programming the way I do.

by urbit 13y ago

colanderman 13y ago

But you don't need to understand any of the H-M algorithm to understand how to use a language with a H-M type system. You just need to understand that every expression in your program must be able to be statically assigned a non-union non-dependent type. If an expression can't be assigned such a type (e.g. it's sometimes an integer and sometimes a string (in the same function call); or it's a non-empty list, etc.) then your program won't type. Otherwise it will. Importantly: it doesn't matter how you come to this conclusion; the compiler will use the H-M algorithm, but that doesn't mean you need to. You can just look at your "if" expression and realize that you're returning an integer in one branch and a string in the other and that that violates the "non-union non-dependent" requirement above. (This, BTW, is an example of the difference between a spec (what I outlined above) and an implementation (what the H-M algorithm says to do).)

urbit 13y ago
This is an excellent point, and we're in vehement agreement. Or almost vehement agreement. The thing is, as a programmer, I have to understand what result the algorithm will produce. I have to understand what type my variable will be. If I have to look and see what the compiler came up with, I have way too much work to do. There are two ways to solve this problem. One is to build an abstract mathematical model which you can emulate in your head - not using the same methods, maybe, but getting the same results. The other is to build a concrete, mechanical model which you don't emulate, but rather simulate. Your brain computes not the goal of the algorithm, but the mechanism by which the algorithm is implemented. Same result - you know what type the variable will be. From my perspective, it's one problem, it has to get solved, and the right way to solve it is the way that's the easiest for the people who will actually use the language. For my kind of people, I feel math guys are far too enamored of doing it the emulation way instead of the simulation way. But this is basically an aesthetic opinion about user interface design, so we may be at the end of Hume's is-ought question here...
- mietek 13y ago
  In practice, using a language with Hindley-Milner type inference is massively more simple than you appear to think it is. There are countless other warts, but this ain't it.
  - dgreensp 13y ago
    I sense a fallacy lurking here. Sure, a type system like Haskell's or even Scala's is magic (and can be used without understanding it) as long as it can "Do What You Mean," but when it can't, you have to understand its workings. We can't sweep that fact under the rug by calling any failure to "Do What You Mean" a bug, a wart to be fixed -- a deviation from correct DWYM behavior. There is no actual DWYM type system, or at least no one's ever come up with one. What type system doesn't have warts? Haskell's probably has both more and fewer than most, depending on how you count them, because so much emphasis is put on the type system. When you use any language long enough, you end up needing to simulate pretty much every observable aspect of it yourself -- not including, for example, the garbage collector, the JVM bytecode verifier, or the GCC code optimizer, which are supposed to be transparent, but including the type inferencer, the JVM threading model, and the JavaScript semicolon insertion rules, which are not. Some of these things you can steer clear of for a long time or even avoid forever by staying on the beaten path, but they lurk, waiting for the thousands of people who have run into bugs or compiler errors and needed to understand them. I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.

tikhonj 13y ago

I think you're just projecting your familiarity with things like RFCs as somehow more intuitive. People have plenty of problems with the network stack and its associated abstractions! TCP/IP or even just HTTP lead to plenty of confusion. In a vacuum, I am not convinced the RFC would be any easier than a paper on Hindley Milner. (Wikipedia is not a good replacement for either.) "Intellectual level" isn't exactly a well-defined term. It inevitably conflates the inherent complexity of something with the background needed to quickly understand it. The difference in the two articles is not in how accessible they are to somebody with no relevant background--both the RFCs and H-M would make no sense to a layperson!--but in the fact that they target different audiences. Both are very stupid in the same way: they are very explicit about every little detail. It's just where an RFC uses technical terminology mixed with a legalese-like language (SHOULD and MUST and so on), H-M uses mathematical notation and inference rules. I do not believe that one of these is so much more inherently difficult to understand than another; it's much more a matter of experience and background knowledge. Without that, reading either is going to be relatively slow and laborious. Having gone through both RFCs and type theory, I've found both similarly slow in terms of content; the main difference is that the mathematical notation happens to be much more dense. So perhaps it takes me five times longer to get through a page about type theory as a page of an RFC, but that single page contains the same amount of information, just encoded differently. Also, I don't buy that you have to understand how the inference works to use it, any more than you have to understand or think about the OSI model to write networking code. You can use both perfectly well--and most people do--without needing to think about or understand everything. Moreover, you won't be able to learn either without a good deal of work and the relevant background. I suspect that it just happens that the background for one matches much more closely with yours than the background for the other. Sure, humans as a species are not very good at mathematics. But they aren't very good at engineering either! They are really bad at keeping a bunch of details in memory and running (even simple) algorithms in their heads. All told, it's better to avoid it.

urbit 13y ago
For the source of my bias, I have actually spent a considerable amount of time working with people in the "RFC world." For example, I wrote the kernel of the Openwave WAP browser, which shipped about a billion units, even if it sucked and no one used it. I have spent just about no time in the PDF world, and even when I was in grad school I was an OS guy. (Here's a fun old paper of mine: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7414 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7...). So, zero time in the "PL theory" world. I can tell you how this world sees the "PL theory" world. They say: look, you have your own way of formalizing computing, there are infinitely many ways of formalizing computing, the one we use seems to work just fine, so why should we learn yours? Whether they won't, or they can't, or they are too pigheaded to - the answer is, they aren't. I don't view language design as an opportunity to change the world to this extent. And I think many, many good ideas are getting lost in the PL theory world. So, my goal was to replicate these ideas, as best as I can, for programmers who think about programming the way I do.