6 ms·

"""Its self-compiling kernel, 7000 lines of code, specifies Hoon unambiguously; there is no Hoon spec.""" You realize there's such a thing as over-specifying s

"""Its self-compiling kernel, 7000 lines of code, specifies Hoon unambiguously; there is no Hoon spec.""" You realize there's such a thing as over-specifying something, right? You realize that using source code as a spec does this? If you don't realize; consider that non-data aspects of a program, such as runtime and memory usage and bug compatibility, can sometimes form part of a specification, and sometimes don't. A specification says as much what is not required of an implementation as what is required. By claiming your one true implementation is the spec, one has no means of ascertaining what behavior is incidental, and what is actually required/able to be relied upon. I'm not normally an XKCD fan, but this strip sums it up perfectly: http://xkcd.com/1172/ http://xkcd.com/1172/ . """Hoon can be classified as a pure, strict higher-order static type-inferred functional language, with co/contra/bivariance and genericity. However, Hoon does not use lambda calculus,""" A higher-order functional language does not "use" the mathematical definition of higher-order functions? In that case, what do you mean by "higher-order functional language"? EDIT: I was going to make an analogy to the hypothetical claim that language X's arithmetic system doesn't use Church numerals (i.e. the mathematical formulation of natural numbers)… but Hoon is actually implemented using Church arithmetic. Go figure. . """unification,""" By what mechanism does Hoon implement type inference? Honestly, that's kind of like saying Hoon doesn't use, say, queues. Great, but, why? . """or other constructs from “PL theory.”""" Disdainful much? I'm really curious what's the background behind the scare quotes here. . EDIT: Just to be clear, I'm not claiming your project is uninteresting or not worth your while. I just feel you're being overly dismissive of the, let's say "traditional" schools of thought, with invalid justification.

urbit 13y ago
As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms. Actually someone reported a (cosmetic) bug in the Nock spec this morning, which is quite cool. There's a very important point in that Nock can specify not what a computer computes - but what it has computed, if it terminates. In general, practical systems have to interrupt long-running computations, so they must always compute some subset of that definition. But it can be, and is, a strict subset. I find this a meaningful and accurate statement. Sorry, I didn't mean "PL theory" as scare quotes - I just didn't want to exclude anyone for whom the term doesn't instantly bring to mind a body of work. The truth, though, is that the "PL theory" we have is just one theory of programming. It's a convention, it's not a piece of reality like pi. Church-Turing equivalence tells us that we have infinitely many such representations. Eg, the Turing Machine is equivalent in power to lambda, but much less useful as a programming framework. My feeling is that, as a programming model, lambda suffers from the fact that it was originally designed, by mathematicians, to do mathematics. Just from a UI basis, programmers are not mathematicians. The skill is very similar, but mathematicians work best in geometric and logical abstractions, whereas programmers are more comfortable with mechanical representations. For instance, the general lambda approach is to represent data as code (Church numerals), a very sensible approach from the math side, whereas the Nock approach is to represent code as data - which feels more natural to the programmer. So, nothing can tarnish the very powerful and elegant model of computing that is "PL theory." But it is not "the" theory of computing - just one of infinitely many possible theories.
- colanderman 13y ago
  As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms. Not my point. The "spec" can be perfect, but you're not saying what a Nock implementation needn't do. If I write NockJIT that optimizes increment-loops into O(1) addition, does that violate the spec? You might reply "no", but someone else who relied on such loops for hardware timing obviously would say "yes".
  - urbit 13y ago
    The spec defines the semantics, not the performance. I think that's a pretty concrete distinction. But in practice, at a certain level some kind of informative or even quasi-normative convention will have to creep in if you want to define the question "computer X can run program Y reasonably well." It's a qualitatively different problem, but it remains a real problem. Not one we have in the early days of the system, though. I am happy to solve most but not all of any problem...
    - colanderman 13y ago
      The spec defines the semantics, not the performance. I think that's a pretty concrete distinction. But it's a distinction you have to make. Concrete ≠ obvious. Other things that are sometimes in specs and sometimes not: Is the intermediate state of a running Hoon program specified by the code? (It matters for someone writing a debugger!) Is how the compiled program handles data at runtime specified? (It matters for a cryptographer!) Are the errors produced by the compiler specified? (It matters for an IDE!) Does the compiler have any limitations that should be allowed to be reduced / not have any limitations that should be allowed to be restricted? (It matters for anyone trying to make a faster compiler!)
      - urbit 13y ago
        I think the source of the confusion is that I'm carving off a stricter, and smaller, definition of the word "spec" than what we're used to. I agree. The word is not quite right. In general the answer to your questions is "yes and no." Well, really it's no - except that as a fairly common case, for example when we want to catch compiler errors without breaking out of the system, we virtualize Nock within itself. This is also serviceable when it comes to adding an extra operator, 11, that dereferences the global namespace. But the fact that "virtual Nock" is just a virtualization stack within one Nock interpreter is not semantically detectable.
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.

