4 ms·

Anyone know the judgement rules behind the interesting parts of Pony's type system? I'm about to crack the dissertation to see what's up but would love a concis

Anyone know the judgement rules behind the interesting parts of Pony's type system? I'm about to crack the dissertation to see what's up but would love a concise description. https://www.ponylang.io/media/papers/a_prinicipled_design_of_capabilities_in_pony.pdf https://www.ponylang.io/media/papers/a_prinicipled_design_of...

haskellandchill 6y ago
I took a stab at it, seems everything is indexed by capabilities which makes sense. There is "Equivalence of ephemeral capabilities" for ephemeral indexing outside of iso and turn. There is "Compatible capabilities with ephemeral modifiers" which shows ephemeral indexing does not matter for compatibility. This is extended to types with "Compatible types" then "define the aliasing operator +, to give us the minimum compatible capability when a new alias to an object has been made" with "Aliasing" presenting the cases. There is "Unaliasing" and that's where I'm checking out. Is there a general theory behind these kind of indexed judgement rules with case splitting?
- hntemppony 6y ago
  Basically unaliasing distinguishes the cases: * I have `iso^` because consumed the last reference to an `iso`, so this value can be sent anywhere or renamed * I have `iso` because I've just evaluated a living reference to an `iso` object, so I can access fields and methods (with automatic receiver recovery) but can't move it anywhere Unaliasing with `consume` is what produces `iso^`
hntemppony 6y ago
The interesting parts: Capabilities describe both uniqueness and read-write ability. `iso` is fully unique and hence sendable, `trn` and `val` are write-unique (but `val` is also sendable since it isn't writable). The `tag` capability allows identity/message sending and is fully sendable Recover blocks and automatic receiver recovery allow creation/usage of isolated data if only sendables are used from the external environment. Only sendables can be included in messages. Actors have `ref` access to themselves but `tag` access to other actors.
- haskellandchill 6y ago
  Could dependent types model capabilities? Would never be as ergonomic as Pony, but I'm wondering about expressive power of dependent types compared to indexed judgement rules or linear judgement rules.

haskellandchill 6y ago

I took a stab at it, seems everything is indexed by capabilities which makes sense. There is "Equivalence of ephemeral capabilities" for ephemeral indexing outside of iso and turn. There is "Compatible capabilities with ephemeral modifiers" which shows ephemeral indexing does not matter for compatibility. This is extended to types with "Compatible types" then "define the aliasing operator +, to give us the minimum compatible capability when a new alias to an object has been made" with "Aliasing" presenting the cases. There is "Unaliasing" and that's where I'm checking out. Is there a general theory behind these kind of indexed judgement rules with case splitting?

hntemppony 6y ago
Basically unaliasing distinguishes the cases: * I have `iso^` because consumed the last reference to an `iso`, so this value can be sent anywhere or renamed * I have `iso` because I've just evaluated a living reference to an `iso` object, so I can access fields and methods (with automatic receiver recovery) but can't move it anywhere Unaliasing with `consume` is what produces `iso^`

hntemppony 6y ago

The interesting parts: Capabilities describe both uniqueness and read-write ability. `iso` is fully unique and hence sendable, `trn` and `val` are write-unique (but `val` is also sendable since it isn't writable). The `tag` capability allows identity/message sending and is fully sendable Recover blocks and automatic receiver recovery allow creation/usage of isolated data if only sendables are used from the external environment. Only sendables can be included in messages. Actors have `ref` access to themselves but `tag` access to other actors.

haskellandchill 6y ago
Could dependent types model capabilities? Would never be as ergonomic as Pony, but I'm wondering about expressive power of dependent types compared to indexed judgement rules or linear judgement rules.