Explore ideas about flattened types.

[cristianoc]

Warning: these are exploratory high-level ideas. It would not be surprising to find major holes in them. But at least there's an attempt to go beyond the surface and consider simple semantic models.

Flattened Types

We study the properties of flattened type constructors c<->, i.e. types whose runtime representation has the semantic property c<c<'a>> = c<'a>. Flattened types are common concepts in JavaScript: nullable values (or possibly undefined), and promises.

Two semantic relations between types will be considered. t1 <= t2 means that every JS value which is a runtime representation of type t1 is a value of type t2; and t1 = t2 means that both t1 <= t2 and t2 <= t1.

Equations

We consider a unary type constructor ?<-> that obeys two equations:

1 ??t = ?t

2 t <= ?t

While equation 1 is self-evident, number 2 isn't. Consider that flattened types normally come with operations to "look inside", i.e. take a value of type ?t, and later continue the computation with a value of type t. If one starts with a value of type ??t and looks inside, then the computation expects to continue with a value of type ?t. However a value of type ??t, because of equation 1, also has type ?t, so the computation must be able to continue with type t. And equation 2 is exactly what allows to provide a value of type t to a computation expecting ?t.

We will also use the injection i : t => ?t, the identity function, which exists because of equation 2.

Option Instantiation

The Option Instantiation also has the two equations plus:

• An element e such that e:?t for any t, the empty element.

We define a function caseAnalysis : (?t, s, t=>s) => s in JS as follows:

const caseAnalysis = (o, d, f) => {
    if (o == e) {
        return d
    } else {
        return f(o)
    }
}

This is sufficient to interpret options:

• None is e
• Some(x) is i(x)
• switch e { | None => e1 | Some(x) => e2 } is caseAnalysis(e, e1, x=>e2)

What is left to define is the type constructor ?t for flattened options.
The definition is t | undefined i.e. it takes all the values that t takes plus the value undefined.

It's clear that equations 1 and 2 hold. Plus we can pick e = undefined.

As for caseAnalysis if o : ?t and o == e does not hold, than it must be that o : t. So the function satisfies the required type.

This gives an instance of flattened options that don't require special representation for the nested case. It differs from ordinary options in that Some(None) is the same value as None.

Promise Instantiation

The Promise Instantiation has the two equations plus:

• A function map : (?t, t=>s) => ?s.

With this we can interpret flattened promises:

• FPromise.resolve is i
• FPromise.then_ is map

Before defining the type ?, we use an auxiliary definition for JS promises.
The type Promise<t> of JS promises is defined as the set of values that are JS promises holding values of type t. Each such value v has the property Promise.resolve(v) == v.

Now the type for flattened promises is defined as:

• ?t is t | Promise<t> so it's either a JS value of type t or a JS promise holding a value of type t.

Let's see how this satisfies the required equations.

For equation 1, ??t is ?t | Promise<?t> i.e.
t | Promise<t> | Promise<t | Promise<t>> i.e. t | Promise<t> because JS promises are flattened, i.e. ?t.

For equation 2, clearly t <= t | Promise<t>.

What is left to do is to define map in JS, as follows:

const map = (p, f) => (Promise.resolve(p)).then(f)

To check the type of map, assume p has type t | Promise<t>,
then Promise.resolve(p) has type Promise<t> so it's safe to apply then and obtain the result of type Promise<s> which also has type ?s.

Note that if p is a string promise of type ???string, then f will be passed a string, but that's OK as a string value also has type ?string as well as ??string.

Compared to ordinary JS promise types, ?t obeys property 2, which is what seems to protect it from issues when types are assigned to nested promises.

Async/await requires no special interpretation. For example:

let double: ?t => ?(t, t) = async (x) => {
  let y = await x
  (y, y)
}

compiles to:

async function double(x) {
  var y = await x;
  return [y, y];
}

Now if x has type ?t, i.e. is a JS value of type t | Promise<t>, then there are 2 cases:

• If x has type Promise<t> then await x has type t
• Otherwise, x has type t and is not a promise, so await x is x, which has type t.

[cknitt]

What I didn't understand: Is this ?t = t | Promise<t> just a concept that you are applying in #5709 to make nested promises safe, or could such a type be added to the type system, and could it be used for the return type of the Promise.then callback?

So that it would become possible to do both

p->Js.Promise2.then(x => x + 1)

and

p->Js.Promise2.then(x => Js.Promise2.resolve(x + 1))

like in JS?

[cristianoc]

What I didn't understand: Is this ?t = t | Promise<t> just a concept that you are applying in #5709 to make nested promises safe, or could such a type be added to the type system, and could it be used for the return type of the Promise.then callback?

So that it would become possible to do both

p->Js.Promise2.then(x => x + 1)

and

p->Js.Promise2.then(x => Js.Promise2.resolve(x + 1))

like in JS?

It describes the meaning of the promise type in terms of its runtime representation: when you see promise<int>, it could be a promise, but it could be just an int. The promise type itself as seen by the language does not change: it's still an abstract type.

What would be possible to expose, is that promise<promise<t>> can be simplified to promise<t>, but not sure how much this convenience would be used in practice, and changing the type system requires a compelling reason.

[DZakh]

When you see promise, it could be a promise, but it could be just an int.

I think it's a dangerous way to go because it goes against the way how developers got used to thinking of the promise type. Because it's different from the Js.Promise.t and other compiled languages to JS.

In my opinion, it breaks the reasoning about promise by adding different meanings for it. And Js.Promise2 fixes an edge case, but not the root of the problem. While going in another direction from many userland libraries and against the runtime-free nature of the Js module.

The actual problem is that await doesn't flatten the promise type.

And I think that it's better to leave the flattening to a user, by adding a helper Promise2.flatten instead of changing the runtime and type behavior.

Here's the preceding discussion: #5709 (comment).

[mununki]

The flatten promise in Js reminds me of the linked list:

// Flatten Promise
module FP = {
  type rec t<'a> = Nil('a) | Cons(t<'a>)

  let rec awaitP = (p: t<'a>) =>
    switch p {
    | Nil(a) => a
    | Cons(p) => awaitP(p)
    }
}

let ppp = FP.Cons(FP.Cons(FP.Cons(Nil(1))))

let p = FP.awaitP(ppp)

😉

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions.