From 94fdd5ec1d798080de673b10a9b0586d1e0d18f6 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 6 Jun 2019 16:07:53 +0200
Subject: [PATCH] Add a bottom type to IDL (#476)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 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
---
 design/IDL.md | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/design/IDL.md b/design/IDL.md
index f53c9e91a5f..8b876f01337 100644
--- a/design/IDL.md
+++ b/design/IDL.md
@@ -77,6 +77,7 @@ This is a summary of the grammar proposed:
   | text
   | null
   | reserved
+  | empty
 
 <constype>  ::=
   | opt <datatype>
@@ -258,6 +259,12 @@ The type `reserved` is a type with unknown content that ought to be ignored. Its
 ```
 **Note:** This type has a similar role as *reserved fields* in proto buffers.
 
+#### Empty
+
+The type `empty` is the type of values that are not present. Its purpose is to mark variants that are not actually there, or -- as argument types of function reference -- indicate that they will not be called.
+```
+<primtype> ::= ... | empty
+```
 
 ### Constructed Data
 
@@ -533,11 +540,15 @@ An exception are integers, which can be specialised to natural numbers:
 nat <: int
 ```
 
-An additional rule applies to `unavailable`, which makes it a top type, i.e., a supertype of every type.
+Additional rules apply to `empty` and `reserved`, which makes these a bottom resp. top type:
 ```
 
 -------------------------
-<datatype> <: unavailable
+<datatype> <: reserved
+
+
+--------------------
+empty <: <datatype>
 ```
 
 #### Options and Vectors
@@ -723,12 +734,13 @@ T(int<N>)   = sleb128(-9 - log2(N/8))
 T(float<N>) = sleb128(-13 - log2(N/32))
 T(text)     = sleb128(-15)
 T(reserved) = sleb128(-16)
+T(empty)    = sleb128(-17)
 
 T : <constype> -> i8*
-T(opt <datatype>) = sleb128(-17) I(<datatype>)
-T(vec <datatype>) = sleb128(-18) I(<datatype>)
-T(record {<fieldtype>^N}) = sleb128(-19) T*(<fieldtype>^N)
-T(variant {<fieldtype>^N}) = sleb128(-20) T*(<fieldtype>^N)
+T(opt <datatype>) = sleb128(-18) I(<datatype>)
+T(vec <datatype>) = sleb128(-19) I(<datatype>)
+T(record {<fieldtype>^N}) = sleb128(-20) T*(<fieldtype>^N)
+T(variant {<fieldtype>^N}) = sleb128(-21) T*(<fieldtype>^N)
 
 T : <fieldtype> -> i8*
 T(<nat>:<datatype>) = leb128(<nat>) I(<datatype>)
@@ -788,6 +800,7 @@ M(b : bool)     = i8(if b then 1 else 0)
 M(t : text)     = leb128(|utf8(t)|) i8*(utf8(t))
 M(_ : null)     = .
 M(_ : reserved) = .
+// NB: M(_ : empty) will never be called
 
 M : <val> -> <constype> -> i8*
 M(null : opt <datatype>) = i8(0)