Urbit: A clean-slate functional OS(urbit.org)

262 pointsby tsax13 yıl önce178 comments

http://www.urbit.org/

47 comments

urbit13 yıl önce

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.

Touche13 yıl önce

Watching the video blew my brains out the back of my head. Figuratively of course. Thanks for not letting me get anything productive done for the rest of the day.

msutherl13 yıl önce

The music is great. I stopped watching and just listened while continuing to get work done.

rxdazn13 yıl önce

Brian Eno - An Ending (Ascent) http://www.youtube.com/watch?v=It4WxQ6dnn0

state13 yıl önce

So here I am, in a submarine, learning a foreign language. What an afternoon.

tsax13 yıl önce

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

urbit13 yıl önce

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.

sbmassey13 yıl önce

Nothing to do with Frank Key's absurdist narrative "Ascent of the Mountain at Hoon", then? http://hootingyard.org/archives/9019

tsax13 yıl önce

Nice! Thought so.

derleth13 yıl önce

> 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

saidajigumi13 yıl önce

For a project ostensibly inspired by K&R C, the copy on this site is amazingly opaque and full of its own rhetoric. Recommendation: delete all the linguistic posturing and get down to the hard work of casting light on your ideas. Let that speak for itself.

By way of example, the K&R C book had a beautiful clarity and ability to fluidly move between the realms of reference, spec, and tutorial. If you're going to hold K&R C up as a model, you'd do well to mimic its documentation philosophy.

urbit13 yıl önce

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.

bjz_13 yıl önce

I for one love the whimsy. We need more LearnYouaThings and Shoes and runtimes that spit out lovecraftian quotes...

stuaxo13 yıl önce

I really enjoyed reading this + a some of the pages.

Very mindbending, got up to watching the video.

Am thinking it looks like it could be quite fast, I guess it would make sense to implement something like ContextFree in it as a start.

groovy2shoes13 yıl önce

I thought the style was a refreshing departure from the usual tone of expository technical documents. I actually enjoyed reading it, even though I disagreed with many of the assertions that were made.

lewispollard13 yıl önce

Personally, I was reminded of the schizophrenic guy on HN who built his own OS.

groovy2shoes13 yıl önce

I often enjoy Terry's writing as well.

wmf13 yıl önce

It seems like Urbit is art for art's sake. The fact that it executes is a side benefit.

(Oops, fyolnish beat me to it.)

jahewson13 yıl önce

I couldn't agree more. I don't want to know about how awesome the author is or how he's cunningly outsmarted everybody else. I'd like to see his ideas put forward without trashing other people's and with some theoretical context rather than just denunciations of PL theory.

Too much hot air.

zzzmarcus13 yıl önce

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/

clarkm13 yıl önce

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

mietek13 yıl önce

I will not comment on the judgement passed upon the education system. The second article exhibits eristic tricks, obfuscatory language, and a plain confusion of ideas, especially when speaking about proof-carrying code and type theory.

It's interesting to see the author wishing for a Python of functional programming, and yet Hoon's syntax appears deliberately obscure.

However, there is one paragraph with which I wholeheartedly agree:

> I think the world could use a charity that funds creative programming. The software systems that people use today — don't even start me on "Web 2.0" — are awful and ancient, and hardly anyone has any reasonable plan to improve them. Free-software programmers are not at all bad at supporting themselves, but nothing like Xerox PARC exists today, and it should.

It should, and, hopefully, it will. Soon.

drewhk13 yıl önce

Deliberately obscure, yes:

>We should note that in Nock and Hoon, 0 (pronounced “yes”) is true, and 1 (“no”) is false. Why? It’s fresh, it’s different, it’s new. And it’s annoying. And it keeps you on your toes. And it’s also just intuitively right.

clarkm13 yıl önce

Well, it's no different than Unix:

https://en.wikipedia.org/wiki/True_and_false_(Unix)

samth13 yıl önce

The fact that it's by a guy who's an unreconstructed racist and thinks the US is inevitably headed for anarcho-capitalist dystopia (except that he doesn't think it's dystopian) certainly reinforces my initial opinion that it's nuts.

colanderman13 yıl önce

