PYF Dark Enlightenment Thinker

The Something Awful Forums > Main > Post Your Favorite: Carefully Curated > PYF Dark Enlightenment Thinker

Krotera: Jun 16, 2013; I AM INTO MATHEMATICAL CALCULATIONS AND MANY METHODS USED IN THE STOCK MARKET

Urbit, Arvo, Nock, and Hoon (by Mencius Moldbug, a genius of the Dark Enlightenment)

code:

!:             ::  To write Nock as an Arvo application in Hoon
|=  *          ::
|=  [a=* ~]    ::  For educational purposes only
:_  ~  :_  ~   ::
:-  %la        ::  Preserve this mysterious boilerplate square
%+  sell  %noun::
.*  a          ::  Replace the formula with your own
:::::::::::::::::
               ::  Formula: increment
[4 0 1]

quote:

In some languages, especially functional languages, types are dangerous scary concepts that involve a lot of math. For those who like this sort of thing, that's the sort of thing they like. For the rest of us, there's Hoon. It's a functional language, but not one of those scary ones.

quote:

In this case, looking directly at the type noun is preferable. But for a core, the type actually contains the entire codebase.

quote:

Essentially all Hoon compiler errors are in a sense type failure. Generally, the compiler wants to shield you from the direct details, because most ways of presenting the direct details automatically would, at least in certain cases, just belch all over the screen.

quote:

Syntactically, any atomic constant can be preceded by % to generate a cube. The exception is @tas, which always needs % and is always cubical.

quote:

An unsigned decimal not broken into groups is a syntax error.

quote:

The semantics of the time system are that UGT (Urbit Galactic Time) is GMT/UTC as of leap second 25.

quote:

A loobean, or just bean, is 0 or 1. 0 is yes, 1 is no. People who find this strange are probably strange themselves.

quote:

We've seen @p used for ships, of course. But it's not just for ships - it's for any short number optimized for memorability, not for arithmetic. @p is great for checksums, for instance.

That said, @p is subtly customized for the sociopolitical design of Urbit as a digital republic. For example, one feature we don't want is the ability to see at a glance which carrier and cruiser issued a destroyer. Consider the carrier 0x21. It issues 255 cruisers, including 0x4321. It issues 255 cruisers, including 0x4321. Of course, anyone who can juggle bits can see that ~famsyr-dirwes is a close cousin of ~lidlug-maprec. But she actually has to juggle bits to do it. Obfuscation does not prevent calculated associations, just automatic ones.

quote:

@tas, a term, is our most exclusive odor.

quote:

Our mutual hope is that by the time you do know Hoon, you will simply be able to see a twig like
code:
|=  a=@
=|  b=@
|-  ?:  =(a +(b))
      b
    $(b +(b))
and, far from merely able to follow this code, actually observe in your mind's eye the function itself - not unlike Keanu with kung fu. You will simply look at this strange collection of squiggles and see decrement.

(Our feeling is that the use of reserved words in most languages, by instead activating the verbal lobes, disrupts this sense of directly, or at least visually, perceiving the program itself. If you object that this sounds too much like Science, Science implies testing hypotheses whereas we generally just wing it.)

... If we had to read this twig, omitting the spaces (which only a real purist would pronounce), we'd say: "bartis A is pat tisbar B is pat barhep wutcol tis pel A lus pel B perper B bucpel B luspel B perper." The authorities would then arrive, and drag us out in a big net. Definitely don't do this at the airport.

quote:

What is a tile? First, concretely, a tile is an AST subtree that's reduced statically into a twig. It can be reduced in four ways - cryptically called bunt, clam, fish, and whip. A tile is always some leg of a twig, and that twig defines how the tile is reduced.

... A tile is actually two steps away from being a type, in the strict sense of ++type. The tile is converted statically into a twig, which in turn may (depending on the conversion) produce the icon, test for it, etc. And always, the icon is some function of the tile and its subject.

quote:

The rules for using an %iron core are that (a) the context is opaque (can neither be read nor written), and (b) the sample is write-only. Why? Because it's absolutely okay to use as your comparator a gate which accepts a more general sample than you'll actually call it with. You can write a more specialized noun into this sample - but if you read the default value and treat it as more specialized, you have a type loophole.

A %zinc (covariant) core is the opposite - the context remains opaque, the sample is read-only. We don't use any %zinc at present, but this is only because we haven't yet gotten into inheritance and other fancy OO patterns. (Hoon 191 had inheritance, but it was removed as incompletely baked.) You make a %gold core %zinc with ^& (ketpam, %ktpm).

