15 ms·

> not all of the last 30 odd years of systems and programming research was pointless. Indeed, which is why it's a shame our primary server OSes (Unix-likes) ca

by pcmonk 9y ago

> not all of the last 30 odd years of systems and programming research was pointless. Indeed, which is why it's a shame our primary server OSes (Unix-likes) can't incorporate them. Urbit can. As for what are the approaches different, there have been many words spilled over that, but here's a few examples to wit, most of which exist in one or two other systems, but aren't widely used: - All events are transactions, down to the VM level. There's no concept of an event that left garbage around because power was cut or the machine was rebooted. You can always crash an event, making it as if it never happened. - Single-level store. Never worry about ORM because your in-memory state never goes away (because all events are transactions). - Persistent connections with exactly-once messaging. Disconnection is just seen as long latency. - Strict, purely functional language with a strong type system but no Hindley-Milner (so you don't need category theory). - Sane indentation for a functional language, known as "backstep". - The file system is a typed revision control system, which allows intelligent diffs on types other than plain text. Most, if not all, of these, have been described in research, but nobody's bothered to build a system with them.

Munksgaard 9y ago
I'm curious: What's the advantage of ditching Hindley-Milner?
- Chattered 9y ago
  I want to give urbit a try. I have a planet, but last time I fired it up the latency was so bad that I wasn't having fun. I'll try again sometime. I can even get behind runes, and I set up abbreviations in Emacs to learn their names. And generally, I like the philosophy of language where short, one syllable, old/middle English words are used in place of the less familiar Latin/Greek derived words. I don't have a problem with revising our existing vocabulary in this way. But the attitude to type theory strikes me as anti intellectual, precisely because we get nonsense claims about Hindley Milner requiring category theory. This sort of misinformation does no good for anyone.
- vmchale 9y ago
  None whatsoever. Hindley-Milner is in fact used widely in language design because of its relatively good error messages (as well as ease of implementation). Also it really doesn't have much to do with category theory.
mrkgnao 9y ago
Rust uses Hindley-Milner type inference. OCaml uses Hindley-Milner. Swift apparently uses a variant of the system with more features. None of these make use of monads or anything rooted in category theory. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy... HM is a type system that also gives you an algorithm to infer types without having to do the "List<Integer> foo = new ArrayList<Integer>()" dance from languages without type inference. That's it. It has nothing to do with category theory.
- steveklabnik 9y ago
  (Rust doesn't use Hindley-Milner, though the plan is to try to move closer to it in the future)
  - mrkgnao 9y ago
    Oh, thanks for the correction. It would appear that my knowledge is out of date: did Rust use something closer to H-M in the past? (Going off of https://github.com/rust-lang/rust/pull/15955 https://github.com/rust-lang/rust/pull/15955 here.)
    - steveklabnik 9y ago
      For more, see here: https://www.reddit.com/r/rust/comments/6fs5q9/language_servers_and_ides/dikywtc/ https://www.reddit.com/r/rust/comments/6fs5q9/language_serve... see aturon's reply about that PR/blog post. Rust has done almost everything in the past; I wouldn't be surprised if somewhere back in there it was actually HM. :)
- jolux 9y ago
  Arguably optionals are monadic.
  - mrkgnao 9y ago
    Optionals are also "applicative", but Haskellers used them for a long time before applicative functors became popular. A concept can support a certain way of thinking about it without everyone needing to think that way :)
vmchale 9y ago
>Sane indentation for a functional language, known as "backstep" This is A) not an impressive problem to solve, and B) not actually a problem in Haskell or Elm.
occultist_throw 9y ago
> Persistent connections with exactly-once messaging. Disconnection is just seen as long latency. Bullshit. https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf Unless you and Yarvin really think there's a valid answer to the 2 Generals problem... Im sure there's a Fields medal in there if you do. "Every major message queue in existence which provides any guarantees will market itself as at-least-once delivery. If it claims exactly-once, it’s because they are lying to your face in hopes that you will buy it or they themselves do not understand distributed systems. Either way, it’s not a good indicator." ~ http://bravenewgeek.com/you-cannot-have-exactly-once-delivery/ http://bravenewgeek.com/you-cannot-have-exactly-once-deliver...
- rhencke 9y ago
  Urbit claims, like you, exactly-once messaging is impossible: https://news.ycombinator.com/item?id=14666015 https://news.ycombinator.com/item?id=14666015 But that doesn't mean we can't provide systems where, for all practical purposes, it is a guarantee. Another way to think about it: SHA1 cannot provide a unique hash for every possible set of content - there are overlaps. This is the pigeonhole principle. Yet, we have entire systems designed around assuming SHA1 is and will always be a unique hash for a piece of content (Git), and, for all practical purposes, it is a guarantee good enough to work despite that.
  - occultist_throw 9y ago
    >Urbit claims, like you, exactly-once messaging is impossible: https://news.ycombinator.com/item?id=14666015 https://news.ycombinator.com/item?id=14666015 >But that doesn't mean we can't provide systems where, for all practical purposes, it is a guarantee. Nuh huh. Dont you play wordgames with me. Exactly-once messaging is PROVEN impossible. And I, unlike the rest of you Urbiters, actually use standard terminology when understanding the last of 60 years of CS. > [Blablabla unrelated blather] Your point?
    - rhencke 9y ago
      From all reference I have read, the phrase "exactly-once messaging" does not have a strict technical definition. Neither of your links define or use the exact term "exactly-once messaging". If you can point me to a definition of this specific phrase's standard terminology, I would be grateful. But, I cannot find one. I don't understand why you address me with such a hostile tone. What have I done to deserve this? You accuse me of playing word games, but this is not my intent. I am just trying to have a conversation about the technical aspects of a system.