"""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/

.

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

urbit13 yıl önce

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.

andolanra13 yıl önce

"PL theory", the field of study, contains many, many theories of programming. There is not a lambda calculus, there are several (e.g. the untyped lambda calculus, the simply typed lambda calculus, System F, Martin-Löf's dependent type theory, among others) although not all of them are Turing-equivalent (the lack of which can be a useful feature), as well as other systems which are not based on lambda (e.g. concatenative calculi, which correspond roughly to things like Forth.) In fact, from a quick perusal, it seems that Nock is a minor variation on a graph rewriting system with the graphs restricted to DAGs, so... a studied and established theory of computation.

Similarly, there are techniques for representing code as data that are quite widely known and understood in programming language theory, e.g. through Danvy's defunctionalization or the use of arrows to make explicit the structure of computation or stage-separation and things like Lisp macros. These also are not ignored in the field of PL theory.

Effectively, my criticism is that your practical understanding of "PL theory" amounts to a mostly-remembered reading of "Types and Programming Languages," and so you are accidentally reinventing things poorly and describing them in an ad-hoc way. Now, Nock and Hoon and the others are quite interesting and impressive, and I plan to keep following them in the future, but I still assert that, rather than standing on the shoulders of giants as you could be, you've dismissed them as windmills and are trying to climb your own way.

freyrs313 yıl önce

Arguably there's a lot of folks reinventing things poorly in ad-hoc ways, doubtful that will ever change. What's more concerning is the flagrant anti-theory attitude that, at least to me, seems to be on the rise. In the context of discussions around Haskell or Agda it's sadly common to see "mathematical" bandied around as a synonym for "impractical".

colanderman13 yıl önce

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

urbit13 yıl önce

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

colanderman13 yıl önce

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!)

urbit13 yıl önce

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.

urbit13 yıl önce

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.

tikhonj13 yıl önce

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.

urbit13 yıl önce

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.

colanderman13 yıl önce

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.) then your program won't type. Otherwise it will.

Importantly: it doesn't matter how you come to this conclusion; the compiler will use the H-M algorithm, but that doesn't mean you need to. You can just look at your "if" expression and realize that you're returning an integer in one branch and a string in the other and that that violates the "non-union non-dependent" requirement above.

(This, BTW, is an example of the difference between a spec (what I outlined above) and an implementation (what the H-M algorithm says to do).)

urbit13 yıl önce

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

colanderman13 yıl önce

As a side note, you should check out Erlang's static checker, Dialyzer. It implements a complete (i.e. no-false-positives) type system, as opposed to a sound (i.e. no-false-negatives) type system (e.g. H-M and friends). It pretty much eliminates the need to make any predictions about what the type checker will say, as it will only complain if your program can provably crash due to a type error.

Of course this still permits the possibility of type errors, but in practice it works fairly well, and does not constrain the programmer.

mietek13 yıl önce

Dialyzer is decent, given the constraints for which it was designed, but nowhere near as helpful as a ML-derived static type system.

For example, Dialyzer won't reject a function declared to return values of type A and actually returning values of type B along an execution path which isn't currently traveled.

samograd13 yıl önce

> One is to build an abstract mathematical model which you can emulate in your head

The ability to emulate your abstract or concrete programming model in your head cannot be overemphasized. I used to program the original 8-bit B&W Gameboy, which was a machine so simple and small I could literally emulate it at the clock cycle level while I was writing the code for it.

If you can fit your model into your cache (brain) you can do amazing things using just your wetware.

mietek13 yıl önce

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.

dgreensp13 yıl önce

I sense a fallacy lurking here. Sure, a type system like Haskell's or even Scala's is magic (and can be used without understanding it) as long as it can "Do What You Mean," but when it can't, you have to understand its workings. We can't sweep that fact under the rug by calling any failure to "Do What You Mean" a bug, a wart to be fixed -- a deviation from correct DWYM behavior. There is no actual DWYM type system, or at least no one's ever come up with one.

What type system doesn't have warts? Haskell's probably has both more and fewer than most, depending on how you count them, because so much emphasis is put on the type system.

When you use any language long enough, you end up needing to simulate pretty much every observable aspect of it yourself -- not including, for example, the garbage collector, the JVM bytecode verifier, or the GCC code optimizer, which are supposed to be transparent, but including the type inferencer, the JVM threading model, and the JavaScript semicolon insertion rules, which are not. Some of these things you can steer clear of for a long time or even avoid forever by staying on the beaten path, but they lurk, waiting for the thousands of people who have run into bugs or compiler errors and needed to understand them.

I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.

mietek13 yıl önce

Let's not confuse Hindley-Milner type inference with Haskell's (or ML's) type system.

While Haskell's type system can be complex, depending on the exact language extensions in play, Hindley-Milner type inference is simple. It's just good UI — you almost never need to write explicit type declarations, because the compiler (or typechecker) can almost always figure out what you mean. That's it!

Using advanced Haskell extensions can occasionally require annotating a non-top-level value with a type, in order to resolve an ambiguity. The compiler will point out which value has an ambiguous type.

Also, if you've made a mistake and your program doesn't typecheck, depending on whether explicit type declarations have been provided or not, the compiler may complain about different parts of the program. Adding type annotations may help pinpoint the exact location of the mistake. This isn't really a problem, and it's more of an issue in SML and OCaml than Haskell, because these languages don't encourage annotating top-level values with types.

There is never any need to simulate any part of the Hindley-Milner type inference algorithm in your head. The algorithm's only failure mode is a request for more information, and the requested information should already be obvious to you, the programmer, as programming in a ML-derived language means thinking in terms of typed values.

The warts I had in mind were problems with the Haskell ecosystem, such as Cabal hell, or the Haskell community, such as a tendency towards academese — not anything to do with its type system, or type inference mechanism.

In a stark contrast, Scala's "type inference" is not Hindley-Milner, and is barely able to infer the existence of its own arse with both hands, failing in even the simplest of cases.

Example 1. Unable to infer type of `optBar`, because `None` is also a type:

    scala> class Foo {
         |   def setBar(bar: Int) = optBar = Some(bar)
         |   def getBar = optBar.get
         |   var optBar = None
         | }
    <console>:8: error: type mismatch;
     found   : Some[Int]
     required: object None
             def setBar(bar: Int) = optBar = Some(bar)
                                                 ^

Workaround:

    scala> class Foo {
         |   def setBar(bar: Int) = optBar = Some(bar)
         |   def getBar = optBar.get
         |   var optBar: Option[Int] = None
         | }
    defined class Foo

Example 2. Unable to infer type of `foobar`, with uncurried `foo`:

    scala> def foo(bar: Int, baz: Int) = bar + baz
    foo: (bar: Int, baz: Int)Int

    scala> val foobar = foo(1, _)
    <console>:8: error: missing parameter type for expanded function ((x$1) => foo(1, x$1))
           val foobar = foo(1, _)
                               ^

Workaround:

    scala> val foobar = foo(1, _: Int)
    foobar: (Int) => Int = <function1>

Workaround, with curried `foo`:

    scala> def foo(bar: Int)(baz: Int) = bar + baz
    foo: (bar: Int)(baz: Int)Int

    scala> val foobar = foo(1)_
    foobar: (Int) => Int = <function1>

Which languages have "basic unidirectional type inference"? I'm not familiar with the term.

colanderman13 yıl önce

Scala […] is barely able to infer the existence of its own arse with both hands, failing in even the simplest of cases.

Thanks for this. Not only did I lol, but this confirmed my suspicion that Scala was "not the language I was looking for" to use for an upcoming project (a compiler that, for business/politics reasons, must run on the JVM). You've no doubt spared future me regret.

tikhonj13 yıl önce

Check out ermine[1], a language for the JVM that was written for exactly that reason. It's being used at S&P Capital IQ. You can look at the user guide[2] for more information.

[1]: https://github.com/ermine-language

[2]: https://launchpad.net/ermine-user-guide

mietek13 yıl önce

Thanks for pointing it out!

tikhonj13 yıl önce

I think you're just projecting your familiarity with things like RFCs as somehow more intuitive. People have plenty of problems with the network stack and its associated abstractions! TCP/IP or even just HTTP lead to plenty of confusion. In a vacuum, I am not convinced the RFC would be any easier than a paper on Hindley Milner. (Wikipedia is not a good replacement for either.)

"Intellectual level" isn't exactly a well-defined term. It inevitably conflates the inherent complexity of something with the background needed to quickly understand it. The difference in the two articles is not in how accessible they are to somebody with no relevant background--both the RFCs and H-M would make no sense to a layperson!--but in the fact that they target different audiences.

Both are very stupid in the same way: they are very explicit about every little detail. It's just where an RFC uses technical terminology mixed with a legalese-like language (SHOULD and MUST and so on), H-M uses mathematical notation and inference rules. I do not believe that one of these is so much more inherently difficult to understand than another; it's much more a matter of experience and background knowledge. Without that, reading either is going to be relatively slow and laborious. Having gone through both RFCs and type theory, I've found both similarly slow in terms of content; the main difference is that the mathematical notation happens to be much more dense. So perhaps it takes me five times longer to get through a page about type theory as a page of an RFC, but that single page contains the same amount of information, just encoded differently.

Also, I don't buy that you have to understand how the inference works to use it, any more than you have to understand or think about the OSI model to write networking code. You can use both perfectly well--and most people do--without needing to think about or understand everything. Moreover, you won't be able to learn either without a good deal of work and the relevant background. I suspect that it just happens that the background for one matches much more closely with yours than the background for the other.

Sure, humans as a species are not very good at mathematics. But they aren't very good at engineering either! They are really bad at keeping a bunch of details in memory and running (even simple) algorithms in their heads. All told, it's better to avoid it.

urbit13 yıl önce

For the source of my bias, I have actually spent a considerable amount of time working with people in the "RFC world." For example, I wrote the kernel of the Openwave WAP browser, which shipped about a billion units, even if it sucked and no one used it. I have spent just about no time in the PDF world, and even when I was in grad school I was an OS guy. (Here's a fun old paper of mine: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7...). So, zero time in the "PL theory" world.

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.

bcoates13 yıl önce

My instinct is to agree with urbit here but I just wanted to thank you for the sudden enlightenment that many intelligent people probably find legalese, spec-ese and RFC-speak (or as I refer to it, "plain English prose") as awkward and unnecessarily painful to read as I do conventionally written math papers.

It sounds trivial and self-evident written down like that but most long overdue revelations probably do.

Darmani13 yıl önce

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.

mjmahone1713 yıl önce

You can solve this, to some extent, in OCaml, by just type-hinting everything. But then what fun is type inference?

freyrs313 yıl önce

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

urbit13 yıl önce

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?

freyrs313 yıl önce

> 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 programmers" is that they've taken the time to learn the language. In my experience many people turn away from Haskell because they can't immediately transfer their existing knowledge into it and don't like feeling like a beginner again, so they stop. I've met many /more/ people who think that programming in Java is too smart for them as well, it's just a matter of putting the time in to learn.

urbit13 yıl önce

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.

freyrs313 yıl önce

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

urbit13 yıl önce

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?

freyrs313 yıl önce

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

My whole argument is that you don't need to know anything about the implementation of the inferencer to use it, you don't need to predict it's behavior anymore than you need to model the CPU instruction selection of the compiler in your head. Most of the time you can safely program at a level of abstraction that doesn't involve the implementation of the language, and in Haskell this "normal level" is well above the level that involves low-level things like the lambda calculus.

I think we're just an impasse, the meme that you need mathematics or PL theory to program in Haskell is one that puzzles me and I don't understand where it comes from. Best of luck on your project.

dgreensp13 yıl önce

I'm not sure it's realistic to say someone could make a career in a programming language without being able to look at a function and deduce the static type of a value without asking the computer.

As I wrote elsewhere in the comments:

When you use any language long enough, you end up needing to simulate pretty much every observable aspect of it yourself -- not including, for example, the garbage collector, the JVM bytecode verifier, or the GCC code optimizer, which are supposed to be transparent, but including the type inferencer, the JVM threading model, and the JavaScript semicolon insertion rules, which are not. Some of these things you can steer clear of for a long time or even avoid forever by staying on the beaten path, but they lurk, waiting for the thousands of people who have run into bugs or compiler errors and needed to understand them.

I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.

I could imagine citing C++ as a counterargument -- no one understands the type system, but people use the language anyway -- but it's still not an abstraction you don't have to understand to use, like a CPU.

Dewie13 yıl önce

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

I don't think that LYAHFGG treats Haskell as a black box, not for the level that it aims to teach Haskell - it makes it very clear that all functions are curried, emphasizes that a functor should be viewed more as of a "computational context" instead of a "box" (for example function composition), and so on. I've found it to be as precise and vigorous as other tutorials on Haskell, for the level it aims at.

colanderman13 yıl önce

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?

urbit13 yıl önce

But my previous reply is a little content-free, as what you're really asking for is how we solve the same problem that typeclasses solve in Haskell.

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.

mietek13 yıl önce

It's difficult to have a conversation with someone using their own terms for well-established concepts.

If I understand you correctly, what you're calling "geometric polymorphism" is usually called structural typing or subtyping, and what you're calling "generic polymorphism" is usually called duck typing.

Duck typing isn't amenable to static typechecking, so it's not comparable to Haskell's typeclasses.

mietek13 yıl önce

Looks like I'm behind on my programming language theory research! Typed Racket and soon, Typed Clojure, are actually adding optional static typing to duck-typed languages. Are you doing something similar?

urbit13 yıl önce

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.

mietek13 yıl önce

That's a bit underwhelming.

offensivehandle13 yıl önce

why, would you prefer some other answer than 'false'?

now, the real question is whether Hoon thinks that (= 5 "5"), or (= 100 "1e2"), or (= 4 "four"), like some languages helpfully provide.

mietek13 yıl önce

The question posed by colanderman's expression is valid if and only if there is a type containing both 5 and "foo".

Here's Haskell's answer:

    Prelude> \ a b -> a == b && b == 5 && a == "foo"

    <interactive>:2:25:
        No instance for (Num [Char]) arising from the literal `5'
        Possible fix: add an instance declaration for (Num [Char])
        In the second argument of `(==)', namely `5'
        In the first argument of `(&&)', namely `b == 5'
        In the second argument of `(&&)', namely `b == 5 && a == "foo"'

Here, the typechecker took the most general type of 5, namely some type belonging to the Num typeclass, and discovered that the type of "foo", which is [Char], isn't an instance of the Num typeclass, or, in Java parlance, doesn't implement the Num interface. This means there is no type containing both 5 and "foo", hence — type error.

You're asking about implicit conversions, which are an undisputable evil. However, attempting to provide answers to invalid questions also isn't very good.

You may have already seen the rather entertaining Wat talk, by Gary Bernhardt: https://www.destroyallsoftware.com/talks/wat

The central theme of this talk is not just implicit conversions — it's surprising answers to invalid questions. A much better way to handle an invalid question is to reject it as early as possible — Fail Fast. With a static type system, this can be very early indeed.

jsd198213 yıl önce

I was with you til you introduced the Hoon syntax. Why ruin a great concept with a shit language? WHAT IS WRONG WITH LANGUAGE DESIGNERS?! Just come up with a sane language with a sane syntax on a great platform. This is apparently asking a lot. It's not fucking rocket science.

urbit13 yıl önce

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

jsd198213 yıl önce

I like that you upvote your critics. That amuses me greatly. I had not viewed the video before I made my first comment but after watching the video I'm impressed with your implementation and solid practical concepts, but I still abhor your Hoon syntax. I haven't looked into Nock yet but I have a feeling I might knock its syntax as well, pun intended.

eli_gottlieb13 yıl önce

Hoon is a high-level language which defines itself in Nock. Its self-compiling kernel, 7000 lines of code, specifies Hoon unambiguously; there is no Hoon spec. 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, unification, or other constructs from “PL theory.” Hoon also excels at handling and validating untyped data, a common task on teh Internets. Its syntax is entirely novel and initially quite frightening.

Crank detected. Homing in for the kill.

urbit13 yıl önce

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

nutate13 yıl önce

Oh wow.

After watching the video I'm legitimately interested in more than the language. You've got some cool ideas going on there. I'll be emailing for a 32-bit destroyer in a second.

gwern13 yıl önce

>I ate something I shouldn't have the other day and ended up having this surreal dream where Mencius Moldbug had gotten tired of the state of the software industry and the Internet and had made his personal solution to it all into an actual piece of working software that was some sort of bizarre synthesis of a peer-to-peer identity and distributed computing platform, an operating system and a programming language. Unfortunately, you needed to figure out an insane system of phoneticized punctuation that got rewritten into a combinator grammar VM code if you wanted to program anything in it. I think there even was a public Github with reams of code in it, but when I tried to read it I realized that my computer was actually a cardboard box with an endless swarm of spiders crawling out of it while all my teeth were falling out, and then I woke up without ever finding out exactly how the thing was supposed to work.

http://lesswrong.com/r/discussion/lw/ipu/open_thread_septemb...

yebyen13 yıl önce

I distinctly get the impression that the authors of this project will already know what Lojban is. This language (especially when you get to the part about reserved words, actually made up with special characters as runes, and how to pronounce them) made me think of the structure of Lojban right away.

For anyone who hasn't heard of it, http://www.tlg.uci.edu/~opoudjis/lojbanbrochure/lessons/

Urbit of course having the advantage that it can be programmed in... the video is very cool!

Ixiaus13 yıl önce

The first time I have ever seen someone mention Lojban in the wild!!! How exciting!!

urbit13 yıl önce

mi prami la lojban .ui

nemo161813 yıl önce

ge'edai

yebyen13 yıl önce

I googled, got 1/3 of the way through "Subsequent UI Cmavo", and gave up.

If you explained in lojban, I promise I'd struggle a few minutes longer before giving up :D

http://www.lojban.org/tiki/Subsequent+UI+Cmavo

I read Arabic fairly well but I did not understand Lojban, not having any framework to understand it in, whereas I took Arabic classes for basically four years of college.

I got "prami" to mean love, and .ui to mean ":)"

Why do you put .i at the beginning of some sentences?

nemo161813 yıl önce

Disclaimer: I'm no lojban expert myself, so this may be inaccurate.

{mi prami la lojban .ui} is pretty straightforward: I love lojban, plus the {.ui} attitudinal, which indicates happiness (or as you said, ":)").

The period {.} is an interesting part of lojban. It indicates a glottal stop. Most words in lojban start with a consonant, so glottal stops are placed before words that begin with a vowel (mainly just attitudinals and names). This is to prevent words from flowing into one another when speaking rapidly, which is important since one of the design goals of lojban is to avoid ambiguity.

{.i} is actually punctuation: it marks the boundary between sentences. All punctuation is pronounced in lojban. This may sound exhausting, but again, it reduces ambiguity.

{ge'edai} is intended to mean "I know that feel" -- {ge'e} meaning "unspecified emotion" and {dai} meaning "empathy" -- but I'm not sure if combining them is grammatically correct. Perhaps {dai} alone would be more accurate.

yebyen13 yıl önce

I know about . and it makes sense to me because of hamza in Arabic. It's the same. It's not a letter, it only serves to reduce ambiguity, but they wouldn't say it's punctuation either. Thanks for breaking it down for me!

yebyen13 yıl önce

Next I'm going to bring up the name FactorCode because I like namedropping languages :)

FeepingCreature13 yıl önce

Well, I've read most the docs, let's say _skimmed_ the code examples, and I think you're a very smart, competent engineer with a sense of what makes for good language syntax that is utterly, incomprehensibly alien to me. So I guess, martian-language mission accomplished?

fyolnish13 yıl önce

This is art.

"There is never a reason to program in Nock. Except to learn Nock." Classic

quanticle13 yıl önce

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 complicated built with Perl quickly converges to unintelligible line noise (barring the exercise of zen-like discipline). If you're making something for beginners, please, please, give them the tools to build abstractions in a consistent and understandable manner.

urbit13 yıl önce

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

aray13 yıl önce

The unicode-in-strings but not in variables/etc bothers me about Java (coming from Go, where unicode is allowed in variables). It seems inconsistent to have two separate character sets for different semantic subsections of what is a single text file.

What about unicode in comments? If I put a string in a comment can it go there?

urbit13 yıl önce

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.

FeepingCreature13 yıl önce

Spread the word of .Xcompose?

quanticle13 yıl önce

I can search Google for reserved words. But I can't search Google for $@_{}

urbit13 yıl önce

Hey, man, that's all on Google as I see it.

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

nmcfarl13 yıl önce

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.

quanticle13 yıl önce

It's not age. C is older than Perl by decades, but I think C is a lovely little language. Lisp is as old as FORTRAN (almost) and I think it's probably the most elegant language invented yet. No, my quibble with Perl is that in throwing around implicit state everywhere (in an effort to make programming languages more like human languages) Perl is just bad as a system for building complex systems. It's not unique in this regard - Perl shares its weakness with the shell scripts it was supposed to replace.

pekk13 yıl önce

Python is about as old as Perl

Gavitron13 yıl önce

Larry Wall released Perl 1.0 in Dec 1987 - two years before Guido started writing Python. First usenet release of Python was Feb 1991, with 1.0 coming in 1994, with Java coming approx 1 more year later.

urbit13 yıl önce

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

mietek13 yıl önce

The video shows an utterly fascinating mixture of Lisp, Erlang, Plan 9, and Bitcoin. The only missing ingredient is a proper static type system!

agumonkey13 yıl önce

This felt like an epilog to 2001 a space odyssey. Alien world.

noonespecial13 yıl önce

With all that jargon I was expecting a set up for a punch line at the end. Don't nock it so hoon, it's not done jet. Ha!

urbit13 yıl önce

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

state13 yıl önce

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

agentultra13 yıl önce

This is really, really neat.

I really like the concepts in Avro and Urbit. Particularly interesting for me is the checkpoint/replay, distributed version control, and neighbours.

This is a really cool experiment!

urbit13 yıl önce

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

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

agentultra13 yıl önce

I think I've lost all precious free time I have... this is great stuff. :)

tlb13 yıl önce

You say addition is O(n^2), but I think you can write an O(n) addition with only increment, recursion, and equality testing.

In Python syntax:

  def add(a, b):
    return add_r(a, b, 0)

  def add_r(a, b, c):
    if b == c: 
      return a
    else:
      return add_r(a, b, c+1) +1

jcburnham13 yıl önce

Yeah... just one of the many many things we haven't gotten around to fixing. Since it doesn't really matter for a jet-propelled function.

https://github.com/urbit/urbit/issues/11

urbit13 yıl önce

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

betenoire13 yıl önce

It's python, so it can't handle it either way, but by moving the final "+1" into the function call, it becomes tail-recursive.

  return add_r(a+1, b, c+1)

[deleted]13 yıl önce

theonewolf13 yıl önce

I'm pretty sure this is a giant joke ? Or nothing is implemented yet (and still, kind of jokish especially in description)?

yebyen13 yıl önce

Is this comment a joke?

I haven't tried compiling it, but even if large parts of the documentation say "this isn't finished yet" there are code and compilation instructions for Linux and OSX. If it's a joke then it's a joke that two contributors seem to have taken very seriously for a number of months now.

EDIT: Not like, say, Flynn... jab jab

theonewolf13 yıl önce

I meant in a similar vein to say, esoteric languages or subsests like jsfuck.com.

I see this is considered more art, and I would agree with that.

It appears as if it is a large art + learning experience, and I appreciated that after I watched the movie.

Not a lot of _novel_ ideas per se, but an interesting mixture of things.

ajanuary13 yıl önce

So rather than having a lengthy standard it has lots of small non-standardized and brittle performance optimizations?

I remain skeptical over whether this tradeoff is worth it.

urbit13 yıl önce

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.

jamii13 yıl önce

What about when the pure code is too slow to run? Or when the pure code is wrong but the jet is right - so that the nook spec is now not sufficient to determine semantics.

Let me bury that criticism though by saying that this is the most beautiful piece of work I have seen in some time. If more people were willing to be a little crazy we might not be quite as tangled in spaghetti.

urbit13 yıl önce

Thanks, and you're right about both problems.

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.

sstewartgallus13 yıl önce

Because Nock is so simple (just a few substitution rules) I wonder if it'd be reasonable to formalize it in a theorem prover like Coq, or Agda to ensure correctness.

wgd13 yıl önce

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 optimizations are quite a bit less brittle than the ones you get with a JIT-compiled virtual machine.

nwmcsween13 yıl önce

This is what about 90% of the libc libraries out there do as well. Also tracing jits also do the same thing they see a trace that has a known optimization and it is performed.

dragonwriter13 yıl önce

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

wgd13 yıl önce

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.

jahewson13 yıl önce

"if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time"

This is what JITs do. At least the good ones.

lucian190013 yıl önce

That's not entirely different from what a simple JIT does (or the unoptimised stage of a JIT without an interpreter).

cldr13 yıl önce

> Hoon is a keyword-free language - any alphanumeric text in the program is part of the program. Where other languages have reserved words, Hoon has squiggles.

But... why?

urbit13 yıl önce

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.

cldr13 yıl önce

I'm not asking why reserved words are a bad idea, just opining that I think having 100 single- and double-character symbols might not be the best UI for a language. Why not have just names (neither reserved like keywords nor inscrutable like symbols?)

I don't know, I am similarly annoyed by mathematicians because they usually use single letters for variables. It's a little more excusable for them because math functions are usually very short and have few variables, but still I'd rather use words. But I digress.

urbit13 yıl önce

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.

FeepingCreature13 yıl önce

The alternative, as I see it, is to let people add new keywords to the language from inside the language, so there's feature parity again.

urbit13 yıl önce

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.

mietek13 yıl önce

In my view, CPU speed advances and a high-quality optimizing compiler mean there aren't many reasons to use macros in Haskell. People do, though; for examples of extensive Template Haskell use, see Yesod.

qznc13 yıl önce

We are pretty much done with CPU speed advances and compiler optimizations. If you use an Intel i7 with the Intel C compiler, there might be a few percent left to optimize, but not much. Free lunch is over for a decade now.

You might get more cores at the same speed, but even that seems to be limited due to heat issues.

You can get more efficient CPU (e.g. SIMD instructions) but the compiler cannot optimize for them very well. Some people say implicit SIMD is a bad idea anyways.

Touche13 yıl önce

Lisp has no reserved words.

urbit13 yıl önce

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.

Peaker13 yıl önce

The Lambda Calculus is so tiny how can you view it as anything but trivial?

Just 3 syntactic forms building up an expression tree:

  Expr = Lam Name Expr | Var Name | Apply Expr Expr

And one reduction rule:

  reduce (Apply (Lam name body) arg) = subst name arg body

At least assuming unique names (no shadowing nonsense), you can't get much simpler than this...

urbit13 yıl önce

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.

fsck--off13 yıl önce

>I think, because it leads directly to the Question of Why Lisp Failed.

Lisp isn't a failure. You're commenting on a server that is powered by a Lisp.

>Why did Lisp fail? Many people say, because it couldn't be standardized properly.

There was a very good idea about how to standardize Common Lisp back in 1982. It divided documentation into 4 different parts, or 4 different "colored pages". It was eventually abandoned because of the time constraints. Read DLW's (one of the 5 main Common Lisp authors) news.yc post about it:

https://news.ycombinator.com/item?id=81258

Read more about it here:

http://www.saildart.org/ARPA.PRO%5BCOM,LSP%5D

http://xach.livejournal.com/319717.html

Peaker13 yıl önce

Lisp isn't really the only attempt to work with the lambda calculus.

Look at Haskell, Agda, and others, which are based on an a slightly extended form of LC. I doubt anyone would claim that these extensions are "hairy".

tsax13 yıl önce

Brainfuck

nutate13 yıl önce

I really like this. I hope some younger people with more time on their hands push this farther.

tomrod13 yıl önce

I'm not sure I follow what this is. Where would I use Nock and Hoon?

nutate13 yıl önce

To build your startup? No.

To have fun? Why not.

tomrod13 yıl önce

I should rephrase my question: on what technology platforms would one use Nock and Hoon? Embedded systems? Anything (due to "portability")?

urbit13 yıl önce

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

zaphar13 yıl önce

You are still missing the point. They wrote it because it looked like fun. It's not targeting a business problem as such it's more like it's scratching the "This looks like fun" itch.

Could it maybe be used for something sure. But that doesn't have to be the motivation of the authors.

richardlblair13 yıl önce

As others have pointed out, this is art.

You don't look at art, and ask "Why did you do this??". You simply enjoy it. The artist did it, to do it, and nothing further.

If you can not see this that way, then I am truly sorry.

tomrod13 yıl önce

I see beauty in many things. I'm not yet at the level of programming where I see beauty in syntax -- maybe one day though!

nightski13 yıl önce

If it is truly art then it doesn't make much sense why he is trying so damn hard to make it practical.

richardlblair13 yıl önce

Think of it as great architecture...

tinco13 yıl önce

In the end it compiles down to C, so supposedly any system. Though the virtual machine is bound to have side effects (I/O) so you are bound to whatever platforms they have impleme ted those for, which might as well be Windows XP.

Tldr; this question warrants an answer from someone who knows.

arh6813 yıl önce

Would you mind doing lots more screencasts? Maybe writing a jet, rigging a test, profiling, and maybe a bunch of other things. I very much like your demo style, and I have a hunch these docs are going to be pretty dense. ;)

jpt413 yıl önce

From pedestal to pinnacle, all things are quantum, not classical. The metaphor that better avoids scaling obsolescence for your project is perhaps Bohmian, rather than Maxwellian.

dmytrish13 yıl önce

Codex Seraphinianus of programming?

I think it's a true piece of postmodern art.

samograd13 yıl önce

    So if we had to read the above decrement...we’d say: 
    “luslus dec sigfas cen dec bartis a tis pat sigbar soq
    dec soq ketcab pat wutgal tis pel zero a per tislus b 
    tis pat barhep wutcol tis pel a lus pel b per per b buc 
    pel b lus pel b per per.”

Absolute brilliance.

eonil13 yıl önce

Though I couldn't understand them fully...

The names are awesome! The concepts are awesome! And the music is awesome!!!

eonil13 yıl önce

I see some similarity to Smalltalk or Windows PowerShell. And this made me to imagine typed Smalltalk/Objective-C style syntax on shell which would be great for usability...

offensivehandle13 yıl önce

Shell programs are expected to take streams of data and produce other streams of data. Shell programs are also supposed to, but often don't, have uniform configuration options. Instead, we have ps ax | grep chromium | grep -v grep | awk '{print $1}' | xargs kill

* ps accepts ax with no -

* awk is its own programming language lol

* xargs gets pretty complicated if anything bigger than this happens

(incidently, I know about awk '/chromium/ {print $1}' and killall. but i have seen that command line in the wild. because some people don't read the awk manual for fun, and i'm not sure if every unix system even has a killall command)

...and yet the shell is still the preferred tool for what it does because everything else requires too much typing (of both varieties)

Apparently urbit also has streams of raw data. It's about time someone came up with a new idea for a shell that keeps what's great about the shell (though personally, i would standardize on streaming a form of json, because it turns out that data is very often found as scalars, lists, and mappings).

So anyway. If urbit actually ends up being better to live in than unix, and having shell programs that are configured in exactly one way would be an improvement, and having data that's easier to parse than plain text while remaining as easy to read as plain text would also be an improvement, well, I've always wanted to live in a submarine. If it gets a nice editor and c++ compiler, that is. I do need the best performance possible out of my computer for my work.

offensivehandle13 yıl önce

Okay, since you want comments here, here I'll put mine.

The reason you were so successful in coming up with a new political philosophy is that your "I'm a Martian" trick got you think thoughts that no respectable person would be caught dead thinking.

There aren't the same taboos in computer system design, so while you can refer to the systems people use every day as gigabytes of, what was it, of ass fucking more ass, there's nothing you say that I haven't already heard.

I'm still waiting for the Python of functional programming. Paul Graham announced Arc when I was in middle school. Maybe it will be released as the scripting system in Half-Life 3.

Being an alien from Alpha Centauri, and observing the growing collection of programming languages, what do you think people keep designing new ones for? Why do some Urplatians argue for Scheme and other Urplatians for Python?

Rather than asking the question of 'what is a programming language', and trying to design the axiomatically simplest possible thing, try asking the question of 'how do people use programming languages'.

Is your system a bit of syntax regularization away from the pseudocode people scribble on paper to explain algorithms to each other? No, that's Python.

Is your system something that compiles down to use the bare metal to its fullest potential while maintaining as much creature comforts as possible? No, that's C++.

Is your system something with an ancient history of having a solid ABI, that in fact every other language's ABI is described with? No, that's C.

Is your system a heap of cruft upon kludges with the original intention of providing programming access to a hypertext document? That's Javascript.

I wouldn't want to write a regex as anything but a regex.

In conclusion, you're asking a question that's been asked before and getting an answer that's been gotten before. But, maybe it is finally time for functional programming to come back. Maybe you're a popular enough guy to get people to use your system.

davidgerard13 yıl önce

"Being an alien from Alpha Centauri, and observing the growing collection of programming languages, what do you think people keep designing new ones for? Why do some Urplatians argue for Scheme and other Urplatians for Python?"

Typical mind fallacy. http://lesswrong.com/lw/dr/generalizing_from_one_example/

Most people model other people as just like themselves, plus or minus a diff. The trouble is that they don't understand just how wide-ranging human thoughts and feelings can be, and assume they will understand and be able to model based on the diff, even if the diff is larger than their whole mind.

It's why geeks keep coming up with "intuitively obvious" schemes no-one else can understand, and why engineers are routinely surprised at what actual end users do with their products in user testing.

So people write new languages that suit their personal peculiar ways of thinking. Thankfully, many are quite aware that this is what they are doing and don't claim universality.

This is why Urbit is art: translating numbers and ASCII characters into nonsense syllables that you are actually expected to pronounce and think in suits Yarvin's mind, even as it leaves me thinking "there is such a thing as being too much of a Borges fan". Which is absolutely fine. But this is why Urbit is art (an expression of a unique personal vision), not anything people are actually going to use without similar levels of confusion to the present.

For an example of fully rampant Typical Mind Fallacy in Urbit, see the security document: http://www.urbit.org/2013/08/22/Chapter-6-security.html About two-thirds of the way down, you can actually see Yarvin transform into Moldbug and start pontificating on how humans communicating on a network should work, and never mind the observable evidence of how they actually have behaved whenever each of the conditions he describes have obtained. The very first thing people will do with the Urbit system is try to mess with its assumptions, in ways that its creators literally could not foresee (due to Typical Mind Fallacy), though they might have been reasonably expected to (given the real world as data).

alfredjaynock13 yıl önce

So this is what moldbug does in his spare time.

[deleted]13 yıl önce

melloclello13 yıl önce

Hey Moldy I just want to say 'ur-bit' is a pretty cool name B-)

cdcarter13 yıl önce

I can't tell what I'm more confused/impressed by, Hoon or the social model. Either way, I've got a destroyer and now I'm trying to understand just how zod works.

mhartl13 yıl önce

Congrats on the launch (even if teh Internets did it for you)!

dreen13 yıl önce

Love the fact you used music by the god of ambient, Bran Eno.

wgd13 yıl önce

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.

jamii13 yıl önce

Haskell has rewrite rules which is how eg stream fusion is implemented.

http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/rewri...

JulianMorrison13 yıl önce

I love this concept of jets and how it allows a "completely isolated" VM to magically grow connections to the real world.

perlgeek13 yıl önce

A VM that can be precisely described in 200 words? Does that include the IO subsystem? I have my doubts that it's possible to describe a full set of IO operations that any modern VM needs in so few words, just because of the wealth of features that you usually need (file system access, sockets (TCP and UDP), pipes, IPC, ...)

sr-ix13 yıl önce

I dig the Borges references riddled about.

0xdeadbeefbabe13 yıl önce

Reminds me of the punchline, "consider a spherical cow"

> To a Pascal purist, to anyone who thinks mathematically, this seemed hideous. C isn’t really a high-level language at all - it’s a glorified macro assembler. Mankind retreats to the cave.

Leaky abstractions are hideous too, don't you think?

sz4kerto13 yıl önce

Astonished.

Reminds me a bit of A+, however. :)

quarterto13 yıl önce

  Hoon also excels at handling and validating untyped data, a common task on teh Internets.

Not sure if satire?

[deleted]13 yıl önce

batemanesque13 yıl önce

using "teh Internets" on yr front page is a great way to put off anyone who doesn't subscribe to calcified "geek culture"

jyf198713 yıl önce

so its root in forth?

[deleted]13 yıl önce

dancecodes13 yıl önce

without flash of course there

dancecodes13 yıl önce

video not work in ff linux

offensivehandle13 yıl önce

i just finished watching it in firefox on a freshly-installed linux mint 15

dancecodes13 yıl önce

nothing appropriate, gentoo and Im too lazy for fixing it (=^‥^=)

losethos13 yıl önce

[deleted]13 yıl önce