Writing types in JavaScript instead of TypeScript

[SimonMeskens]

Okay, so I've been pondering (and talking to @axefrog). If TypeScript's type system itself is turing complete and that offers great opportunities, why are we writing the types in this stunted turing tarpit language, instead of writing the types themselves in JavaScript too? Here's the idea: you write a program, that when run, outputs itself without the type annotations. This is exactly like what TypeScript does, but in this case, the input is JavaScript, the output is JavaScript and the original JavaScript is both the source and the compiler at the same time (running the program is compilation, the output is the stripped version).

Here's what that would look like:

import { Type, isType } from "js-types";

// Record definition

const Complex = {
    real: Number,
    imaginary: Number
}

// Function definition

const ComplexMult = (a, b) => {
    if (isType(a, Number) && isType(b, Number)) {
        return Number;
    } else {
        throw TypeError();
    }
};

Type(
    ComplexMult,
    function mult(a, b) {
        return {
            real: (a.real * b.real) - (a.imaginary * b.imaginary),
            imaginary: (a.real * b.imaginary + a.imaginary * b.real)
        };
    }
);

// Alternate ways to write the definition:

const ComplexMultAlt1 = (a, b) => {
    if (isType({ a, b }, { a: Number, b: Number })) {
        return Number;
    } else {
        throw TypeError();
    }
};

// With arrays instead of objects:

const ComplexMultAlt2 = (a, b) => {
    if (isType([a, b], [Number, Number])) {
        return Number;
    } else {
        throw TypeError();
    }
};

// Helper definition, notice it returns a function

const Func = (inputTypes, outputType) => {
    return (...inputs) => {
        if (isType(inputs, inputTypes)) {
            return outputType;
        }
        else {
            throw TypeError();
        }
    };
};

// With this helper, we could've done this:

Type(
    Func({ a: Complex, b: Complex }, Complex),
    function mult(a, b) {
        return {
            real: (a.real * b.real) - (a.imaginary * b.imaginary),
            imaginary: (a.real * b.imaginary + a.imaginary * b.real)
        };
    }
);

// Example of function returning function, very simple

Type(
    Func(Complex, Func(Complex, Complex)),
    function add(a) {
        return (b) => ({
            real: a.real + b.real,
            imaginary: a.imaginary + b.imaginary
        });
    }
);

// Generics, again, super simple

const IdentityFunction = a => a;

Type(
    IdentityFunction,
    function identity(a) {
        return a;
    }
);

// Variadic kinds
// Note that f would also be a type-checking function
// when it comes in

const CurryFunction = (f, ...a) => {
    if (isType(f, Function)) {
        return (...b) => f(...a, ...b)
    }
    else {
        throw TypeError();
    }
};

Type(
    CurryFunction,
    function curry(f, ...a) {
        return (...b) => f(...a, ...b);
    }
);

And here's the output of running that program:

function mult(a, b) {
  return {
    real: a.real * b.real - a.imaginary * b.imaginary,
    imaginary: a.real * b.imaginary + a.imaginary * b.real
  };
}

function add(a) {
  return b => ({
    real: a.real + b.real,
    imaginary: a.imaginary + b.imaginary
  });
}

function identity(a) {
  return a;
}

function curry(f, ...a) {
  return (...b) => f(...a, ...b);
}

I know this is quite the silly idea, but I think there's merit to it. As you can see, the sample seems to indicate it can easily type a curry function, something that is apparently quite hard in TypeScript.

[SimonMeskens]

I also wonder if this is something you could add onto TypeScript itself. Allow TS to consume these type-checking functions, so we can write the really complex types ourselves in JS (or TS).

[atennapel]

You need to be able to check the types statically, in your examples in seems like you are inspecting the arguments at runtime. If you were to write some complex type checking function this way it wouldn't work because you won't have the arguments at runtime! For example the arguments might come from a network request.

Your CurryFunction does not check that the types of the arguments of the function actually match the arguments themselves, it only checks that the function is actually a function.

I don't think a Turing complete type system is great at all, you don't want loops or inconsistencies at the type level. You want the type checker to terminate and tell you if the types you wrote are correct.

[SimonMeskens]

I think I didn't explain the samples very well. Let me try to correct it. First off, I'm not saying turing completion is what makes it good, I'm just saying that JavaScript is a way better language than the TypeScript annotation system, so it makes sense to write types in JS, not the TS annotation system. To this end, I give an example of that and I'm trying to show that it very trivially allows for the typing of a "curry" function.

Let's go over some of the other points: 1) The bottom code is what is output by the compiler, there are no types available at runtime, so there's no checking of arguments at all. 2) The sample provided doesn't use any iteration or recursion, so there's no chance of this code not terminating. Could you write a piece of type-checking code that doesn't terminate? Yes, but unlike in TS, it would be fairly obvious and the sample types a rather complex piece of code without using loops or recursion, so it's probably rare.

