Add Oracle Types

[jcreedcmu]

This PR introduces a new feature, Oracle Types, which is a variant
of the type providers concept from languages like F# and Scala. We
call these Oracles.

This enables features like:

• Connecting out to an external SAT solver from the type language
• Type level arithmetic
• An ORM that automatically extracts type defintions dynamically from
  a running database, without requiring a burdensome explicit schema
  compilation step.
• Automatic language localization of keys in record types
• "Mobile-first" interactive typechecking

More details can be found in our companion repository, featuring various demos,
as well as our paper to appear in SIGBOVIK'21. You can also watch the
the conference presentation.

How it works

We have added a new intrinsic called Shell that allows calling out
to an external type provider, by executing the argument as a shell command.

Usage is quite simple: for example,

type Today = Shell<'date "+%Y-%m-%d"'>

will make the type Today defined to be equivalent (at time of writing) to the string literal type
"2021-04-01\n".

For a more fully worked example, consider the following approach for
calling out to the well-known Z3 constraint solver.
(This assumes you have z3 installed and on your executable path)

//
// First we build up some machinery to generate Z3 inputs.
//

// A phantom type used to express constraints about integer values
type Constr<T> = { constr: T };

// An integer value so constrained
type ConstrNum<T> = number & Constr<T>;

// Generate a Z3 assertion for constraint T
type GenAssert<T> = T extends string ? `(${T})` : 'false';

// Generate Z3 code that checks whether T implies U.
// Z3 will return 'unsat' if the implication *does* hold,
// because T && !U will be false.
type GenZ3<T, U> = `
(declare-const x Int)
(assert ${GenAssert<T>})
(assert (not ${GenAssert<U>}))
(check-sat)
`;


//
// Now we deal with calling Z3 and cleaning up the output
//

// Strip trailing newline from a string literal type
type StripNl<T extends string> = T extends `${infer S}\n` ? S : T;

// Given a string type containing an sexp expressing a z3 program,
// return 'sat' or 'unsat'
type SolverResult<Z3 extends string> =
  StripNl<Shell<`echo '${Z3}' | z3 -in`>>;


//
// Set up some conveniences for the user
//

// If T => U, yields the appropriate result type for constraint U, otherwise unknown.
type InferCond<T, U> = SolverResult<GenZ3<T, U>> extends 'unsat' ? ConstrNum<U> : unknown;

// Convert x from one constraint type to another
export function infer<T, U>(x: ConstrNum<T>): InferCond<T, U> {
  return x as any;
}

type strish = string | number;
export type Plus<T extends strish, U extends strish> = `(+ ${T} ${U})`;
export type LessEq<T extends strish> = ConstrNum<`<= x ${T}`>;

//
// Example usage
//
function test_cases(x: LessEq<5>) {

  // Error, because <= x (+ 2 3) is not intensionally the same as <= x 5!
  { const bad: LessEq<Plus<2, 3>> = x; }

  // However, we can insert an `infer' call to mediate between
  // different representations of logically equivalent constraints:
  { const good: LessEq<Plus<2, 3>> = infer(x); }

  // Error, because not sound to infer <= (+ 2 2) from <= 5!
  { const bad: LessEq<Plus<2, 2>> = infer(x); }

  // Sound, because <= 5 implies <= 6
  { const good: LessEq<Plus<2, 4>> = infer(x); }

}

As you can see, Oracle Types provide a simple and powerful way to
extend the TypeScript type system. Their security, safety, and
all-round general reasonableness is almost assuredly guaranteed by the
fact that some unit tests pass, provided you don't think about it too
hard.

To make some of our examples work, we had to bump up the
instantiationDepth limit. We believe that 640 recursive calls ought
to be good enough for anybody.

[ghost]

Thank you for your submission, we really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution.

❌ jcreedcmu sign now
_{You have signed the CLA already but the status is still pending? Let us recheck it.}

[typescript-bot]

This PR doesn't have any linked issues. Please open an issue that references this PR. From there we can discuss and prioritise.

[phpnode]

This seems like a totally reasonable idea and implementation. 👍 good job.

[sandersn]

@jcreedcmu can you provide a docx version of the paper? That's the standard in our field.

Also the recursiveMappedTypes test now stack overflows. Looks like instantiationDepth=640 was too much for today's node.

[danielearwicker]

I got around the stack limit with:

type MoreDeep = Shell<'tsc ...'>

By recursively invoking TS I can get another 640 deep.

[weswigham]

I look forward to watching the presentation during the livestream later tonight~

[webstrand]

Cool, you can use this to automatically add missing dependencies at compile time.

type injector = Shell<`npm install -D @types/missingTypes`>

Maybe even some kind of conditional compilation that only loads types if they're going to be used.