Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Urbit: A clean-slate functional OS

urbit.org

Post reply on HN
Print view View original

111–120 of 185 posts

Re: Urbit: A clean-slate functional OS

#111

Post by urbit »

colanderman wrote: post #109
urbit wrote: post #100

Earlier quoted context omitted.

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,…

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…

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.

Re: Urbit: A clean-slate functional OS

#112

Post by clarkm »

zzzmarcus wrote: post #72

Just some background, this is by Mencius Moldbug, a.k.a. Curtis Yarvin, a.k.a. C. Guy Yarvin of Unqualified Reservations fame. It's been in the works for a long time and is certainly a serious project. http://unqualified-reservations.blogspot.com/2010/01/urbit-f... http://moronlab.blogspot.com/

Someone earlier in this thread mentioned his apparent disdain for PL research. If you want some background on his experiences, as well as some great musings on the current state of CS grad programs, I recommend these two articles:

http://unqualified-reservations.blogspot.com/2007/07/my-navr...

http://unqualified-reservations.blogspot.com/2007/08/whats-w...

Re: Urbit: A clean-slate functional OS

#113

Post by urbit »

freyrs3 wrote: post #107
urbit wrote: post #98

Earlier quoted context omitted.

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'…

> 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 program…

My experience is that there are two very different kinds of Haskell programmers: those who really understand the math, like you, and those who treat it as a black box (the "Learn You A Haskell" contingent).

As a black-box language, I think Haskell is of nontrivial value, but the black box is very deep and weird. This is a UI problem. If you expect people to understand the theory, this is also a UI problem in a different way.

So, two UI problems add up to a big UI problem, which is my theory about the adoption issues. I'm curious as to what your theory is.

Re: Urbit: A clean-slate functional OS

#114

Post by nmcfarl »

quanticle wrote: post #44

I love the project concept. A toy functional OS would be an admirable counterpart to e.g. MINIX. That said, I have one minor quibble: A programming language is called a language for a reason - it should activate the human linguistic lobes. Another programmer said this, a long time ago, and that's how we ended up with Perl. Please don't seek to emulate Larry Wall. Perl is great for quick automation, but anything compl…

Larry Wall is a great man. And Perl was mighty force. An empire was built, and it may have crumbled, but all empires crumble.

One day you will be repeating these words, to a youngster that says the heroes of your Ruby palace, (or your conquering Pythonistas) were weak men of little vision, and laughs at you for following them. And when that day comes, I ask only that you think of me, and Wall, as I now think of one who followed Backus, and the mighty FORTRAN army.

Re: Urbit: A clean-slate functional OS

#115

Post by wgd »

dragonwriter wrote: post #83
wgd wrote: post #42

Earlier quoted context omitted.

I think it's a fascinating tradeoff. A typical approach with JIT-compilation is to write relatively inefficient code and hope that the JIT compiler picks up on it and optimizes it for you. Their approach seems to instead be to say "if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time". IMO this is a really cool idea because the performance o…

> A typical approach with JIT-compilation is to write relatively inefficient code and hope that the JIT compiler picks up on it and optimizes it for you. Their approach seems to instead be to say "if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time". I don't see the "instead" there. Those seem to be two ways of saying the same thing.

The difference is one of universality.

Let's say that my VM of choice has a tracing JIT, and it will attempt to optimize traces up to 1,000 instructions long. Let's further say that in the current version of my code, the body of my hot loop is 980 instructions long. Then in a new version I add another few operations which push it up to 1,010 instructions. Suddenly the JIT stops trying to optimize that portion of my code and performance tanks.

Meanwhile some other guy wrote his code using a VM which used this sort of "Jets" approach. It's probably not as fast or as versatile overall, but when he adds another few dozen instructions to a hot loop he can do so secure in the knowledge that all the preexisting code will continue to execute just like it did before.

Re: Urbit: A clean-slate functional OS

#116

Post by freyrs3 »

urbit wrote: post #113
freyrs3 wrote: post #107

Earlier quoted context omitted.

> 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 program…

My experience is that there are two very different kinds of Haskell programmers: those who really understand the math, like you, and those who treat it as a black box (the "Learn You A Haskell" contingent). As a black-box language, I think Haskell is of nontrivial value, but the black box is very deep and weird. This is a UI problem. If you expect people to understand the theory, this is also a UI problem in a differ…

> If you expect people to understand the theory, this is also a UI problem in a different way.

I don't really understand what you mean by "theory", you don't need to know /any/ PL theory to write Haskell and you certainly don't need to know mathematics. What specific ideas are you referring to that require advanced knowledge as a prerequisite for doing day-in-day-out programming tasks in Haskell?

Re: Urbit: A clean-slate functional OS

#117

Post by derleth »

urbit wrote: post #20
tsax wrote: post #18

Earlier quoted context omitted.

Lame qn but does the name Albert Jay Nock have anything to do with 'Nock'?

http://en.wikipedia.org/wiki/Albert_Jay_Nock http://en.wikipedia.org/wiki/Tea_at_the_Palaz_of_Hoon Four-letter names that haven't been overexposed are hard to find. But four letters fits in a 32-bit direct atom, so the attraction is pretty irresistible.

> But four letters fits in a 32-bit direct atom, so the attraction is pretty irresistible.

Reminds me of how ITS limited filenames to six letters per component, because they used six bits per character and six times six is thirty-six bits, or one machine word.

To this day, HAKMEM ('Hacks Memo') is still called that:

http://en.wikipedia.org/wiki/HAKMEM

Re: Urbit: A clean-slate functional OS

#118

Post by mietek »

urbit wrote: post #110
colanderman wrote: post #102

Earlier quoted context omitted.

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.) th…

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…

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.

Re: Urbit: A clean-slate functional OS

#119

Post by Darmani »

tikhonj wrote: post #93
urbit wrote: post #88

Earlier 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…

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.

Re: Urbit: A clean-slate functional OS

#120

Post by urbit »

freyrs3 wrote: post #116
urbit wrote: post #113

Earlier quoted context omitted.

My experience is that there are two very different kinds of Haskell programmers: those who really understand the math, like you, and those who treat it as a black box (the "Learn You A Haskell" contingent). As a black-box language, I think Haskell is of nontrivial value, but the black box is very deep and weird. This is a UI problem. If you expect people to understand the theory, this is also a UI problem in a differ…

> If you expect people to understand the theory, this is also a UI problem in a different way. I don't really understand what you mean by "theory", you don't need to know /any/ PL theory to write Haskell and you certainly don't need to know mathematics. What specific ideas are you referring to that require advanced knowledge as a prerequisite for doing day-in-day-out programming tasks in Haskell?

Again, you have to be able to perform the same computation as the type inference algorithm - for any inference engine, any type system, any language, you can't use it if you don't know what it's going to do.

There are a lot of different ways of handling this problem in Haskell - some involve knowing the notations and results of the branch of math called "PL theory," some don't.

As UIs, they all have drawbacks - and we know this, because you and I both know all the ways Haskell is awesome and rocks. We also know what people say when they complain about Haskell. They're complaining about exactly this material - so why not take the customer at his word?

Post reply on HN