8 ms·

Hoon's Moronic Type System

62 points by somedude99 13y ago

agentultra 13y ago
Staring at this until my brain goes fuzzy, but it looks like a kind of sequent calculus. Is that far off the mark?
- urbit 13y ago
  I don't think so, but I wouldn't know enough to tell you. I can tell you that I am not very interested in 20th-century formal logic, at least as a way of defining programming, but you knew that. I think it seems like a logical equivalent that my approach is not very interesting from the standpoint of 20th-century formal logic.
  - agentultra 13y ago
    Must be my monkey-brain trying to explore the unfamiliar by finding similarities to what I already know. I may of course simply be looking through a bottle (and constrained by backwards-tracking logicians). All of this is starting to smell of an Incompleteness Theorem of Programming Languages.
    - agentultra 13y ago
      I think I get it now. Sort of like a sequent calculus without the logic backtracking. Instead of proving anything Hoon just defaults it to something. Or crashes. :)
Vivtek 13y ago
This is actually Chapter 8 of the punishment book from Anathem, right?
comex 13y ago
A language that has "cube", "face", "stem", "bulb", "coil", "foot", "battery", "gene", "gold", "iron", "ash", and "yew"... It's not that other languages don't make up arbitrary terms as well, but it's hard to understand why a language that claims to be simple and "moronic" does it so enthusiastically, with the result that anyone trying to learn it has to first memorize a large number of terms.
- urbit 13y ago
  Basically, I'd say, ordinary human beings are much better at memorizing words and symbols than most smart people think - and much worse at understanding highly abstract concepts. Think of the number of things you need to memorize to be an auto mechanic. Yet there are a large, large number of people who are capable of becoming auto mechanics, but not capable of becoming Haskell programmers.
  - nnq 13y ago
    Shouldn't we compare the abilities of people vs. computers? Computers can store a lot in their memory, but it's pretty hard to make them prove theorems, whereas humans are pretty bad at memorizing anything and pretty good at abstraction. ...and since a programming language should be primarily designed for humans (or, as I actually see it, a programming language should be an interface between the human mind and the computer) and at the same time be executable by computers, choosing more memorization and less abstract concepts seems like a bad idea ...most smart people's minds find juggling abstract concepts easier and more enjoyable than memorizing rules (and when working memory is not enough to hold all the abstract concepts we're juggling, we use anything from pen and paper to other more advanced devices - just ask any mathematician), and those that don't are also those that "just don't get (or like) software", so they shouldn't be programming anyway.
    - urbit 13y ago
      I agree with your goals but not with your observations. Perhaps I'm biased by the fact that I have small children. I am regularly amazed by their ability to memorize words, numbers, symbols, etc, combined with complete incompetence at abstract concepts. Grownups are different, of course, but it's still natural that most of what I know about learning comes from my own kids.
humbledrone 13y ago
I'm disappointed to see the depressingly common male-genetalia-centric humor in "Gonadic" combinators. I find myself agreeing with much of the forward-thinking, throw-the-past-away design of Hoon/Nock, but it's jarring to find this kind of asinine brogrammer mentality mixed in with it. Yet another sling and/or arrow of discomfort for the half of the human population that already has to put up with too much of this shit. [EDIT] As a reply points out, Gonad is gender neutral. I still think that this humor is distasteful.
- jcburnham 13y ago
  ...the term "gonad" is gender-neutral. http://en.wikipedia.org/wiki/Human_gonad http://en.wikipedia.org/wiki/Human_gonad
- urbit 13y ago
  It is an understandable comment. Maybe we'll rethink it. Bad taste is a social construct, but you live in the society you live in... On the other hand, the identity dialogue defaults unwary bros to %lady, which certainly ought to cause a little wailing and gnashing of teeth.
samatman 13y ago
Nock made me suspect Mencius is a Kabbalist. This metal and wood business confirms it. Hoon is still far and away the most WTF part of Urbit from my perspective. Nock: brilliant. Urbit proper: obviously the right thing. Hoon: line noise or poetry? I remain totally undecided. Eagerly awaiting comprehensive documentation of the digraphs.
- aaronem 13y ago
  From chapter 4: > So if we had to read the above decrement, omitting the spaces (which only a real purist would pronounce), 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.” Kabbalist? This sounds more Holy Roller to me. I plan to spend at least some of the upcoming weekend with Urbit. It should be interesting, to say the least.