Finally, the entire payload of a %lead (bivariant) core is immune to reading or writing. So all that matters is the product of the arms. You make a lead core with ^? (ketwut, %ktwt).

quote:

When the arm we're executing is %elm, not %ash, there is actually no check that the payload in the actual core, type p, nests in the original payload q.q.

Moreover, %elm arms (defined not with ++ or slus, which means %ash, but +- or shep) are actually not even type-checked when compiled. They have to generate valid nock, but all verification is disabled.

quote:

Let's deploy this boy! Here is ++list:

++ list |*(a=_,* $|(~ [i=a t=(list a)]))
Don't worry. This is just grievously badass hardcore Hoon - as irregular as Marseilles street slang. As a novice Hoon monkey, you won't be writing ++list or anything like it, and you can stick to French as she is spoke in Paris.

On the other hand, at least this grizzled old baboon has no trouble parsing the apparent line noise above. Why so funky? Why, oh why, _,*? Because for various irrelevant reasons, the ++list here is trying as hard as possible to build itself out of tiles.

quote:

Note that list and lust do the same thing and are perfectly compatible. But sadly, lust still looks like line noise. Let's slip into something more comfortable.

quote:

There are three main ways we can talk about a core: its variance model, %gold, %iron, %zinc or %lead, %gold by default; the inference approach of each of its feet, %ash or %elm, informally dry or wet, dry or ash by default; and its payload pattern, which makes it a gate, reef, book, trap or tray. There are also several ways of using cores: you can pull, kick, slam or slug them

...A core whose payload is either another core, or a constant (%cube), is a book...A book whose payload is either another reef, or a cube, is a reef. Effectively, a reef is an entirely constant core...Any core with one arm named %$ is a trap. "It's a trap!"...A gate is a trap whose payload has the form [sample context], sample being dynamic data and context being anything...A tray is any core whose payload has the form [sample context]...Every reef is a book. Every gate is a trap. Every gate is a tray.

As we already know, a name or axis (which of course applies to all nouns, not just cores) is a limb. A list of limbs is a wing.

To access a wing or limb in a core is to pull it. When we write a.b.x, we pull the wing a.b (ie, a within b) from x. If the result is defined as a subtree of x, the wing is a leg. If it is computed from x by a formula, it's an arm.

To pull %$ - the empty name - on a core is to kick it. To replace the sample with a in gate g then kick the gate, is to slam g with a.

[many paragraphs later]

The gonad rune is ;~, [%smsg p q]. A gonad has one go, the V part - p in [%smsg p q] - and one or more nads, the F, G, H or I parts (q).

(If you want a real thrill, read the chapter on type inference!)

Krotera has a new favorite as of 06:47 on Oct 6, 2014

# ¿ Oct 6, 2014 06:42

Adbot: ADBOT LOVES YOU

# ¿ May 8, 2024 11:05

Krotera: Jun 16, 2013; I AM INTO MATHEMATICAL CALCULATIONS AND MANY METHODS USED IN THE STOCK MARKET

Political Whores posted:

Is the name Hoon a reference to something?

He makes occasional cryptic references to Australia, where it's a slang term for a rude person, but none of the terms or mnemonics have explicit justifications, and that includes the name.

Oh, by the way, this is articulated in a few different places but not super clearly and not all that consistently -- these are the apparent meanings of the terms he uses for things related to his language:

Nock: the assembly language
Hoon: the compiled language a few inches above the assembly language
Arvo: the OS/bridge to conventional system functionality (Arvo : Hoon :: UNIX : C)
Urbit: the combined infrastructure and philosophy

I don't understand Hoon well enough to concisely describe what the entities being manipulated are and his prose style's a little too grandiose and self-important to draw clear definitions from. Nock is exhaustively specified but the Hoon material is more of a tutorial series, and it's a pain to decipher even though the breezy style makes it seem like it ought to be pretty simple.

# ¿ Oct 6, 2014 07:53

Krotera: Jun 16, 2013; I AM INTO MATHEMATICAL CALCULATIONS AND MANY METHODS USED IN THE STOCK MARKET

Ratoslov posted:

That Hoon poo poo is some of the most deliberately impenetrable documentation for anything I have ever seen. Is there actually a compliler for this pile of poo poo?

If I remember right, the implementation was actually pretty good! That said, I didn't work on it personally, and the language itself is not very computationally tractable for the same reason that Peano numbers aren't -- the issue being that Peano numbers can be optimized-around (see i.e. Idris) while expressing literally everything in terms of weird tree traversals is harder to do that for.

