Question shortcut - > Jump to a thread.
| Table of Contents |
|---|
I had understood that registers, memory, local storage, network protocols, and other per-node resources would each have separate namespaces. Will this be accomplished by adding extra formula constructors (e.g. 'const' in C) in the same way that we add modalities and collection constructors?
→ Lucius Meredith: Short answer is 'Yes' - these are different built in channel types. There will be grammar for specifying built in channel types beyond merely the term constructors and collection monad. There is a very early version of this in the leithaus github repository. I am using Nominal as a generic class for objects that act as channels. Why have channels for local resources such as storage and network? → Cost and reliability is different. A contract could be blocked (dependent) on storage or network channels. It's important to identify these dependencies at the namespace type level. The namespaces contribute in unique ways for cost analysis.
→ Namespace is a storage tree - this is the abstraction. I/O events get packaged into events within a namespace as a storage tree. But since we have the information at the point of I/O event, we can percolate that information up. Then, at the type level - I can declare a channel as working with events from memory only. So if you receive events up in the storage tree from elsewhere, you can identify this as a bug.
My understanding of namespaces is limited and theoretical. I think it's true to say that the communication/transaction type underlying a particular channel could separate that channel type into its own namespace (i.e., tcp socket vs memory vs ...). In this case, it seems clear that names for channels could be syntactically distinct, allowing up-front classification. For example, the form of a name in the TCP socket namespace will look distinct from a namespace for some other resource.
Will elements of different namespaces expressing differently typed channels (memory vs network, for example) have different structure?
-→ Michael Stay (Unlicensed): I asked Greg about this at the last dev standup; he said that there would probably be type modifiers for doing that. So while "&⊤" is the "any name" namespace, we may see namespaces like "http &⊤" that means "any name referring to a resource on the web".
Ignoring different channel types (or multi-blockchain interoperability, like rchain ↔ ethereum), how are namespaces delineated? For example, if I wish to run the same contract "in two different namespaces", as opposed to running the contract twice in the same namespace but with different input values, can I do that?
→ Michael Stay (Unlicensed): >How are namespaces delineated
Greg's original idea for namespaces had to do with quoted formulae, where a formula is an expression that denotes a set of processes. However, in the last dev meeting, he said that we can adjoin arbitrary grammars to the notion of namespace so that, for instance, we could use URLs like `https://rchain.coop/members/*` to denote a namespace.
→ Michael Stay (Unlicensed): >if I wish to run the same contract "in two different namespaces", as opposed to running the contract twice in the same namespace but with different input values, can I do that?
Yes. Since deploying a contract involves selecting a set of names to give to the contract as arguments, running the contract in two different namespaces is simply choosing names from two different namespaces. Running it twice in the same namespace can have different meanings depending on which names you give it; you can give the two instances disjoint names so that there are two copies running in an overarching namespace, or you can invoke it twice with the exact same names, creating, for example, two servers listening for incoming messages at the same address.
Nash Foster: This answer doesn't seem quite right to me. I think it has to do with the "adjoining arbitrary grammars" thing you mentioned in the last answer. I am having a hard time getting my head around this, but if the inputs are given by the quoted term, you can't run the same program twice with different inputs without changing the quoted term, in which case it's "in a different namespace."
Michael Stay (Unlicensed): Namespaces should be thought of like circles on a Venn diagram. Given two circles, they may be disjoint, one may contain the other, or they may intersect without one containing the other. Names themselves are points on the plane.
You can pick the same points twice, or pick different points in the same circle, or pick points in entirely disjoint circles.
Nash Foster: I understand you can pick the same points twice, but then it results in the same set (namespace). The question Chris is asking is "can I run the same program twice with the same inputs" and the answer is "no, that's just one program because the inputs are the same." It may be trivially fixable by introducing a parameter whose value is just an arbitrary "contract" identifier, which you are allowed to vary any way you like. But, then it isn't "the same" inputs, exactly. This probably feels like fussing about details, but in distributed cloud computing the implementation details here matter ALOT. Because the same program usually runs on different machines (i.e. sharding) and then the "sameness" of two programs is a critical property in allowing for elegant failover and scale-out designs.
Here's a simple contract:
contract sendX(y) = y!<*x>
Now I deploy the contract once using the name z. It'll send x once on z. Now I deploy it again using the name z. It'll send x again on z. Sending x twice on z is different than sending it once on z. So you can deploy the contract twice using the same name and get a fundamentally different effect.
The name z may be part of a namespace Z that also contains the name z'. Deploying the contract using the name z' is still deploying it in the Z namespace.
Are namespaces declared or reserved or carved out somehow at some point?
→ Michael Stay (Unlicensed): > namespaces declared
We'll probably want to allow the ability to define local grammars for namespaces, but I haven't thought about how this would work. At worst this is something we can check using developer tools, but I'd like a more principled approach to declaring namespaces.
What are the allowable types for channels? Can a channel accept other channels? Can one create a contract that exposes (and accepts values along) a channel of type channel of any type, a type like
Channel[Channel[Any]]?
→ Michael Stay (Unlicensed): >allowable types for channels
In rho calculus, the only kind of thing you can send is a process P, which shows up on the other side as a name &P. You can constrain the shape and behavior of the process you're expecting with a formula.
→ Michael Stay (Unlicensed): >a channel accept other channels?
Suppose I have a name x on which a process is listening
`for (z ← x).P`
and I have a name y that I want to make available to the continuation P of that process. I'd say
`x!<*y>`
and then when the process received the message, it would bind z to y in P.
→ Michael Stay (Unlicensed): >any type
yes
Can a name be constructed programmatically by a contract and then used by that contract?
→ Michael Stay (Unlicensed): Yes
There is talk of a special system namespace (or several of them). What names are in the system namespace?
One possible answer is to have `system` be a namespace modifier, and then the system namespace would be `system &⊤`.
REEEEEEEEEEEEEEEEE.
"I need a namespace modifier for system."
vs.
"I can adjoin arbitrary grammars."
This stuff feels to "clever" by half.
There's still a lot of work to be done in figuring out what namespaces we need beyond the fundamental ones from quoted rho calculus terms, and what kinds of naming we want to allow applications to do.
What namespaces do we need, how to construct them and whether there's some way to declare a schema for namespaces so that we can statically check them, etc. Here are some things that we should talk about:
system namespace
comms namespaces
namespaces for intra-vm comms
namespaces for inter-vm intra-node comms
namespaces for inter-node comms
namespaces for the blockchain
namespaces for other protocols like http
→ Lucius Meredith (Via Developer standup meeting on 09.13.17)
Namespaces are a collection of channels. N=P(N) - P is the theory of process calculi that depend on N. Rho Calc is the smallest solution to this equation.
G is an index - there is a bunch of G's.
N[G] = P(N[G]) + ∑G → G = URI + UnicodeStrings+ integers
Are we going to use multiple copies of P(N[G]) for the system namespaces or other namespaces? For the layman's instructions we are not just making quoted processes be the set of names. There is a Row 0 theory (N=P(N) that says that once you show Row 0 works out, you can expand row it to include these other names. If we do not upset the kernel theory then we know we are safe with respect to these other names but you also know, -
N[G] = P(N[G]) + ∑G
Because this is a sum, you can do type level analysis on the names themselves and determine when you have a name at the type level (statically) when the name is a quoted process or something else - so you can at the type level determine if the de-reference makes sense or not. Then we can say that it is a 'type error to dereference this type of URI"
There is a class of high performance system names that are integers. All other names are URI's + Unicodes → URI encoded names, especially public names. This gives us coverage for all the web technologies out there today.
- Integer portion →class of fast, internal system names.
- Unicode → dereferencing portion
- URI → Customer facing portion of names.
URI scheme that gives us a tree versus an overlapping scheme which is easier for us to think about. Ex: memory://path, net://path. Michael Stay (Unlicensed) - How does the collection Monad work with anything that isn't a process. Greg - we can do a brute force thing, and just run Ladl over the unicode structure, or we could use XPath.
People will not generate namespaces in the Integer portion. They will only generate URI + Unicode string names.
Michael Stay (Unlicensed): Are we going to allow any local namespacing? Ex: an app wants to use a specific format for urls - if they don't - throw a compile error? Lucius Meredith: For Mercury this could be a tool, and later this becomes part of the system.
What it means to dereference a name that isn't a quoted process
storage type modifiers like "register" or "memory" etc.
how URLs or prolog terms get involved
→ Answer?
Elsewhere in CS, namespaces are types that have a "resolve" operation that converts a name into an object of a some type. The type of name you can put into resolve() and the type of object you get out are specified by the namespace. E.g., DNS name "resolves" to an object of type IP address (bare data), but a name of type <proto, dns, port> name "resolves" to a socket connection (not bare data). Though, I should note the "resolve" operation on <proto, dns, port> is actually called "connect" and not "resolve," it's more or less isomorphic. It's not obvious to me how "resolve" works in our namespaces.
→ Lucius Meredith - That is under the assumption that resolve gets you to a resource. DNS gets you to a name. If we are passing actual names, there is no need to use names. Inside the VM we will handle resolving names to an internal resource.
There's not an explicit hierarchy in play here, but hierarchies are easier to teach, easier to work with, and easier to verify correctness. Even Greg talks about namespaces as looking "like URLs" so it's clear everyone is already thinking in terms of a hierarchy. The question is why aren't we being explicit and just giving a global hierarchy to start with? Does it limit us in some way?
→ Answer?
I've been thinking about cross-namespace transactions. Imagine a scenario where there are three namespaces A, B, and C. A contains an instance of a token contract for the token REV. B and C contain their own version of REV, call them REV-B and REV-C. All balances are 0 except P_A, which has a 1000 REV. Assume I want to transfer 100 REV from P_A in namespace A to address P_B in namespace B. We can do this transfer T as follows (based on https://github.com/ethereum/wiki/wiki/Sharding-FAQ#how-can-we-facilitate-cross-shard-communication): 1. I create a transaction to namespace A that does the following: decrement P_A balance by 100 and create a receipt on namespace A saying it will send 100 REV to P_B. 2. I create a second transaction to namespace B that does the following: provide a link to the receipt on namespace A and using it as proof, increment P_B by 100 REV-B. Now I want to transfer 100 REV from P_B to P_B2 in namespace B. As this is intra-namespace, we can simply make a call to the token contract in namespace B. Finally, we want to transfer 100 REV from P_B2 in namespace B to P_C in namespace C. In Ethereum's proposed sharding model, we can repeat a similar process to T as the validators are randomly sampled for each shard. In Rchain's model, validators choose the namespaces they are interested in, and thus repeating T would imply that namespace C's validators trust namespace B's.
Assume namespace B's validators are malicious: they could issue a transaction saying that P_B sends 100 REV-B to P_C (since P_B has 0 after transfering everything to P_B2). How will namespace B's validators be punished and by whom? Namespace A's and C's validators cannot punish B's as it is unaware that the intra-namespace transfer occured. Only after more than 100 REV-B leaves namespace B can B's validators called out. If namespace B's validators gradually transfered a total of 101 REV-B across all other namespaces, all other namespaces will have to collaborate to detect that more REV-B left namespace B than went in. This implies at least a couple validators will have to look at all namespaces for a global token. It also implies that we might have to rewrite the token contract to support namespaces?
→ Answer?