promised-type-relationships.md

High-Order Type Relationships for promised T

Definitions

1. Definition - A type T is promise-Like iff T has a callable then method that accepts a function as its first argument.

2. Definition - The fulfillment type of T is the type V in T.then((value: V) ⇒> {}).

3. Definition - The promised type of T (nee. promised T) is the promised type of the fulfillment type of T iff T is promise-like; otherwise, T.

4. Definition - The constraint type C is the base constraint of T, such that T <: C.

Theorem

• Given - There exists types S₁ and T₁ such that S₁ <: T₁.
• Given - There exists a type T₂ such that T₂ <: T₁ and ¬(T₁ <: T₂).
• Given - There exists a type S₂ such that S₂ <: S₁ and ¬(S₁ <: S₂).

1. Lemma - If S <: T, then promised S <: promised T.

   1. Proof - If S := S₁ and T := T₁, we have:

      S <: T    ⇒  promised S <: promised T
      S₁ <: T₁  ⇒  promised S₁ <: promised T₁                     (by instantiation)
      S₁ <: T₁  ⇒  S₁ <: T₁                                       (by Definition 3)
      

   2. Proof - If S := Promise<S₁> and T := Promise<T₁>, we have:

      S <: T    ⇒  promised Promise<S> <: promised Promise<T>
      S₁ <: T₁  ⇒  promised Promise<S₁> <: promised Promise<T₁>   (by instantiation)
      S₁ <: T₁  ⇒  S₁ <: T₁                                       (by Definition 3)
      

2. Lemma - If S <: promised C where C is the constraint type of T, then S <: promised T.

   1. Proof - If S := S₁, C := T₁, and T := T₂, we have:

      S <: promised C    ⇒  S <: promised T
      S₁ <: promised T₁  ⇒  S₁ <: promised T₂                       (by instantiation)
      S₁ <: T₁           ⇒  S₁ <: T₂                                (by Definition 3)
      

      • This is a contradiction as ¬(T₁ <: T₂), therefore we cannot prove that S₁ <: T₂.

   2. Proof - If S := S₁, C := Promise<T₁>, and T := Promise<T₂>, we have:

      S <: promised C             ⇒  S <: promised T
      S₁ <: promised Promise<T₁>  ⇒  S₁ <: promised Promise<T₂>     (by instantiation)
      S₁ <: T₁                    ⇒  S₁ <: T₂                       (by Definition 3)
      

      • This is a contradiction as ¬(T₁ <: T₂), therefore we cannot prove that S₁ <: T₂.

3. Lemma - If promised C <: T where C is the constraint type of S, then promised S <: T.

   1. Proof - If C := S₁, S := S₂, and T := T₁, we have:

      promised C <: T    ⇒  promised S <: T
      promised S₁ <: T₁  ⇒  promised S₂ <: T₁                     (by instantiation)
      S₁ <: T₁           ⇒  S₂ <: T₁                              (by Definition 3)
      S₁ <: T₁           ⇒  S₁ <: T₁                              (by transitive rule)
      

   2. Proof - If C := Promise<S₁>, S := Promise<S₂>, and T := T₁, we have:

      promised C <: T             ⇒  promised S <: T
      promised Promise<S₁> <: T₁  ⇒  promised Promise<S₂> <: T₁   (by instantiation)
      S₁ <: T₁                    ⇒  S₂ <: T₁                     (by Definition 3)
      S₁ <: T₁                    ⇒  S₁ <: T₁                     (by transitive rule)
      

After exploring this further, it seems that Lemma 2 is a fallacy.