Modeling Javascript the Weird Parts with Boolean Unification

JS.flix

/*
This is a showcase on how boolean unification can be used to type check the weird parts of Javascript.
*/

/*
Each boolean paramater is a flag for a possible value for a Javascript builtin
For example:
    `Value [false, true, false, false, false, false false, false]` must be a string
    `Value [false, true, true, false, false, false false, true]` must be a string, a number, or null
*/

enum Value
[
    _object : Bool,
    _string : Bool,
    _number : Bool,
    _bigint : Bool,
    _boolean : Bool,
    _undefined : Bool,
    _symbol : Bool,
    _null : Bool
]
/*
Flix doesn't have GADTs so unfortunately there isn't a type safe representation.
Since type checking is the primary concern here, the definition is left void.
*/
{}

// The types of objects, strings, numbers, ...

def object(): Value[true, b2, b3, b4, b5, b6, b7, b8] = ???

def string(): Value[b1, true, b3, b4, b5, b6, b7, b8] = ???

def number(): Value[b1, b2, true, b4, b5, b6, b7, b8] = ???

def bigint(): Value[b1, b2, b3, true, b5, b6, b7, b8] = ???

def boolean(): Value[b1, b2, b3, b4, true, b6, b7, b8] = ???

def undefined(): Value[b1, b2, b3, b4, true, b6, b7, b8] = ???

def symbol(): Value[b1, b2, b3, b4, b5, b6, true, b8] = ???

def null_(): Value[b1, b2, b3, b4, b5, b6, b7, true] = ???

/*
Javascript Addition table
```
| e + e'    | object | string | number | bigint | boolean | undefined | symbol | null   |
| -         | -      | -      | -      | -      | -       | -         | -      | -      |
| object    | string | string | string | string | string  | string    | _      | string |
| string    | string | string | string | string | string  | string    | _      | string |
| number    | string | string | number | _      | number  | number    | _      | number |
| bigint    | string | string | _      | bigint | _       | _         | _      | _      |
| boolean   | string | string | number | _      | number  | number    | _      | number |
| undefined | string | string | number | _      | number  | number    | _      | number |
| symbol    | _      | _      | _      | _      | _       | _         | _      | _      |
| null      | string | string | number | _      | number  | number    | _      | number |
```
*/

def add
    (
        _left : Value [ b1, b2, b3, b4, b5, b6, false, b8],
        _right : Value [ b9, b10, b11, b12, b13, b14, false, b16 ]
    ) : Value [
        // add never returns object
        false,
        // lots of things can return strings
            b1 and b9 or
            b1 and b10 or
            b1 and b11 or
            b1 and b12 or
            b1 and b13 or
            b1 and b14 or
            b1 and b16 or

            b2 and b9 or
            b2 and b10 or
            b2 and b11 or
            b2 and b12 or
            b2 and b13 or
            b2 and b14 or
            b2 and b16 or

            b3 and b9 or
            b3 and b10 or

            b4 and b9 or
            b4 and b10 or

            b5 and b9 or
            b5 and b10 or

            b6 and b9 or
            b6 and b10 or

            b8 and b9 or
            b8 and b10
        ,
        // lots of things can return numbers
            b3 and b11 or
            b3 and b13 or
            b3 and b14 or
            b3 and b16 or

            b5 and b11 or
            b5 and b13 or
            b5 and b14 or
            b5 and b16 or

            b6 and b11 or
            b6 and b13 or
            b6 and b14 or
            b6 and b16 or

            b8 and b11 or
            b8 and b13 or
            b8 and b14 or
            b8 and b16
        ,
        // only add with bigints can return bigints
        b4 and b12,
        false,
        false,
        false,
        false
        /*
        TODO force all these constraints to be satified:
        ```
            // can't add numbers to bigints 
            (b3 and b12) == false,

            (b4 and b11) == false,
            (b4 and b13) == false,
            (b4 and b14) == false,
            (b4 and b16) == false,

            (b5 and b12) == false,

            (b6 and b12) == false,

            (b8 and b12) == false
        ```
        */
    ] = ???


/*
An example showing that `string + number = string`.
Even inference with partial application works!
*/
def example(): Value [false, true, false, false, false, false, false, false] =
    let partial = x -> add(string(), x);
    let valid = partial(number());
    // let invalid = add(symbol(), string());
    valid