4 ms·

For a toy project of mine, I needed a way to encode small programs to send around. I originally wrote a interpreter for the MIPS instruction set, but then I enc

For a toy project of mine, I needed a way to encode small programs to send around. I originally wrote a interpreter for the MIPS instruction set, but then I encountered Urbit's functional machine language, "nock", and switched right over to that. It ended up being a much much simpler interpreter with more compact program encodings and a lot fewer arbitrary-feeling decisions involved. Nock also turns out to be a really straightforward compile target for lisp-like languages. Nock is confusing to approach, but it is really very clever. I would recommend learning it if you are in the mood for a puzzle! Nock: https://github.com/cgyarvin/urbit/blob/master/doc/book/1-nock.markdown https://github.com/cgyarvin/urbit/blob/master/doc/book/1-noc... My project's nock VM: https://github.com/PeterReid/hoplight/tree/master/vm https://github.com/PeterReid/hoplight/tree/master/vm

chc4 10y ago
Neat! Are you compiling Hoon for the programs, or did you make your own language that targets it? How are you handling infinite loops or calling potentially unsandboxed jets? Reading over your code, it looks like you expanded Nock a bit with opcodes for e.g. hashing. instead of having a base stdlib context you are calling against with a jetted gate for it. Any reason? The problem with Nock as an embedded language is that you need a certain critical mass of jets before it's usable, unfortunately. How has that worked out for you? I thought that Nock would be a cool language for this type of stuff, or replacing Bitcoins/Etherums embedded stack languages due to the purely functional, its-just-reduction aspect.
- samatman 10y ago
  This is one of the reasons I included all arithmetic operations in ax: https://github.com/mnemnion/ax/blob/master/ax%20spec.md https://github.com/mnemnion/ax/blob/master/ax%20spec.md Also because once you say 'natural number', the arithmetic operations are already in scope, so to speak.
  - chc4 10y ago
    I get that Nock is half philosophical perfection, so it makes sense to me. All those operations can be trivially defined without any cost, but they muck up the spec (Does your language gzip to 340 bytes? Can I wear it on a t-shirt?). Not that there's anything wrong with defining a language that is usable out of the box, but at the same time muh intellectual purity.
    - samatman 10y ago
      You might have to use the back of a t-shirt. A spec which includes the term 'natural numbers' but not subtraction might even be argued to be incomplete, rather than minimal. Ymmv.
      - chc4 10y ago
        You can synthesize subtraction from recursion and addition. Peano numbers really only have successor, but is still a valid encoding. Really, you aren't wrong. But then how would we be able to advertise how stupid Nock is for those sweet internet points? It can't even do subtraction! Come see, tickets one dollar! Addition is kinda the prime operation that is needed - everything else can be dissolved into it, but without it the jet system doesn't hold up because your language can't really /do/ anything. If you didn't require jets to be transparent to the reduction, you could just have /all/ operations be jets and not even pretend Nock was useful without them.
        pcmoore 10y ago
        Check out https://github.com/tibru/tibru https://github.com/tibru/tibru No primitive arithmetic operations at all, no need for jets but the same time complexity as arithmetic in C just with a higher constant factor.
- PeterReid 10y ago
  I cut out jets entirely. The programs that I anticipate having to execute are mostly simple compositions of retrieving data, storing data, transmitting packets, and cryptographic operations, so being able to do heavy computations did not seem worth the complexity. It is still early days in this project, though, so I might change my mind. Infinite loops are covered by a general cost-tracking system. A computation begins with a certain number of ticks allocated to it, which an agent will use to weigh the CPU/storage space/network usage of what they're executing against the benefit of maintaining a relationship with the agent for whom it is executing. Infinite loops will just run down the tick counter and terminate. I am not compiling Hoon. I have not actually learned it well yet! Since the programs involved are simple, I have mostly just been writing Nock slightly programmatically, like this: https://github.com/PeterReid/hoplight/blob/3971f7c7e45bceed90146a77e91acdab2d876a16/vm/src/eval.rs#L460 https://github.com/PeterReid/hoplight/blob/3971f7c7e45bceed9... But I did write an abomination to make that a little easier. I am programmatically constructing a the AST here, since I have not gotten around to writing a parser. lett(vec![ ("decrement", lambda(vec!["target", "possible_antecedent"], iff( equal(var("target"), increment(var("possible_antecedent"))), var("possible_antecedent"), invoke("decrement", vec![ var("target"), increment(var("possible_antecedent"))])) )) ], invoke("decrement", vec![var("~"), literal_u8(0)] ) ) But I will probably learn Hoon instead. Edit: I thought to add, after reading the sibling comment, that another reason I cut out jets was that basic arithmetic operations were less obviously in scope, because the atoms are byte sequences instead of natural numbers.