- samograd 13y ago
  My take on hoon is to use[2] the alphabetic names of the line noise operators to create words and use them to make a non-symbolic (if you take alphanumeric characters as non-symbolic) functional, executable conlang[3]. To me it's what Liebniz was looking for[1], but with funny looking words that make no sense to the uninitiated, which use the 'linguistic nodules' that cgyarvin is hoping to utilize, without the symbolic name decoding that using line noise requires (if you use the names in [2] rather than the line noise symbols). I personally think hoon looks like absolute brilliance, but I can't say yet that I've had the pleasure to write anything in it, which is the best thing to take that shiny feeling away by actually trying to use it. But as art, I think it's perfect. [1] http://sunsite.utk.edu/math_archives/.http/hypermail/historia/may99/0211.html http://sunsite.utk.edu/math_archives/.http/hypermail/histori... [2] As follows from http://www.urbit.org/2013/08/22/Chapter-4-syntax.html http://www.urbit.org/2013/08/22/Chapter-4-syntax.html: ace space gal < per ) bar | gar > sel [ bas \ hax # sem ; buc $ hep - ser ] cab _ kel { sig ~ cen % ker } soq ' col : ket ^ tar * com , lus + tec ` doq " pam & tis = dot . pat @ wut ? fas / pel ( zap ! [3] https://en.wikipedia.org/wiki/Constructed_language https://en.wikipedia.org/wiki/Constructed_language
samograd 13y ago
(_Gonadic combinators_? Yes - using our gonad rune, semsig or ;~. If you are a sophisticated professor type and understand monads, gonads may seem real familiar to you. Out here in Urbit world we are just dumb country peasants and all we got is gonads. This is the South Park of system design, or at least it makes me laugh just as much. These guys are great although the software is still a bit fragile.
auggierose 13y ago
I have no idea what any of this means.
- auggierose 13y ago
  Ok, I just clicked on the link and what I saw there just didn't make any sense to me :-) Still doesn't now, but after reading the comments, I returned to the site and studied it more carefully. Maybe the link should point to chapter 0, not chapter 5, to have any idea about what this is about ... After reading chapter 0 now, I can understand the goal of urbit, and I think it is a great one! But note that you can work on exactly the same goal without leaving PL theory and theorem proving entirely behind you. Check out http://proofpeer.net http://proofpeer.net to see how this might be possible.
  - urbit 13y ago
    That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indifferent substrate. But... +1 for an exciting vision of math uber alles.
archgrove 13y ago
I'm presuming this is "in joke" that I'm very much out of. I honestly have no idea what this is about at all, nor can I find any context.
- urbit 13y ago
  More context from the front page: http://urbit.org http://urbit.org. Previous HN discussion: https://news.ycombinator.com/item?id=6438320 https://news.ycombinator.com/item?id=6438320 This is a perfectly serious type system that infers perfectly serious types all day long. It is moronic, though.
  - tsukikage 13y ago
    > This is a perfectly serious type system that infers perfectly serious types all day long ...in a submarine.
    - samatman 13y ago
      Your desktop isn't wood, your folders aren't manila, and your windows aren't glass. Why balk at a submarine? It's made of the usual combination of bits and vivid metaphor.
      - tsukikage 13y ago
        My desktop is most certainly not wood, it's %gold ;) Who's balking? I'm right there under the water. I find myself craving a destroyer, without quite knowing what I'd do with one ;)
andrewcooke 13y ago
anyone got a summary for people with less patience or an apparently broken sense of humour?
- urbit 13y ago
  Hoon is a very stupid little higher-order type-inference engine that does not use Hindley-Milner, category theory, etc. Higher-order functional programming is so cool it should be accessible to the majority of human beings who unfortunately happen to be bad at math. Also, layering a type system on top of an untyped data model has various practical benefits - eg, your types can be used as validators for untrusted data you got over the network.
  - deleted 13y ago
    [deleted]
  - samatman 13y ago
    You appear to be saying, among other things, that a noun is of a particular type if it may be passed through a function that parses and validates that, yes, those bits may be treated in that fashion. Is that accurate? There's clearly more to it, as there's at least one conceptual leap between that notion and any kind of inference.
    - urbit 13y ago
      The type, as a set of nouns, is the range (excuse me, "codomain") of a function. So, if we have another function and we call it with a noun of that type, we know the range of the input, we know the code in the function, we can infer the range of the output. It's not terribly rocket scientific.
      - samatman 13y ago
        This explanation falls apart for me because the third time you use the word "function", it can refer to either of the two referents you already introduced. I think you're saying a type is the range of inputs to function1 which succeed by not crashing; given function2 and a noun in the type, we may use function1 to infer the range of values which function2 must accept? Maybe?
