urbit

In any language, a type defines a set of values and some semantics for manipulating those values. It so happens that our way of defining common sets is to build a function whose range is some useful set.

Actually any gene (ie, expression) has a product range. It doesn't even need to be a function. So the range of the constant

[%foo %bar]

whatever the subject is, is always [%foo %bar], ie, the pair [7.303.014 7.496.034].

So, if we have another function and we call it with a noun of that type, we know the range of the input, we know the code in the function, we can infer the range of the output. It's not terribly rocket scientific.

Previous HN discussion: https://news.ycombinator.com/item?id=6438320

This is a perfectly serious type system that infers perfectly serious types all day long. It is moronic, though.

By the way, I don't think there's anything wrong at all with bribing early adopters. Just sayin'...

If I had to get the whole new operating system, etc, through the IETF, I might agree with you!

You know, all your questions have the same answer. Of course no standard can control the behavior of a remote server. But when you have an environment in which mutability is neither expected nor produced, any violation of immutability is easily recognized as a bug - and (in a highly specified system like Urbit) a very unlikely bug.

Whereas whatever conventions you add to the W3 environment that say "this resource is immutable," pretty much everything in that environment is "overloaded with a number of purposes, which don't always mesh very well" - and if the receiving end of a protocol actually treats your conventions as if they were ironclad rules, it's violating Postel's Law. There's just too much "give" in the whole system, and that's a mistake that's much easier to not make in a new system, than to fix in the old one.

Urbit runs on Linux right now - but you're right, it would be very cool to run directly on the hypervisor, and it's totally possible for a self-contained system like this one. Personally I think Haskell never should have tried to be a language for producing Unix system calls - the impedance mismatch between FP and imperative OS is just too great.

If an event depends on data that's been deleted, that event never happened. But, at the Unix level (which can generate any events it wants), we can generate another event which reports the error. So it's not like things fall silently down the hole, either. (For the same reason, you can also get the stack trace of the infinite loop that was interrupted by your ^C.)

No, but you have to decide how your code will behave if it detects a change. Should it keep a hash and report an error?

But that's just a matter of adding an RFC to describe how to mark URIs as naming immutable resources.

That's certainly an interesting way to use the word just. You don't strike me as someone who first heard of the IETF yesterday.

And besides, we already have an RFC that does exactly that. It's RFC 2616 - use Cache-Control: max-age. Except that - this channel is polluted with crap information, because lots of sites set their cache-control wrong and don't mean it.

So you need a new channel that isn't polluted with crap information. Maybe we're agreeing after all.

Why does it require completely reworking the Internet infrastructure from scratch?

DNS is also not referentially transparent. Nor are HTTP responses signed by DNS identities.

When all is said and done, you have a new service by any standards. Why layer the new service (which is much simpler than the old service) over the old ball of mud? If you want to talk to it from the ball of mud, write a gateway.

(But not for everyone - just for everyone who doesn't have powerful enemies. That's why it's essential to abstract across cloud hosting and personal hosting. If people who have powerful enemies and need to host at home have the same experience on the network as most people (who don't have powerful enemies), except that their enemies can't own them in some data center, they experience a kind of "herd immunity." Everyone doesn't need privacy against powerful enemies - everyone just needs to be able to obtain privacy, without deleting their digital lives, if they find out they have powerful enemies.)

The problem is when you try to build immutable resources on top of a mutable namespace. How exactly do you know they're immutable? By what convention? What happens to your code if they mutate?

Even worse, using a mutable-namespace for immutable bindings, you have two immutable systems talking to each other through a mutable pipe. First the kind of transformation you describe has to be applied, then it has to be reversed. It's a recipe for madness.

Prediction: one day my protocol will run on top of yours. Rebuilding teh Internets, one layer at a time...

It's easy to build mutable resources on top of an immutable namespace. Just put the date, change number, or label, in the name. But once you stop being referentially transparent, you can never recover that virginity. There was sort of an attempt to make Cache-Control headers work in HTTP, but they really don't (I speak as a recovering browser developer), and there's just no substitute for everything having an infinite lifetime.

Basically thanks to HN, 8300 people have watched a 10-minute screencast of a command-line session. Totally insane. My lovely and talented wife, who put together this video, was really hoping people would spend more time watching it than it took to edit.

Edit: And Google makes my point and VJ's brilliantly, by breaking the link to his Google TechTalk. Brilliant!

Basically, the Internet has spam because identity isn't a limited resource. IP addresses are kind of a limited resource, but they're not really the property of the person using/abusing them, so a blacklist doesn't inflict precise targeted damage, can't be made too draconian, and is easy to evade in lots of ways.

And everything above the IP level is unlimited. If there's an unlimited supply of identities, you can't tell the difference between a new customer and an old enemy. You want the first to have positive default reputation and the second to have infinite negative reputation.

People in the personal cloud community often point to email as proof that spam can be solved. Yes - but spam was solved in email because email already existed in an spam-free Internet. On the Internet we have, there's a much easier solution to the fact that any new protocol which is successful starts to attract spammers. The solution is: stop using the protocol. Google turned off XMPP federation for this very reason.

Basically in an orc-infested environment, you can't have your own cute little bungalow in the cloud. You gotta have an apartment in a giant fortified castle in the cloud.

Having a limited supply of identities, in which identities are (a) property and (b) property you control cryptographically (Bitcoin style, "allodial title"), makes it easy to make spamming not pay, once the price of an identity is greater than the profit a spammer can earn by burning it. And it does not require a central governance authority, or even a central reputation authority. (Reputation authorities shouldn't be built into any system, because if they abuse their own reputations the consequences are insanely dire.)

NAT is a problem, but there are lots of ways to tunnel around it. Which all suck, of course, but...

I'd dispute the point about the CAP theorem slightly. Thing is, your data - Little Data - is naturally centralized. It doesn't have to be centralized in the same center as everyone else's data though! Then it becomes Big Data, where it's having this giant privacy-violating orgy with everyone else's data all day long.

The amount of traffic that your own Little Data has to serve, unless you're a celebrity in which case you can pay for serious hosting, is never going to require a giant cluster of replicated servers. So CAP just isn't that much of an issue.

The other talks are great too! Watch them all!

Very briefly, there's two ways of asking whether a caller can change the type of a parameter. The normal way is to say, are all the possible values of the caller's type in the set of nouns that the parameter defines? This is what I call "geometric polymorphism."

But there's also "generic polymorphism," in which we ask: will the Nock code that was generated for the parameter type, actually work with the type we're calling it with? A really stupid way to ask this is to recompile the function, with the parameters exchanged for the arguments. The Hoon approach is a little bit smarter than this but not much.

So, with these two approaches, you basically get variance and genericity, which is all of polymorphism.

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?

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.

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.

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...

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.

And besides, I can't Google for "go." And yet, Go seems to be doing just fine...

One, it takes a good bit of work to boot Arvo beyond a merely correct nock interpreter. The Hoon type system, for instance, is enormously painful if not jet-propelled.

Two, the kind of bug you're describing is in fact the nastiest class of bug. The best way to get around it is to always make sure you write the pure code first. But this isn't possible in a variety of circumstances - and it sure wasn't possible when making Hoon first compile itself. So, as inevitably in the real world, there is no substitute for not screwing up.

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...

&(=(a b) =(5 b) =("foo" a))

and it'd work just fine.