chriswarbo 10y ago
> For a toy project of mine, I needed a way to encode small programs to send around. There are a few languages springing up in this space, often as something like "JSON + functions". I hadn't thought of Nock in that way. Some of those I find most interesting at the moment: - Scheme: always nice, although should be limited to a pure subset, maybe without call/cc - annah/morte/dhall: I love the ability to use URLs as identifiers, and using IPFS to prevent mutation. A a less-cluttered syntax like plain s-expressions would be nice; maybe a version for untyped lambda calculus too. - Binary lambda calculus: a very nice representation, suitable for all the same church-encoding tricks as annah/morte/dhall. Wouldn't make sense to be so minimal if URLs are being used as identifiers though. - For something fast or imperative, Forth (maybe Joy), APL, Lua, etc. might be better, although they'd have to be interpreted without arbitrary side-effects.

chc4 10y ago

Neat! Are you compiling Hoon for the programs, or did you make your own language that targets it? How are you handling infinite loops or calling potentially unsandboxed jets? Reading over your code, it looks like you expanded Nock a bit with opcodes for e.g. hashing. instead of having a base stdlib context you are calling against with a jetted gate for it. Any reason? The problem with Nock as an embedded language is that you need a certain critical mass of jets before it's usable, unfortunately. How has that worked out for you? I thought that Nock would be a cool language for this type of stuff, or replacing Bitcoins/Etherums embedded stack languages due to the purely functional, its-just-reduction aspect.

samatman 10y ago
This is one of the reasons I included all arithmetic operations in ax: https://github.com/mnemnion/ax/blob/master/ax%20spec.md https://github.com/mnemnion/ax/blob/master/ax%20spec.md Also because once you say 'natural number', the arithmetic operations are already in scope, so to speak.
- chc4 10y ago
  I get that Nock is half philosophical perfection, so it makes sense to me. All those operations can be trivially defined without any cost, but they muck up the spec (Does your language gzip to 340 bytes? Can I wear it on a t-shirt?). Not that there's anything wrong with defining a language that is usable out of the box, but at the same time muh intellectual purity.
  - samatman 10y ago
    You might have to use the back of a t-shirt. A spec which includes the term 'natural numbers' but not subtraction might even be argued to be incomplete, rather than minimal. Ymmv.
    - chc4 10y ago
      You can synthesize subtraction from recursion and addition. Peano numbers really only have successor, but is still a valid encoding. Really, you aren't wrong. But then how would we be able to advertise how stupid Nock is for those sweet internet points? It can't even do subtraction! Come see, tickets one dollar! Addition is kinda the prime operation that is needed - everything else can be dissolved into it, but without it the jet system doesn't hold up because your language can't really /do/ anything. If you didn't require jets to be transparent to the reduction, you could just have /all/ operations be jets and not even pretend Nock was useful without them.
      - pcmoore 10y ago
        Check out https://github.com/tibru/tibru https://github.com/tibru/tibru No primitive arithmetic operations at all, no need for jets but the same time complexity as arithmetic in C just with a higher constant factor.
PeterReid 10y ago
I cut out jets entirely. The programs that I anticipate having to execute are mostly simple compositions of retrieving data, storing data, transmitting packets, and cryptographic operations, so being able to do heavy computations did not seem worth the complexity. It is still early days in this project, though, so I might change my mind. Infinite loops are covered by a general cost-tracking system. A computation begins with a certain number of ticks allocated to it, which an agent will use to weigh the CPU/storage space/network usage of what they're executing against the benefit of maintaining a relationship with the agent for whom it is executing. Infinite loops will just run down the tick counter and terminate. I am not compiling Hoon. I have not actually learned it well yet! Since the programs involved are simple, I have mostly just been writing Nock slightly programmatically, like this: https://github.com/PeterReid/hoplight/blob/3971f7c7e45bceed90146a77e91acdab2d876a16/vm/src/eval.rs#L460 https://github.com/PeterReid/hoplight/blob/3971f7c7e45bceed9... But I did write an abomination to make that a little easier. I am programmatically constructing a the AST here, since I have not gotten around to writing a parser. lett(vec![ ("decrement", lambda(vec!["target", "possible_antecedent"], iff( equal(var("target"), increment(var("possible_antecedent"))), var("possible_antecedent"), invoke("decrement", vec![ var("target"), increment(var("possible_antecedent"))])) )) ], invoke("decrement", vec![var("~"), literal_u8(0)] ) ) But I will probably learn Hoon instead. Edit: I thought to add, after reading the sibling comment, that another reason I cut out jets was that basic arithmetic operations were less obviously in scope, because the atoms are byte sequences instead of natural numbers.

chriswarbo 10y ago

> For a toy project of mine, I needed a way to encode small programs to send around. There are a few languages springing up in this space, often as something like "JSON + functions". I hadn't thought of Nock in that way. Some of those I find most interesting at the moment: - Scheme: always nice, although should be limited to a pure subset, maybe without call/cc - annah/morte/dhall: I love the ability to use URLs as identifiers, and using IPFS to prevent mutation. A a less-cluttered syntax like plain s-expressions would be nice; maybe a version for untyped lambda calculus too. - Binary lambda calculus: a very nice representation, suitable for all the same church-encoding tricks as annah/morte/dhall. Wouldn't make sense to be so minimal if URLs are being used as identifiers though. - For something fast or imperative, Forth (maybe Joy), APL, Lua, etc. might be better, although they'd have to be interpreted without arbitrary side-effects.