Convert to TypeScript

[mlhaufe]

Current branch in progress: https://github.com/mlhaufe/brevity/tree/typescript

Desired usage (as of March 26):

type ShapeType = { Circle: [number], Rectangle: [number, number] }
const Shape = Data<ShapeType>({ Circle: ['radius'], Rectangle: ['width', 'height'] })

type DiskType = [[number,number], [number,number], number, string]
const Disk = Data<DiskType>(['position', 'velocity', 'radius', 'item'])

This requires two features though:

1. const type parameters which requires features in at least TypeScript 5.0+

Without this feature the end-user is required to annotate every Data() usage with as const:

const Disk = Data(['position', 'velocity', 'radius', 'item'] as const)

2. Partial Generic Inference (Typescript bug #10571)

Because of this issue, the desired syntax is not viable.

This works but the properties are of type any:

const Disk = Data(['position', 'velocity', 'radius', 'item'])

This does not work:

type DiskType = [[number,number], [number,number], number, string]
const Disk = Data<DiskType>(['position', 'velocity', 'radius', 'item'])

TypeScript complains that the 2nd generic is not provided. It's all or nothing. It's not desirable to have the end-user copy/paste the arguments into the 2nd generic position:

type DiskType = [[number,number], [number,number], number, string]
type DiskProps = ["position", "velocity", "radius", "item"]
const Disk = Data<DiskType, DiskProps>(['position', 'velocity', 'radius', 'item'])

Notice the additional syntactic overhead for this Data definition. From 1 line to 3 lines. Inlining the types make readability worse:

const Disk = Data<
    [[number,number], [number,number], number, string], 
    ["position", "velocity", "radius", "item"]
>(['position', 'velocity', 'radius', 'item'])

An object literal is even worse.

In general I'm suspecting this is not worth the effort. To quote Tim Sweeney:

"With correctness proofs, you often run into the problem that the theorem you aspire to prove is approximately as lengthy and complicated as a well-written but unproven implementation of the program itself. [...] If your theorem is as complicated as a simple but unproven implementation of a program, then the former is no better than the later, because you can just as easily have bugs in your theorem (e.g. causing the wrong things to be proven) as bugs in your program (causing unexpected runtime behavior)." -- Tim Sweeney

[mlhaufe]

Some early notes on typing Trait:

https://stackoverflow.com/questions/74917137/how-do-i-define-a-typescript-type-that-will-reduce-a-record-of-functions-to-an

Since that was written, Trait has has been updated to accept an instance of Data as it's first argument:

const and = Trait(Bool, {
    False: (left, _) => left,
    True: (_, right) => right
 })

If Data can be typed appropriately, then in theory there should be little to nothing to annotate on Trait.