tikhonj 13y ago
This might be an interesting project if not for the constant misguided crusading against a PL theory straw man. It's a sort of anti-intellectualism I find particularly galling, but it seems lamentably common in some nooks of the programming world.
- freyrs3 13y ago
  I find the whole hubris of this article kind of alarming, I'm not sure if the author is doing this out of some form of satire or whether he/she actually think that the "disciple of PL theory is just full of misguided imbeciles who use formal words I don't like". The attacks on TAPL too are seemingly weird, because arguably it's one of most thudingly concrete and down to earth books on types ever written. The whole book is about applications to real world problems and reveling in the fact that one haven't read it seems very asinine.
  - urbit 13y ago
    Obviously if you have a door that needs to stay open, a thudingly concrete... never mind. All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right? PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.
    - freyrs3 13y ago
      > Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? Yes I have read TAPL, it's sitting on my desk right now. I'm not even sure what you're trying so say, the fact that a book on type system design doesn't have advice on Java* seems perfectly natural to me. A book on goat husbandry doesn't have advice on Rails development. What are you trying to say? > PL theory is not the theory of programming, any more than TAPL is the doorstop. This is the strawmen that you're arguing against that seems bizarre to many people. PL theory is not so much about the lambda calculus and Hindley-Milner as it is about applying rigor and discipline to the study of programming languages. And yes, sometimes that involves learning the mathematical formalism. * Chapter 19 in TAPL actually does have an implementation of Java's type system.
adultSwim 13y ago
I actually find a lot of arguments he presents compelling. However the general thrust seems to be that programming language should be accessible. Hoon seems to fail that test. I've yet to see how this is better than vanilla ML. I don't see that because Hoon doesn't use standard syntax or terminology. I can't just read some code and a language overview to decide if this is worth (a lot of) my time. I think ML has a fairly steep start-up cost but is definitely understandable by regular people and has real productivity benefits. Hoon is sufficiently obfuscated that it has an incredibly high barrier to even evaluate as a language. I don't think you need to have tons of unintelligible typing rules to make things familiar. By avoiding standard syntax and terminology, it puts an enormous burden on the potential user.
- urbit 13y ago
  Some UI burdens seem high, some are high. An interesting class of UI problem is the set of things that intuitively look difficult, but actually aren't. Human brains are incredibly good at raw memorization of associations. Hoon has about 100 digraphs, and their internal structure isn't random. How hard is to learn 100 characters of Chinese? Perhaps easier than you think. Nor are there no payoffs. For instance, most languages are very bad at defining large, mostly static hierarchical trees, so when it comes time to write code that generates, say, an HTML page, you reach for a special "template language" DSL. That's not a problem we have in Hoon. Also, most functional languages have a very annoying tendency to crawl off the right side of your screen and disappear, because indentation depth matches functional depth. That's also not a problem we have in Hoon. So... you pay, definitely. But you also receive.
- samatman 13y ago
  I'd like to address this obliquely with a question to urbit: Is it always the case that the vowels may be compressed away without loss of meaning? It seems to work some/most of the time, but there is a least a %wet and %wut... I think? Though this be method, yet there is madness to it.
  - urbit 13y ago
    There's %wet but no ++wet. The name of the character is actually just the name of a parser function for it.
adultSwim 13y ago
By the way, what's with all the hate on Ben Pierce? Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or category theory. Just straight programming and simple proofs. That's a world where previously the few who entered were sucked down a rabbit hole of theory, never to return again.
mritun 13y ago
This is work of pure brilliance!
pekk 13y ago
Perl for type systems?
itsuart 13y ago
First of all, I didn't read linked article. Which is wrong of course. As usual, I'm basing on comments in this thread. So you want to do type system without PL theory of modern age. Awesome! Seriously, interesting experiment. Unless you already have read TaPL in which case I fear you would antagonise ideas described there. However, there is a non-merit, non-technical problem: dismissing PL theorists is sounds like dismissing PL theory (wrong implication, but that is how humans are I believe). And this will put you into JS/PHP/whatever-back-to-the-trees basket and your ideas will be dismissed just because of this wrong association. Which means, that you will distorted results of your experiment. How do you plan to alleviate that? Or I'm wrong somewhere and it is non issue?