Look up the "jet" feature if you want an explanation of how the language was supposed to become computationally tractable: it's basically a hashtable from Nock entities (plus some heuristics for more general patterns) to native code with some simple laws to prevent people from doing anything foolish. (speaking in relative terms)

Just being clear if you didn't figure this out from the documentation -- it's basically a notation for side-effect free tree traversals (Nock) and a bunch of opaquely-named macros that implement an idiosyncratic type system with inference (Hoon). (Like I said, the type inference rules are really strange and hilarious: among other things he claims it only works "forwards", not "backwards" -- which is a pretty ridiculous notion if you try to apply it to for instance Algorithm W or a Prolog evaluator.) Anyway, he then wrote a bunch of software on top of that (Arvo) and released it all to the internet (Urbit).

The novel features were basically supposed to be

- builtin distributed computing functionality better than what you get trying to repurpose Unix et al for cloud computing. He probably failed at this because Urbit's weird numeric representations make a lot of constant-time algorithms unanticipatedly linear or worse, so your code overall scales badly no matter what. (Numbers aren't the only thing Urbit represents strangely, but they're a great example.)

- a syntax and mnemonics that intuitively corresponds to how people think about algorithms in ways that the syntax in related languages (probably Lisp, Haskell) doesn't. I'm not a cogpsych student and neither is he, so who knows if he got it right? (He probably didn't.) He starts from a similar jumping-off point to Haskell in that names in Hoon don't have to be meaningful so long as they're distinctive, but I'd argue that his mnemonics are deliberately obfuscating in a way that Haskell's just aren't. It's like how "functor" and "superman" don't mean anything in the context of programming to someone who hasn't been told, but "functor" at least doesn't have an alternate denotation to distract you from what's really meant.

- a type system that teaches people to think about algorithms in a way that makes code easy to maintain and reason about. (explicitly less powerful than the type systems in related languages like Haskell and Agda, which he claims are too confusing for the average programmer) I'm skeptical of some of the advantages he proposes and I think most of the ground he's claiming isn't new, but was already found in dynamic languages like Lisp. I think several of the features of his type system are needlessly confusing and I'd personally rather start by simplifying Haskell (Readerizing typeclasses, expressing records in terms of sugar over other types like i.e. in Vinyl, coming up with a way to emulate dependent types that isn't confusing, etc.) -- minding that I'm a Haskell nerd so of course I'd say that.

- new control flow and organizational primitives that make it easier to express algorithms in his languages than in other languages. I'd argue he's reclaiming the same ground as goto -- clearly in the sense that you can express any control flow you want, goto is the most powerful control primitive. By designing his language as a transparent layer for tree manipulation, obviously you get all the power of tree manipulation, but most of the time what we want isn't tree manipulation or unconditional jumps anyway, but strong abstractions around it, and I don't trust Hoon's abstractions given that they take him forever to explain and don't make sense after even three or four readings. (compare to i.e. continuations and monads, which are grokkable after one reading and a pot of coffee respectively, once you're experienced with the prerequisites.)

MinistryofLard posted:

What was wrong with a regular Boolean that necessitated an almost, but not quite, identical type?

It wasn't "intuitively right." Just trust him.

Dean of Swing posted:

I feel like I am reading an alien text.

That's a design feature.

Krotera has a new favorite as of 05:25 on Oct 9, 2014

# ¿ Oct 9, 2014 05:06

Krotera: Jun 16, 2013; I AM INTO MATHEMATICAL CALCULATIONS AND MANY METHODS USED IN THE STOCK MARKET

I figured Mencius Moldbug's whole persona was basically an attempt to ape _why and other self-deprecating self-absorbed hacker figures -- silly name included. Compare the rhetoric in the Urbit docs ( http://doc.urbit.org/doc/ ) to i.e. the rhetoric in The Poignant Guide to Ruby (http://mislav.uniqpath.com/poignant-guide/) or The cDc #200 Higgledy-Piggledy-Big-Fat-Henacious-Mega-Mackadocious You-Can't-Even-Come-Close-So-Jump-Back-K-BOOMIDY-BOOMIDY-BOOM File. (http://www.textfiles.com/100/cDc-0200.txt)

# ¿ Nov 27, 2014 07:57

The Something Awful Forums > Main > Post Your Favorite: Carefully Curated > PYF Dark Enlightenment Thinker