Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add a bottom type to IDL the need for a bottom type follows from: 1. We have `None` in ActorScript. 2. We want to use it in the IDL (@matthewhammer uses a generic `Result<t1,t2>` type, and if there cannot be an error, puts `None` in `t2`). So `None ∈ dom e`. 3. `None <: t` for all `t` in ActorScript 4. `∀ t1 t2 : dom(e), t1 <: t2 ⟹ e(t1) <: e(t2)` as per #465 This PR proposes adding a bottom type (called `absent`, but other names like `bottom` are fine too). But there are alternatives: * The ADL-AS spec currently has `e(None) = variant {}`. This has the right semantics as an empty set of values, but lacks the right subtyping relation in the IDL subtyping. We could fix the latter, i.e. add an ad-hoc rule `variant {} <: t` and would not have to extend the grammer of the IDL spec. I actually like that. * We define `e` to normalize types with `None` first, with rewrite rules like ``` (None, t) = None shared { n:None, … } = None variant { n:None, … } = variant { … } ? None = null [None] = () None -> t = unavailable t -> None = None // fishy, the function could just be not returning, // but still do something useful ``` with such rules I assume we can completely remove `None` from the actor signature (unless the whole actor becomes `None`). But this might be surprising to the user and cause problems if we add parametric type definitions at some point, such as ``` type Result<t1,t2> = { #ok : t1; #fail : t2 } ``` * s/absent/empty
- Loading branch information