62 points by somedude99 13y ago

agentultra 13y ago

Staring at this until my brain goes fuzzy, but it looks like a kind of sequent calculus. Is that far off the mark?

urbit 13y ago
I don't think so, but I wouldn't know enough to tell you. I can tell you that I am not very interested in 20th-century formal logic, at least as a way of defining programming, but you knew that. I think it seems like a logical equivalent that my approach is not very interesting from the standpoint of 20th-century formal logic.
- agentultra 13y ago
  Must be my monkey-brain trying to explore the unfamiliar by finding similarities to what I already know. I may of course simply be looking through a bottle (and constrained by backwards-tracking logicians). All of this is starting to smell of an Incompleteness Theorem of Programming Languages.
  - agentultra 13y ago
    I think I get it now. Sort of like a sequent calculus without the logic backtracking. Instead of proving anything Hoon just defaults it to something. Or crashes. :)

Vivtek 13y ago

This is actually Chapter 8 of the punishment book from Anathem, right?

comex 13y ago

A language that has "cube", "face", "stem", "bulb", "coil", "foot", "battery", "gene", "gold", "iron", "ash", and "yew"... It's not that other languages don't make up arbitrary terms as well, but it's hard to understand why a language that claims to be simple and "moronic" does it so enthusiastically, with the result that anyone trying to learn it has to first memorize a large number of terms.

urbit 13y ago
Basically, I'd say, ordinary human beings are much better at memorizing words and symbols than most smart people think - and much worse at understanding highly abstract concepts. Think of the number of things you need to memorize to be an auto mechanic. Yet there are a large, large number of people who are capable of becoming auto mechanics, but not capable of becoming Haskell programmers.
- nnq 13y ago
  Shouldn't we compare the abilities of people vs. computers? Computers can store a lot in their memory, but it's pretty hard to make them prove theorems, whereas humans are pretty bad at memorizing anything and pretty good at abstraction. ...and since a programming language should be primarily designed for humans (or, as I actually see it, a programming language should be an interface between the human mind and the computer) and at the same time be executable by computers, choosing more memorization and less abstract concepts seems like a bad idea ...most smart people's minds find juggling abstract concepts easier and more enjoyable than memorizing rules (and when working memory is not enough to hold all the abstract concepts we're juggling, we use anything from pen and paper to other more advanced devices - just ask any mathematician), and those that don't are also those that "just don't get (or like) software", so they shouldn't be programming anyway.
  - urbit 13y ago
    I agree with your goals but not with your observations. Perhaps I'm biased by the fact that I have small children. I am regularly amazed by their ability to memorize words, numbers, symbols, etc, combined with complete incompetence at abstract concepts. Grownups are different, of course, but it's still natural that most of what I know about learning comes from my own kids.

humbledrone 13y ago

I'm disappointed to see the depressingly common male-genetalia-centric humor in "Gonadic" combinators. I find myself agreeing with much of the forward-thinking, throw-the-past-away design of Hoon/Nock, but it's jarring to find this kind of asinine brogrammer mentality mixed in with it. Yet another sling and/or arrow of discomfort for the half of the human population that already has to put up with too much of this shit. [EDIT] As a reply points out, Gonad is gender neutral. I still think that this humor is distasteful.

jcburnham 13y ago
...the term "gonad" is gender-neutral. http://en.wikipedia.org/wiki/Human_gonad http://en.wikipedia.org/wiki/Human_gonad
urbit 13y ago
It is an understandable comment. Maybe we'll rethink it. Bad taste is a social construct, but you live in the society you live in... On the other hand, the identity dialogue defaults unwary bros to %lady, which certainly ought to cause a little wailing and gnashing of teeth.

samatman 13y ago

Nock made me suspect Mencius is a Kabbalist. This metal and wood business confirms it. Hoon is still far and away the most WTF part of Urbit from my perspective. Nock: brilliant. Urbit proper: obviously the right thing. Hoon: line noise or poetry? I remain totally undecided. Eagerly awaiting comprehensive documentation of the digraphs.

