4 ms·

As for the type inference, you don't need unification to do type inference. Hoon infers only forward, not backward. Of course you could say it's a subset of u

by urbit 13y ago

As for the type inference, you don't need unification to do type inference. Hoon infers only forward, not backward. Of course you could say it's a subset of unification, as it is. I find Hindley-Milner inference systems too powerful. The programmer has to model what the inference system is doing in his or her head, and it's a source of significant cognitive load. Hoon's inference algorithm is slightly too smart in some cases, and requires slightly too much typing in others, but I think it's generally well matched to human capacities - especially for those of us who are not natural mathematicians.

tikhonj 13y ago
What? Why do you have to think about what the type inference is doing? I've never needed that with H-M in practice, and I've spent a fair amount of time with both Haskell and OCaml. When I use a good inference system like that, I simply don't think about the typechecker most of the time. It just doesn't come up. The types simply work out, largely because the inference is sufficiently good. The only times I've had to model the inference in my head is when it is insufficiently powerful, like with OCaml objects or certain typeclass patterns in Haskell. That is, it's only a problem when the inference breaks unexpectedly. Type inference just works, until it doesn't. And that's the only place I've had difficulties: when it doesn't. The solution to a problem like that is not to make it break more often! That just exacerbates things. A less capable system (say Scala or, god forbid, Go) just makes life more difficult. Even if it's easier to run the algorithm in your head. Especially then, in fact: you shouldn't be thinking about it on the first place.
- 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.
- Darmani 13y ago
  I've actually found knowledge of type inference quite useful for understanding error messages. In OCaml, you typically allow the compiler to infer all types for functions, and only have them compared to your type signatures later, when the containing module is ascribed to a signature. This means that you can see type errors in a perfectly-correct definition of a function -- if you used it incorrectly earlier in the file. This confused the heck out of me until I thought for a few seconds about how it worked. Haskell mostly avoids this problem by encouraging writing type signatures and checking them immediately against definitions, turning the global analysis that is OCaml's type inference into a local problem. However, when using local definitions, I do still sometimes have to think about whether a type error comes from a definition or a use.
  - mjmahone17 13y ago
    You can solve this, to some extent, in OCaml, by just type-hinting everything. But then what fun is type inference?
colanderman 13y ago
Of course you could say it's a subset of unification, as it is. It definitely is, and a limiting one at that. How does Hoon infer the type error in whatever is the Hoon equivalent of the, say, JavaScript expression (a == b && b == 5 && a == "foo"), where a and b are function parameters?
- urbit 13y ago
  Equality is entirely untyped in Hoon. You're just comparing the nouns - "S-expressions without the S." So there is no type error at all. You'd say &(=(a b) =(5 b) =("foo" a)) and it'd work just fine.
  - mietek 13y ago
    That's a bit underwhelming.
    - offensivehandle 13y ago
      why, would you prefer some other answer than 'false'? now, the real question is whether Hoon thinks that (= 5 "5"), or (= 100 "1e2"), or (= 4 "four"), like some languages helpfully provide.
      - mietek 13y ago
        The question posed by colanderman's expression is valid if and only if there is a type containing both 5 and "foo". Here's Haskell's answer: Prelude> \ a b -> a == b && b == 5 && a == "foo" <interactive>:2:25: No instance for (Num [Char]) arising from the literal `5' Possible fix: add an instance declaration for (Num [Char]) In the second argument of `(==)', namely `5' In the first argument of `(&&)', namely `b == 5' In the second argument of `(&&)', namely `b == 5 && a == "foo"' Here, the typechecker took the most general type of 5, namely some type belonging to the Num typeclass, and discovered that the type of "foo", which is [Char], isn't an instance of the Num typeclass, or, in Java parlance, doesn't implement the Num interface. This means there is no type containing both 5 and "foo", hence — type error. You're asking about implicit conversions, which are an undisputable evil. However, attempting to provide answers to invalid questions also isn't very good. You may have already seen the rather entertaining Wat talk, by Gary Bernhardt: https://www.destroyallsoftware.com/talks/wat https://www.destroyallsoftware.com/talks/wat The central theme of this talk is not just implicit conversions — it's surprising answers to invalid questions. A much better way to handle an invalid question is to reject it as early as possible — Fail Fast. With a static type system, this can be very early indeed.
freyrs3 13y ago
> The programmer has to model what the inference system is doing in his or her head, and it's a source of significant cognitive load. Huh? I don't know what your type-inferred language of choice is, but personally I never have to go down to the level of solving constraint sets and unifying types in my head when working any of the ML dialects. Even when writing my own inference algorithms, once I'm able to establish confluence and progress I rarely give the main inference constraint solver a second thought when writing code.
- urbit 13y ago
  See my response to tikhonj. No, of course not, because you're naturally good at PL theory. Or maybe artificially good at it. Whatever the reason, you're good at it. But I believe it's clear that most people, even most programmers, aren't naturally good at it. And a lot of effort have been invested in trying to make them artificially good at it, without much result as I can see. The number of extremely smart people I've met, who nonetheless think Haskell is too smart for them, is considerable. This is quite simply a UI problem. If you have a UI problem and you either don't try to solve the problem, or do and fail, you get an adoption problem. Haskell has an adoption problem, n'est ce pas? So where does my reasoning go wrong?
  - freyrs3 13y ago
    > Haskell has an adoption problem, n'est ce pas? So where does my reasoning go wrong? The problem is thinking that this comes from unification-based inference algorithms which is an implementation detail thats fairly far removed from the day to day programmer concerns. Most Haskell programmers are not type theorists and don't implement HMF algorithms. The only difference between a Haskell programmer and "most programmers" is that they've taken the time to learn the language. In my experience many people turn away from Haskell because they can't immediately transfer their existing knowledge into it and don't like feeling like a beginner again, so they stop. I've met many /more/ people who think that programming in Java is too smart for them as well, it's just a matter of putting the time in to learn.
    - 13y ago

