urbit

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?

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.

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.

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.

You can get rid of the whole name reduction system. Which is hardly trivial. If you assume it, though, it's true that everything else is trivial.

Getting symbol tables, functions, environments, free and bound variables, etc, etc, out of the fundamental automaton, frees you up to design them right at the higher layer where they (IMHO) belong.

This philosophical argument has serious practical ramifications, I think, because it leads directly to the Question of Why Lisp Failed. Why did Lisp fail? Many people say, because it couldn't be standardized properly.

Why couldn't it be standardized? Because the Lisp way is not to start with a simple core and build stuff on top of it, but to start with a simple core and grow hair on it. So you end up with a jungle of Lisps that are abstractly related, but not actually compatible in any meaningful sense. This is because the lambda calculus is an idea, not a layer.

Basically the point of Nock is to say: let's do axiomatic computing such that it's actually a layer in the OS sense. The way the JVM is a layer, but a lot simpler. Lambda isn't a layer in this sense, so it doesn't provide the useful abstraction control that a layer provides.

mi prami la lojban .ui

Sigh, HN really is turning into - never mind. :-)

Yes. And that's what many people find so elegant about Lisp.

But, one could argue, the "is it a function? or is it a macro?" confusion is a significant cognitive load on the Lisp programmer. These are really two different things, even though you can fit them into the same namespace.

Hoon has the different problem that you allude to - it is hard to extend the macro set at the user level. While this is fairly limiting, many FP languages, like Haskell, seem to do just fine without macro extensions. Perhaps typedness plays a role.

The bottom line on this problem is that there does remain a fair chunk of unused ASCII digraph space, so there is probably a way to put that in the programmer's power, but user-level macros are an unsolved problem in this relatively young language, nor is it one that obviously needs to be solved. But it would be nice if it does get solved.

It's a different approach to learning that I think favors the actual learning curve, not the perceived learning curve.

Your brain is actually built to memorize symbols like this. (I feel I know the learning process pretty well because I have toddler-aged kids who are also learning Chinese.) Of course, kids are not grownups, but even for grownups the process of binding symbol->meaning is easier than it looks like it should be.

Also, when you have name->meaning, the name inevitably is chosen for orthographic reasons and supplies its own meaning, which may mislead from the actual definition of the primitive. If you bind a symbol directly to a semantics, you lose this source of confusion. It is replaced (ideally) by an odd sense of "seeing the function," which I think is also present in experienced Perl ninjas.

Yes, but Hoon would need them. Lisp gets a lot of things for free because it's based on the lambda calculus, which some regard as trivial but I don't.

So, for example, lambda in Hoon is not a primitive but a relatively high-level built-in macro. This means it is part of a larger family of lambda-like things, many of which are (IMHO) quite useful. On the other hand, all these things demand either reserved words, digraphs or Unicode glyphs.

Here's one way to think about it.

You have a Facebook profile, right? That's essentially a special-purpose cloud computer - a cloud information appliance. But, wouldn't it be cool to have an actual personal computer in the sky? Where "Facebook" or whatever would just be... a program on that computer?

You can get a Linux box in the sky, easy. But... that's 15 million lines of code you're wrangling. On a network which makes Helm's Deep look like Mayberry.

So, if it's your home in the cloud, it's not a cute little bungalow in the cloud. It's a giant castle in the cloud guarded by experienced professional elf ninja warriors. And ya know, even experienced professional elf ninja warriors, when they're off duty, like to let their hair down and not be thinking about orcs every other minute.

So if you want the bungalow in the cloud, you need basically a new programming/execution environment, and oh also a new network. So basically a new everything. So, a person could despair, or he could go build a new everything...

Restricting symbols to a strict subset, rather than a strict superset, of global keyboards in practice, is about cultural literacy in practice.

If you put unicode in variables, perhaps because you're using a national keyboard with special unicode powers, your code will be extremely hard to work with for programmers using a different national keyboard. Thus, even if you could do it, you shouldn't.