aaronem 13y ago
From chapter 4: > So if we had to read the above decrement, omitting the spaces (which only a real purist would pronounce), 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.” Kabbalist? This sounds more Holy Roller to me. I plan to spend at least some of the upcoming weekend with Urbit. It should be interesting, to say the least.
samograd 13y ago
My take on hoon is to use[2] the alphabetic names of the line noise operators to create words and use them to make a non-symbolic (if you take alphanumeric characters as non-symbolic) functional, executable conlang[3]. To me it's what Liebniz was looking for[1], but with funny looking words that make no sense to the uninitiated, which use the 'linguistic nodules' that cgyarvin is hoping to utilize, without the symbolic name decoding that using line noise requires (if you use the names in [2] rather than the line noise symbols). I personally think hoon looks like absolute brilliance, but I can't say yet that I've had the pleasure to write anything in it, which is the best thing to take that shiny feeling away by actually trying to use it. But as art, I think it's perfect. [1] http://sunsite.utk.edu/math_archives/.http/hypermail/historia/may99/0211.html http://sunsite.utk.edu/math_archives/.http/hypermail/histori... [2] As follows from http://www.urbit.org/2013/08/22/Chapter-4-syntax.html http://www.urbit.org/2013/08/22/Chapter-4-syntax.html: ace space gal < per ) bar | gar > sel [ bas \ hax # sem ; buc $ hep - ser ] cab _ kel { sig ~ cen % ker } soq ' col : ket ^ tar * com , lus + tec ` doq " pam & tis = dot . pat @ wut ? fas / pel ( zap ! [3] https://en.wikipedia.org/wiki/Constructed_language https://en.wikipedia.org/wiki/Constructed_language

samograd 13y ago

(_Gonadic combinators_? Yes - using our gonad rune, semsig or ;~. If you are a sophisticated professor type and understand monads, gonads may seem real familiar to you. Out here in Urbit world we are just dumb country peasants and all we got is gonads. This is the South Park of system design, or at least it makes me laugh just as much. These guys are great although the software is still a bit fragile.

auggierose 13y ago

I have no idea what any of this means.

auggierose 13y ago
Ok, I just clicked on the link and what I saw there just didn't make any sense to me :-) Still doesn't now, but after reading the comments, I returned to the site and studied it more carefully. Maybe the link should point to chapter 0, not chapter 5, to have any idea about what this is about ... After reading chapter 0 now, I can understand the goal of urbit, and I think it is a great one! But note that you can work on exactly the same goal without leaving PL theory and theorem proving entirely behind you. Check out http://proofpeer.net http://proofpeer.net to see how this might be possible.
- urbit 13y ago
  That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indifferent substrate. But... +1 for an exciting vision of math uber alles.

archgrove 13y ago

I'm presuming this is "in joke" that I'm very much out of. I honestly have no idea what this is about at all, nor can I find any context.

urbit 13y ago
More context from the front page: http://urbit.org http://urbit.org. Previous HN discussion: https://news.ycombinator.com/item?id=6438320 https://news.ycombinator.com/item?id=6438320 This is a perfectly serious type system that infers perfectly serious types all day long. It is moronic, though.
- tsukikage 13y ago
  > This is a perfectly serious type system that infers perfectly serious types all day long ...in a submarine.
  - samatman 13y ago
    Your desktop isn't wood, your folders aren't manila, and your windows aren't glass. Why balk at a submarine? It's made of the usual combination of bits and vivid metaphor.
    - tsukikage 13y ago
      My desktop is most certainly not wood, it's %gold ;) Who's balking? I'm right there under the water. I find myself craving a destroyer, without quite knowing what I'd do with one ;)

andrewcooke 13y ago

anyone got a summary for people with less patience or an apparently broken sense of humour?

urbit 13y ago
Hoon is a very stupid little higher-order type-inference engine that does not use Hindley-Milner, category theory, etc. Higher-order functional programming is so cool it should be accessible to the majority of human beings who unfortunately happen to be bad at math. Also, layering a type system on top of an untyped data model has various practical benefits - eg, your types can be used as validators for untrusted data you got over the network.
- deleted 13y ago
  [deleted]
- samatman 13y ago
  You appear to be saying, among other things, that a noun is of a particular type if it may be passed through a function that parses and validates that, yes, those bits may be treated in that fashion. Is that accurate? There's clearly more to it, as there's at least one conceptual leap between that notion and any kind of inference.
  - urbit 13y ago
    The type, as a set of nouns, is the range (excuse me, "codomain") of a function. So, if we have another function and we call it with a noun of that type, we know the range of the input, we know the code in the function, we can infer the range of the output. It's not terribly rocket scientific.
    - samatman 13y ago
      This explanation falls apart for me because the third time you use the word "function", it can refer to either of the two referents you already introduced. I think you're saying a type is the range of inputs to function1 which succeed by not crashing; given function2 and a noun in the type, we may use function1 to infer the range of values which function2 must accept? Maybe?

