Add a bottom type to IDL

[nomeata]

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 IDL-AS mapping spec #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 }
  

[rossberg]

I understand reason 4, but I'm puzzled about reason 3. @matthewhammer, what's the point of using Result<T, None> instead of just T?

Not sure absent is the best choice, since absent record fields actually have top type, so that's gonna be confusing. The proper name would of course be void, but I'm sure too many folks with C-induced brain damage would get confused. Another common name is empty.

[nomeata]

I understand reason 4, but I'm puzzled about reason 3.

You mean you are puzzled about 2, right?

@matthewhammer, what's the point of using Result<T, None> instead of just T?

The point, I think, is that all functions return in a Result<t1,t2> and thus can uniformly use some combinators:
https://github.com/dfinity-lab/actorscript/blob/fc8bab1d4f9519179788036d2be09ab6eaf858ef/stdlib/examples/produce-exchange/serverActor.as#L138-L144

If we can decide that we don’t need 2, then we can simply not have None ∈ dom(e); works for me as well.

[rossberg]

Hm, I don't see any interesting combinators being used in the code, not even bind. Wouldn't it be the JS frontend code that would have to define and use such combinators on its end? That seems rather unlikely. What would even be the use case? @matthewhammer

[nomeata]

But even disregarding the actual case of produce exchange, do we want to support something like

import T "external-type-definition.as"
actor {
  foo (x : T.type<Int, Nat, None>) = …
}

where the developer is working with some library-provided parametric type T.type that is designed to be parametrized by various types, including None to optionally rule out certain shapes. Since the type is library-provided, the developer cannot (conveniently) just change the type definition.

It’s a bit of an odd case, but not completely unrealistic.

Any other arguments in favor or against including a bottom type?

[rossberg]

I don't have a strong opinion, my only concern is that most languages do not have anything obvious to map it to, which means that we may be simplifying the life for AS for the price of making everybody else's harder. Thoughts?

[nomeata]

Don't most seriously typed languages have an empty type of some sort?

Also, we do have an empty type already in the IDL (variant {}), so it doesn't really change anything with regard to language mapping. We could have empty as a short hand for variant {} (+ the extra subtyping rules).

For untyped languages like JS, it doesn’t really matter, because we never encounter values of type empty, so we can do this:
https://github.com/dfinity-lab/dev/blob/3f88436f80350340a946e45b4ad16d4c160179bb/experimental/js-dfinity-client/src/IDL.js#L81-L94

I don’t feel strongly either, but we have to either

1. Add empty, or
2. don't change the grammar of types, but have variant {} <: t, or
3. Remove None from e, and rewrite the produce exchange.

(I am leaning towards 2: Doesn’t affect other languages, doesn’t complicate the grammar, but still allows AS developers to use None when they want to.)

[rossberg]

Don't most seriously typed languages have an empty type of some sort?

Not so sure. In fact, I can't think of any outside the wider FP camp (to which I count Scala). More importantly, an empty type is not the same as a bottom type.

On the other hand, other langs don't have variants either, which I suppose is similar to your point.

Don't change the grammar of types, but have variant {} <: t

For the record, that would be far too hacky for my taste. Empty variant =/= bottom, empty record =/= top. Type isomorphism is not equivalence -- until we have an IDL based on Homotopy Type Theory.