Now, the symbols on American programmers' keyboards are not all on every keyboard in the world - but pretty much every programmer in the world knows how to find them. Thus, sticking with ASCII is basically sensible use of Postel's Law in the language design context.

In comments - it should be ok but I think it breaks right now. Not a high priority bug, but definitely a bug.

You're saying, why are reserved words a bad idea? I think most defenders of the humble reserved word would consider it, at best, a hack. Maybe it's a necessary hack, maybe not.

With reserved words you are overloading two very different namespaces, the space of language primitives and the space of user functions/variables. Sure, you can get away with this. But do you want to? A language is a UI, and the potential for confusing the programmer is immense. If operators and functions are really different things - as they are in Hoon, anyway - it's very confusing to mush them together.

Well, of course, Larry Wall is a god.

But that said, the main difference between Hoon line noise and Perl line noise is that most of the ASCII we use has a very regular structure, with a (relatively) limited set of exceptions. So it looks about equally alien at first, but the Hoon ideogram (digraph) set should be easier to learn. Unfortunately at present the set of people who know it is very small - so the theory really hasn't been tested.

It is what it is. But at least there's no Unicode. (Not that you can't have Unicode in strings, of course.)

And anyone who doesn't like line noise has to stand up for reserved words. Some of us welcome that conversation...

That's an excellent criticism. Of course the problem is exacerbated by the HN link pointing to the philosophy doc. The greatest philosophy is to have no philosophy at all, but perhaps we're not quite there yet.

Actually the K&R equivalent for Hoon doesn't exist yet, and when it does it will be the first thing to read. Since it doesn't, the Arvo tutorial is the first thing to read:

http://www.urbit.org/2013/08/22/Chapter-1-arvo.html

But this itself is incomplete. Watch the video first:

http://www.urbit.org

Then build Arvo and use the sekrit code it generates to, basically, subscribe to our newsletter.

It's just a bad idea to document anything before it works completely, because you end up with doc that validates this criticism. The right way to build a language is to build it, use it, get comfortable with it, actually master it and become an expert of sorts... then document it. Sadly, not too many of us can live up to this ideal.

Yeah, it's true, the one in our kernel is O(n^2) though. Why? Because we're lame. But it hardly matters, as you'll never get anywhere with either O(n) or O(n^2) addition...

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.

I agree entirely! This is so much better than the typical "middlebrow dismissive" that I upvoted it...

And actually, if you don't like Hoon you can build your own language on this platform. So long as it compiles to Nock. You'll probably have to write your first compiler in Hoon, but we do have pretty decent combinator parsers. If you can swallow the syntax...

Thanks, but Avro is someone else's cool project!

(Arvo is named for http://en.wikipedia.org/wiki/Arvo_P%C3%A4rt.)

It's fairly easy to make them non-brittle, because it's very easy to rig a testing framework to run both the hand-optimized "jet" and the pure code, and compare them.

Standardizing performance is a subtler and more interesting point. It's a fairly safe bet that anything in the kernel that needs to be is jet-propelled. Above that layer, who knows? Good old normative text may handle it.

But in general, the feeling should be like the difference between hardware GL and software GL. The developer doesn't see it and the user sees it only as fast versus slow.

Have fun!

I recommend you start with the Nock tutorial:

http://www.urbit.org/2013/08/22/Chapter-2-nock.html

The build instructions in this file are out of date, use the ones from the Arvo chapter. Also, probably the best short overview is the header comment in the Hoon compiler:

https://github.com/urbit/urbit/blob/master/urb/zod/arvo/hoon...

Also don't miss the video: https://vimeo.com/75312418

A better link would be the front page: http://www.urbit.org/

I guess on the Internets, you never release anything - it's released for you. Please be warned, (a) the doc is incomplete, (b) if you create an Urbit ship you'll eventually have to destroy it, as we don't have continuity yet.

A demo video: http://vimeo.com/75312418