tikhonj 13y ago

This might be an interesting project if not for the constant misguided crusading against a PL theory straw man. It's a sort of anti-intellectualism I find particularly galling, but it seems lamentably common in some nooks of the programming world.

freyrs3 13y ago
I find the whole hubris of this article kind of alarming, I'm not sure if the author is doing this out of some form of satire or whether he/she actually think that the "disciple of PL theory is just full of misguided imbeciles who use formal words I don't like". The attacks on TAPL too are seemingly weird, because arguably it's one of most thudingly concrete and down to earth books on types ever written. The whole book is about applications to real world problems and reveling in the fact that one haven't read it seems very asinine.
- urbit 13y ago
  Obviously if you have a door that needs to stay open, a thudingly concrete... never mind. All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right? PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.
  - freyrs3 13y ago
    > Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? Yes I have read TAPL, it's sitting on my desk right now. I'm not even sure what you're trying so say, the fact that a book on type system design doesn't have advice on Java* seems perfectly natural to me. A book on goat husbandry doesn't have advice on Rails development. What are you trying to say? > PL theory is not the theory of programming, any more than TAPL is the doorstop. This is the strawmen that you're arguing against that seems bizarre to many people. PL theory is not so much about the lambda calculus and Hindley-Milner as it is about applying rigor and discipline to the study of programming languages. And yes, sometimes that involves learning the mathematical formalism. * Chapter 19 in TAPL actually does have an implementation of Java's type system.

adultSwim 13y ago

I actually find a lot of arguments he presents compelling. However the general thrust seems to be that programming language should be accessible. Hoon seems to fail that test. I've yet to see how this is better than vanilla ML. I don't see that because Hoon doesn't use standard syntax or terminology. I can't just read some code and a language overview to decide if this is worth (a lot of) my time. I think ML has a fairly steep start-up cost but is definitely understandable by regular people and has real productivity benefits. Hoon is sufficiently obfuscated that it has an incredibly high barrier to even evaluate as a language. I don't think you need to have tons of unintelligible typing rules to make things familiar. By avoiding standard syntax and terminology, it puts an enormous burden on the potential user.

urbit 13y ago
Some UI burdens seem high, some are high. An interesting class of UI problem is the set of things that intuitively look difficult, but actually aren't. Human brains are incredibly good at raw memorization of associations. Hoon has about 100 digraphs, and their internal structure isn't random. How hard is to learn 100 characters of Chinese? Perhaps easier than you think. Nor are there no payoffs. For instance, most languages are very bad at defining large, mostly static hierarchical trees, so when it comes time to write code that generates, say, an HTML page, you reach for a special "template language" DSL. That's not a problem we have in Hoon. Also, most functional languages have a very annoying tendency to crawl off the right side of your screen and disappear, because indentation depth matches functional depth. That's also not a problem we have in Hoon. So... you pay, definitely. But you also receive.
samatman 13y ago
I'd like to address this obliquely with a question to urbit: Is it always the case that the vowels may be compressed away without loss of meaning? It seems to work some/most of the time, but there is a least a %wet and %wut... I think? Though this be method, yet there is madness to it.
- urbit 13y ago
  There's %wet but no ++wet. The name of the character is actually just the name of a parser function for it.

adultSwim 13y ago

By the way, what's with all the hate on Ben Pierce? Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or category theory. Just straight programming and simple proofs. That's a world where previously the few who entered were sucked down a rabbit hole of theory, never to return again.

mritun 13y ago

This is work of pure brilliance!

pekk 13y ago

Perl for type systems?

itsuart 13y ago

First of all, I didn't read linked article. Which is wrong of course. As usual, I'm basing on comments in this thread. So you want to do type system without PL theory of modern age. Awesome! Seriously, interesting experiment. Unless you already have read TaPL in which case I fear you would antagonise ideas described there. However, there is a non-merit, non-technical problem: dismissing PL theorists is sounds like dismissing PL theory (wrong implication, but that is how humans are I believe). And this will put you into JS/PHP/whatever-back-to-the-trees basket and your ideas will be dismissed just because of this wrong association. Which means, that you will distorted results of your experiment. How do you plan to alleviate that? Or I'm wrong somewhere and it is non issue?