The more I think about it the more I really like the whole "Jets" concept (although I'm not sold on the name, I'd love to learn that it's a known concept in the PL field with a nicer name). I'd like to see how such an approach would work out for optimizing something more "fundamental" like the Binary Lambda Calculus.
Urbit: A clean-slate functional OS
91–100 of 185 posts
Re: Urbit: A clean-slate functional OS
#92""" 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…
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 computatio…
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".
Re: Urbit: A clean-slate functional OS
#93""" 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…
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 so…
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.
Re: Urbit: A clean-slate functional OS
#94""" 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…
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 so…
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?
Re: Urbit: A clean-slate functional OS
#95""" 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…
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 so…
> 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.
Re: Urbit: A clean-slate functional OS
#96Earlier quoted context omitted.
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 so…
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…
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
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.
Re: Urbit: A clean-slate functional OS
#97If ever there was a right attitude about bringing a radical project in to the world: this is it.
I just spent 15 minutes just _reading_ the documentation. Because it's _interesting_. That never happens.
Re: Urbit: A clean-slate functional OS
#98Earlier quoted context omitted.
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 so…
> 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 c…
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?
Re: Urbit: A clean-slate functional OS
#99Earlier quoted context omitted.
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 so…
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?
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.
Re: Urbit: A clean-slate functional OS
#100Earlier quoted context omitted.
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 computatio…
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 wou…
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...