urbit 13y ago

As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms. Actually someone reported a (cosmetic) bug in the Nock spec this morning, which is quite cool. There's a very important point in that Nock can specify not what a computer computes - but what it has computed, if it terminates. In general, practical systems have to interrupt long-running computations, so they must always compute some subset of that definition. But it can be, and is, a strict subset. I find this a meaningful and accurate statement. Sorry, I didn't mean "PL theory" as scare quotes - I just didn't want to exclude anyone for whom the term doesn't instantly bring to mind a body of work. The truth, though, is that the "PL theory" we have is just one theory of programming. It's a convention, it's not a piece of reality like pi. Church-Turing equivalence tells us that we have infinitely many such representations. Eg, the Turing Machine is equivalent in power to lambda, but much less useful as a programming framework. My feeling is that, as a programming model, lambda suffers from the fact that it was originally designed, by mathematicians, to do mathematics. Just from a UI basis, programmers are not mathematicians. The skill is very similar, but mathematicians work best in geometric and logical abstractions, whereas programmers are more comfortable with mechanical representations. For instance, the general lambda approach is to represent data as code (Church numerals), a very sensible approach from the math side, whereas the Nock approach is to represent code as data - which feels more natural to the programmer. So, nothing can tarnish the very powerful and elegant model of computing that is "PL theory." But it is not "the" theory of computing - just one of infinitely many possible theories.

colanderman 13y ago
As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms. Not my point. The "spec" can be perfect, but you're not saying what a Nock implementation needn't do. If I write NockJIT that optimizes increment-loops into O(1) addition, does that violate the spec? You might reply "no", but someone else who relied on such loops for hardware timing obviously would say "yes".
- urbit 13y ago
  The spec defines the semantics, not the performance. I think that's a pretty concrete distinction. But in practice, at a certain level some kind of informative or even quasi-normative convention will have to creep in if you want to define the question "computer X can run program Y reasonably well." It's a qualitatively different problem, but it remains a real problem. Not one we have in the early days of the system, though. I am happy to solve most but not all of any problem...
  - colanderman 13y ago
    The spec defines the semantics, not the performance. I think that's a pretty concrete distinction. But it's a distinction you have to make. Concrete ≠ obvious. Other things that are sometimes in specs and sometimes not: Is the intermediate state of a running Hoon program specified by the code? (It matters for someone writing a debugger!) Is how the compiled program handles data at runtime specified? (It matters for a cryptographer!) Are the errors produced by the compiler specified? (It matters for an IDE!) Does the compiler have any limitations that should be allowed to be reduced / not have any limitations that should be allowed to be restricted? (It matters for anyone trying to make a faster compiler!)
    - urbit 13y ago
      I think the source of the confusion is that I'm carving off a stricter, and smaller, definition of the word "spec" than what we're used to. I agree. The word is not quite right. In general the answer to your questions is "yes and no." Well, really it's no - except that as a fairly common case, for example when we want to catch compiler errors without breaking out of the system, we virtualize Nock within itself. This is also serviceable when it comes to adding an extra operator, 11, that dereferences the global namespace. But the fact that "virtual Nock" is just a virtualization stack within one Nock interpreter is not semantically detectable.

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.