Now let's go over the CurryFunction in detail to show it does indeed prove type correctness:

CurryFunction will be called by the compiler with a list of types. It checks that the type of "f" is a function and creates a closure over the rest of the types in ...a (closures are like generics). It returns a type checking function that takes a new list of types, which in turn will run the type-checking function "f" with the closed over types and the newly provided types. "f" will run and throw a type error if it doesn't accept this list of types. If the types are correct for "f", it will return the return type of "f". This is what we set out to do, the function is correctly checking the types of the curry function.

Give me a second and I'll write up a sample of running CurryFunction with actual types.

[atennapel]

Aaah I'm sorry! I didn't read your code well enough. So the arguments to the functions in the first sample are types. That is very interesting, it reminds me of Shen (http://shenlanguage.org/learn-shen/index.html#9 Types).

[SimonMeskens]

Yeah, it's quite similar to how typing is handled in some Lisp dialects. It's an odd way to work, instead of a compiler, you have a compiler library. You write the compiler for every piece of code yourself, using this library. The code is run once to provide the actual runtime code as output.

Here's a sample that shows how CurryFunction works. That first console.log would be what's run at runtime, the second console.log is what the compiler actually checks:

// A very naive implementation of isType
const isType = (a, b) => {
    if (a !== Number && a !== String) {
        a = Function;
    }
    return a === b;
}

// The function we're going to curry
const mult = (a, b) => a * b;

// The type-checking function for this function
const MultFunction = (a, b) => {
    if (isType(a, Number) && isType(b, Number)) {
        return Number
    }
    else {
        throw TypeError();
    }
}

// The curry function
const curry = (f, ...a) => (...b) => f(...a, ...b);

// Here's our CurryFunction that type-checks it
const CurryFunction = (f, ...a) => {
    if (isType(f, Function)) {
        return (...b) => f(...a, ...b)
    }
    else {
        throw TypeError();
    }
};

// At some point in the code, the compiler encounters a call to curry
console.log(curry(mult, 2)(3) === 6);

// To type-check this piece of code, it will run the CurryFunction
console.log(CurryFunction(MultFunction, Number)(Number));

// An incorrect call will trigger a TypeError
console.log(CurryFunction(MultFunction, String)(String));

// Console output: true, Number, TypeError

[atennapel]

Yeah I see now, it's a very cool idea. I suggest you read the "Type Systems as Macros" paper, it's quite similar to what you are proposing.

I think type inference will complicate your system though, you would no longer to be able to check equality of types easily in the presence of type-variables.

[SimonMeskens]

I'll have a read, I seem to vaguely recall reading it before.

The final step that might be cool is to add this as a feature to TypeScript:

type CurryFunction = import("something").CurryFunction;

const curry: CurryFunction = (f, ...a) => (...b) => f(...a, ...b);

Not sure what syntax it would take, but you get the idea, I can now just import these new JS types and use them in TS.

[SimonMeskens]

Ah, yes, that paper is exactly what I propose, with one small change, I don't like macro systems, I prefer programs you run, that output other programs. The reason is exactly the same: macro languages tend to be stunted, awful languages, when there's a perfectly good language right there. I can even imagine typing your types, so you'd end up with a program you run, to get a program you run, to get the actual program, etc. Small modular compilation steps.

[SimonMeskens]

@tycho01 If I wanted to extend the TS compiler to be able to write custom typecheckers like I did above, do you know where I'd need to hook in? I'm very unfamiliar with the TS codebase.

I'm looking for a point where the compiler goes: "the code is trying to call function X with parameters Y and Z, are those types allowed?"

[KiaraGrouwstra]

This is a fair question, and I sympathize with some of the frustration -- TS types are definitely more complex than doing JS, while, even if it merits the label Turing complete, it certainly isn't feature complete, as there's plenty we can't do in it, unlike JS. Moreover, issues with TS types can be tough to debug, as we can't just add logging statements. It's trial and error, step by step.

JavaScript is a way better language than the TypeScript annotation system, so it makes sense to write types in JS, not the TS annotation system.

I think @atennapel hit the heart of the issue though: it's fairly hard to approach TS's level of type checking this way: types are sets, while JS does values. Say, you could have an operator +, but it needs to be able to type-check both operands typed 1 and number.

So operators in TS abstract over this level of granularity, which means for most types in this library, you can substitute an input type number with 1 or 1 | 2 | 3, and still expect a sane inferred result type. And while set may sound like Set, types are abstract descriptions, rather than literal enumerations of all possible values. That's what TS does.

I think TS got that right -- having a type system like it allows inferring over the original code as well. In an ideal world, the standard library is so well-typed inference can do the rest. To nail all the details like capturing generics' values, checking assignability, and giving all the right errors, I think you'd end up with something very similar to TS (/ Flow).

I don't think a Turing complete type system is great at all, you don't want loops or inconsistencies at the type level. You want the type checker to terminate and tell you if the types you wrote are correct.

Now, I've probably been the strongest proponent of a powerful type system. But I agree, you'd want your type checker to terminate and tell you what's what. Non-termination has been an issue for problematic types in this repo, the result of TS issues combined with my use of recursive types used to e.g. iterate tuples. So, why iterate? I wanted to type e.g. R.path(['a', 'b'], {a: {b: 2}}); //=> 2. I don't think iteration is evil, though non-termination is definitely tougher to debug than errors. And I think that's where type repos like this and typelevel-ts could help, handling the tougher parts so users won't have to.

Could you write a piece of type-checking code that doesn't terminate? Yes, but unlike in TS, it would be fairly obvious

I think in either case this would be the result of a faulty looping condition.

TS types may be another bit to learn, but I think that's a necessary evil, and on the bright side, the operators are limited to just &, |, keyof, in, and member access.

I'd flip the question to ask, which parts of TS are not useful to accomplish its goal? I'd argue for the most part all its parts are there for a reason.

@SimonMeskens:

@tycho01 If I wanted to extend the TS compiler to be able to write custom typecheckers like I did above, do you know where I'd need to hook in? I'm very unfamiliar with the TS codebase. I'm looking for a point where the compiler goes: "the code is trying to call function X with parameters Y and Z, are those types allowed?"

So, the files are in https://github.com/Microsoft/TypeScript/tree/master/src/compiler. You'll see a bunch, and they're each handling a different part of the compiler. However, all of the interesting parts happen in the type checker, checker.ts -- the biggest part of the compiler. It's too big for Github to show, so you'd need to download/clone the repo to see.

Functions in there mostly follow patterns like get*Type, assignability checks, is*Type, check*. Your scenario here is about function checkCallExpression. In there, it's got the nodes of the function and its (type) parameters. These are first checked individually, after which it calls into getReturnTypeOfSignature where, eventually (following some more internal calls), it confirms whether the used (type) parameters match the type signature of the function. If not, it attaches an appropriate error message to the right node, so in your IDE the right part of the code gets a red squiggle with the appropriate error tooltip.

[SimonMeskens]

Thanks for the reply!

I do get your argument about a good inference engine and I agree, but I do think that you can almost prove that no type inference engine will ever be able to figure out some of the more complex types, so we are stuck with annotations at some point. TypeScript's annotations do amazingly well for simple stuff, but I think you need a better workhorse for code that has deeper level of generics, and we have a good language right there to do it. As the sample shows, while you probably don't want to pull out this gun for the simpler types, it does massively simplify typing the harder types.

That's why I decided it might be best to combine the two approaches and extend TypeScript to be able to load types from a JS module. This way, you can move only the complex typing to such a module and keep using the inference engine and simple annotations for most of the codebase.

I'll have a look at checker.ts, to see if I can simply add this functionality to TS. It doesn't sound very hard in theory, though releasing the code might be more of an issue, which I'll tackle later, I just want to get a simple proof of concept going.

[KiaraGrouwstra]

Yeah, zero annotations wouldn't be realistic. I think most of the current gaps in functionality are fixable though. If I got my last few PRs ready and merged we might be a bit further in that respect. I think when we can type partial-lenses we're largely there, and that's essentially just combining the issues currently faced in typing Ramda. But if those barriers are out of the way, then we're probably there -- the inference issues are mostly at the lower level I think (what can we type, has the standard library been typed well).

Maybe the reason I'm optimistic is I already wrote types using missing features (PRs), so I haven't really found much totally out of reach yet. I'm not so much worried about generics, specifically, but there's a bit still up in the air, like iterating object literal / union types.

A low-level API like JS would definitely provide ways to do any thinkable manipulation, admittedly. Then again, a TS equivalent is easy to imagine -- just a type-level Object.keys, and I feel like ditching everything TS has nailed is raising way more new questions than it would address.

Manually throwing a TypeError where you did seems to work well enough, but if you were to scale this to all the errors TS will already catch for you for free, I'm not sure this would still look better than just learning TS type operators...

On another note, you may wanna check @gcanti's https://github.com/gcanti/tcomb and maybe JSON Schema, both of which check stuff using JS as well, like Sanctuary. Probably more run-time focused though...

If you get more questions about the compiler, let me know!

[SimonMeskens]

My example was very crude, if I manage to hook into the TS system, you'd still be able to throw decent errors of course. And yeah, I agree that with just JS types, that might be a serious step backwards from what we have now (even with a good inference engine).

I think the next step is for me to put the money where my mouth is and provide a PoC, so we can further discuss merits :)

And yeah, I keep wanting to play around with tcomb and schemas, I should do that at some point.

[KiaraGrouwstra]

I'm gonna mark closed in the sense of 'not actionable within the scope of this lib'. Discussion though is always welcome.