by urbit 13y ago

tikhonj 13y ago

What? Why do you have to think about what the type inference is doing? I've never needed that with H-M in practice, and I've spent a fair amount of time with both Haskell and OCaml. When I use a good inference system like that, I simply don't think about the typechecker most of the time. It just doesn't come up. The types simply work out, largely because the inference is sufficiently good. The only times I've had to model the inference in my head is when it is insufficiently powerful, like with OCaml objects or certain typeclass patterns in Haskell. That is, it's only a problem when the inference breaks unexpectedly. Type inference just works, until it doesn't. And that's the only place I've had difficulties: when it doesn't. The solution to a problem like that is not to make it break more often! That just exacerbates things. A less capable system (say Scala or, god forbid, Go) just makes life more difficult. Even if it's easier to run the algorithm in your head. Especially then, in fact: you shouldn't be thinking about it on the first place.

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.
Darmani 13y ago
I've actually found knowledge of type inference quite useful for understanding error messages. In OCaml, you typically allow the compiler to infer all types for functions, and only have them compared to your type signatures later, when the containing module is ascribed to a signature. This means that you can see type errors in a perfectly-correct definition of a function -- if you used it incorrectly earlier in the file. This confused the heck out of me until I thought for a few seconds about how it worked. Haskell mostly avoids this problem by encouraging writing type signatures and checking them immediately against definitions, turning the global analysis that is OCaml's type inference into a local problem. However, when using local definitions, I do still sometimes have to think about whether a type error comes from a definition or a use.
- mjmahone17 13y ago
  You can solve this, to some extent, in OCaml, by just type-hinting everything. But then what fun is type inference?

colanderman 13y ago

Of course you could say it's a subset of unification, as it is. It definitely is, and a limiting one at that. How does Hoon infer the type error in whatever is the Hoon equivalent of the, say, JavaScript expression (a == b && b == 5 && a == "foo"), where a and b are function parameters?

urbit 13y ago
Equality is entirely untyped in Hoon. You're just comparing the nouns - "S-expressions without the S." So there is no type error at all. You'd say &(=(a b) =(5 b) =("foo" a)) and it'd work just fine.
- mietek 13y ago
  That's a bit underwhelming.
  - offensivehandle 13y ago
    why, would you prefer some other answer than 'false'? now, the real question is whether Hoon thinks that (= 5 "5"), or (= 100 "1e2"), or (= 4 "four"), like some languages helpfully provide.
    - mietek 13y ago
      The question posed by colanderman's expression is valid if and only if there is a type containing both 5 and "foo". Here's Haskell's answer: Prelude> \ a b -> a == b && b == 5 && a == "foo" <interactive>:2:25: No instance for (Num [Char]) arising from the literal `5' Possible fix: add an instance declaration for (Num [Char]) In the second argument of `(==)', namely `5' In the first argument of `(&&)', namely `b == 5' In the second argument of `(&&)', namely `b == 5 && a == "foo"' Here, the typechecker took the most general type of 5, namely some type belonging to the Num typeclass, and discovered that the type of "foo", which is [Char], isn't an instance of the Num typeclass, or, in Java parlance, doesn't implement the Num interface. This means there is no type containing both 5 and "foo", hence — type error. You're asking about implicit conversions, which are an undisputable evil. However, attempting to provide answers to invalid questions also isn't very good. You may have already seen the rather entertaining Wat talk, by Gary Bernhardt: https://www.destroyallsoftware.com/talks/wat https://www.destroyallsoftware.com/talks/wat The central theme of this talk is not just implicit conversions — it's surprising answers to invalid questions. A much better way to handle an invalid question is to reject it as early as possible — Fail Fast. With a static type system, this can be very early indeed.

freyrs3 13y ago

> The programmer has to model what the inference system is doing in his or her head, and it's a source of significant cognitive load. Huh? I don't know what your type-inferred language of choice is, but personally I never have to go down to the level of solving constraint sets and unifying types in my head when working any of the ML dialects. Even when writing my own inference algorithms, once I'm able to establish confluence and progress I rarely give the main inference constraint solver a second thought when writing code.

urbit 13y ago
See my response to tikhonj. No, of course not, because you're naturally good at PL theory. Or maybe artificially good at it. Whatever the reason, you're good at it. But I believe it's clear that most people, even most programmers, aren't naturally good at it. And a lot of effort have been invested in trying to make them artificially good at it, without much result as I can see. The number of extremely smart people I've met, who nonetheless think Haskell is too smart for them, is considerable. This is quite simply a UI problem. If you have a UI problem and you either don't try to solve the problem, or do and fail, you get an adoption problem. Haskell has an adoption problem, n'est ce pas? So where does my reasoning go wrong?
- freyrs3 13y ago
  > Haskell has an adoption problem, n'est ce pas? So where does my reasoning go wrong? The problem is thinking that this comes from unification-based inference algorithms which is an implementation detail thats fairly far removed from the day to day programmer concerns. Most Haskell programmers are not type theorists and don't implement HMF algorithms. The only difference between a Haskell programmer and "most programmers" is that they've taken the time to learn the language. In my experience many people turn away from Haskell because they can't immediately transfer their existing knowledge into it and don't like feeling like a beginner again, so they stop. I've met many /more/ people who think that programming in Java is too smart for them as well, it's just a matter of putting the time in to learn.
  - 13y ago