by pcmonk 9y ago

Munksgaard 9y ago

I'm curious: What's the advantage of ditching Hindley-Milner?

Chattered 9y ago
I want to give urbit a try. I have a planet, but last time I fired it up the latency was so bad that I wasn't having fun. I'll try again sometime. I can even get behind runes, and I set up abbreviations in Emacs to learn their names. And generally, I like the philosophy of language where short, one syllable, old/middle English words are used in place of the less familiar Latin/Greek derived words. I don't have a problem with revising our existing vocabulary in this way. But the attitude to type theory strikes me as anti intellectual, precisely because we get nonsense claims about Hindley Milner requiring category theory. This sort of misinformation does no good for anyone.
vmchale 9y ago
None whatsoever. Hindley-Milner is in fact used widely in language design because of its relatively good error messages (as well as ease of implementation). Also it really doesn't have much to do with category theory.

mrkgnao 9y ago

Rust uses Hindley-Milner type inference. OCaml uses Hindley-Milner. Swift apparently uses a variant of the system with more features. None of these make use of monads or anything rooted in category theory. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy... HM is a type system that also gives you an algorithm to infer types without having to do the "List<Integer> foo = new ArrayList<Integer>()" dance from languages without type inference. That's it. It has nothing to do with category theory.

steveklabnik 9y ago
(Rust doesn't use Hindley-Milner, though the plan is to try to move closer to it in the future)
- mrkgnao 9y ago
  Oh, thanks for the correction. It would appear that my knowledge is out of date: did Rust use something closer to H-M in the past? (Going off of https://github.com/rust-lang/rust/pull/15955 https://github.com/rust-lang/rust/pull/15955 here.)
  - steveklabnik 9y ago
    For more, see here: https://www.reddit.com/r/rust/comments/6fs5q9/language_servers_and_ides/dikywtc/ https://www.reddit.com/r/rust/comments/6fs5q9/language_serve... see aturon's reply about that PR/blog post. Rust has done almost everything in the past; I wouldn't be surprised if somewhere back in there it was actually HM. :)
jolux 9y ago
Arguably optionals are monadic.
- mrkgnao 9y ago
  Optionals are also "applicative", but Haskellers used them for a long time before applicative functors became popular. A concept can support a certain way of thinking about it without everyone needing to think that way :)

vmchale 9y ago

>Sane indentation for a functional language, known as "backstep" This is A) not an impressive problem to solve, and B) not actually a problem in Haskell or Elm.

occultist_throw 9y ago

> Persistent connections with exactly-once messaging. Disconnection is just seen as long latency. Bullshit. https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf Unless you and Yarvin really think there's a valid answer to the 2 Generals problem... Im sure there's a Fields medal in there if you do. "Every major message queue in existence which provides any guarantees will market itself as at-least-once delivery. If it claims exactly-once, it’s because they are lying to your face in hopes that you will buy it or they themselves do not understand distributed systems. Either way, it’s not a good indicator." ~ http://bravenewgeek.com/you-cannot-have-exactly-once-delivery/ http://bravenewgeek.com/you-cannot-have-exactly-once-deliver...

rhencke 9y ago
Urbit claims, like you, exactly-once messaging is impossible: https://news.ycombinator.com/item?id=14666015 https://news.ycombinator.com/item?id=14666015 But that doesn't mean we can't provide systems where, for all practical purposes, it is a guarantee. Another way to think about it: SHA1 cannot provide a unique hash for every possible set of content - there are overlaps. This is the pigeonhole principle. Yet, we have entire systems designed around assuming SHA1 is and will always be a unique hash for a piece of content (Git), and, for all practical purposes, it is a guarantee good enough to work despite that.
- occultist_throw 9y ago
  >Urbit claims, like you, exactly-once messaging is impossible: https://news.ycombinator.com/item?id=14666015 https://news.ycombinator.com/item?id=14666015 >But that doesn't mean we can't provide systems where, for all practical purposes, it is a guarantee. Nuh huh. Dont you play wordgames with me. Exactly-once messaging is PROVEN impossible. And I, unlike the rest of you Urbiters, actually use standard terminology when understanding the last of 60 years of CS. > [Blablabla unrelated blather] Your point?
  - rhencke 9y ago
    From all reference I have read, the phrase "exactly-once messaging" does not have a strict technical definition. Neither of your links define or use the exact term "exactly-once messaging". If you can point me to a definition of this specific phrase's standard terminology, I would be grateful. But, I cannot find one. I don't understand why you address me with such a hostile tone. What have I done to deserve this? You accuse me of playing word games, but this is not my intent. I am just trying to have a conversation about the technical aspects of a system.