leibniz

A small TypeScript framework for unit testing types using Leibniz equality.

• Motivation
• Usage
  • Leibniz equality
    • Eq
    • Other relations
  • Writing tests
    • Basic tests
    • Relation tests
    • Custom relation tests
  • Examples
    • Basic examples
    • Testing for properties
    • Safe JSON encoding
• Caveats

Motivation

Types are a very useful tool to ensure safety, especially for library designers. However, if you're designing a library that works with complicated types, it's possible that you can accidentally change your types in a way that makes your types too broad, too narrow, or changes type inference. leibniz gives you a framework to write tests to make sure that the code you expect to compile still compiles, and the code that shouldn't compile still doesn't.

Usage

Leibniz equality

Eq

The most important type in leibniz is Eq<A, B>. A value of type Eq<A, B> is a proof witnessing that two types A and B are equal; if you have a value of type Eq<A, B>, then you know that A and B are the same type. Whenever the compiler can figure out that two types are equal, you can simply use refl (for "reflexive") to make an instance of Eq for those two types:

type A = number;
type B = { foo: number; }["foo"];

const proof: Eq<A, B> = refl;

Like other kinds of equality, Leibniz equality is reflexive, transitive, and symmetric:

• refl proves reflexivity by making an Eq<A, A> for any type A
• sym can be used to turn an Eq<A, B> into an Eq<B, A>, though the compiler should normally figure this out for you
• trans can compose an Eq<A, B> and an Eq<B, C> into an Eq<A, C>
• The sub1 and sub2 functions can be used to substitute the first or second type using another equality

Interacting with these proofs is almost never necessary, but if the compiler has trouble figuring out proofs, you can use the proofs from previous tests to help it out. Usually, you will only have to write refl, and the compiler will do most of the heavy lifting for you.

Other relations

There are many types derived from Eq representing other type relationship proofs:

• NotEq<A, B>: A is not the same type as B
• Sub<A, B>: A is a subtype of B
• NotSub<A, B>: A is not a subtype of B
• StrictSub<A, B>: A is a strict subtype of B (A is a subtype, and is not the same type as B)
• NotStrictSub<A, B>: A is not a strict subtype of B
• Super<A, B>: A is a supertype of B
• NotSuper<A, B>: A is not a supertype of B
• StrictSuper<A, B>: A is a strict supertype of B
• NotStrictSuper<A, B>: A is not a strict supertype of B
• Related<A, B>: A is related to B (one is assignable to the other)
• Disjoint<A, B>: A and B are disjoint (neither is assignable to the other)

Most of these are derived types that can be composed from more basic relationships. For example:

type StrictSub<A, B> = Sub<A, B> & NotEq<A, B>;

All of these should still be able to be instantiated with only a single refl.

Writing tests

leibniz tests are written using the test family of functions. If your tests compile, then all leibniz tests passed. If your tests do not compile, then one of your tests has failed.

If you wish, you can plug a no-op success into your preferred testing framework so it logs that your leibniz tests passed:

import "mocha";
import { testEq, refl } from "@nprindle/leibniz";

testEq<number, number, "sanity check">(refl);

describe("types", () => {
    it("should compile", () => {});
});

Basic tests

This simplest function in leibniz is test, which simply makes sure that an expression or block of code compiles. It is used like so:

test(() => ...);

// optionally, add a description of the test
test<"...">(() => ...);

For example:

// compiles and passes
test<"strings can be appended">(() => {
    const x = "foo";
    const y = "bar";
    return x + y;
});

// fails to compile
test<"strings can be multiplied">(() => {
    const x = "foo";
    const y = "bar";
    return x * y;
});

To group together multiple expressions, you can simply provide an array literal or object literal:

// combining cases in an array
test<"these function calls all compile">(() => [
    foo(3),
    bar("test"),
    baz(foo),
]);

// use an object to name the cases
test<"these function calls compile too">(() => {
    check1: foo(7),
    check2: bar("quux"),
    check3: baz(bar),
});

The test function is actually very boring; since it only needs to check that your code compiles, it's just a no-op; the code in the block is never actually run.

Relation tests

leibniz provides many functions to test the relationship between types. It provides a function for every provided relation proof type (see Other relations). Each function expects a single proof that the relation holds, though just passing refl almost always works.

Here's an example of the most basic relationship test function, testEq:

testEq<
    number,
    number,
    "sanity check that 'number' is equal to 'number'"
>(refl);

Each test function takes two type parameters, the types to compare. They may additionally take an optional third parameter, usually a literal string type that can serve as a description of what the test is checking. If no description is provided, it will default to an empty description.

The provided relation tests are:

• testEq
• testNotEq
• testSub
• testNotSub
• testStrictSub
• testNotStrictSub
• testSuper
• testNotSuper
• testStrictSuper
• testRelated
• testDisjoint

Custom relation tests

If you need a relation test that is not provided by default, you can test a custom relation using the testRel function. Since the relation proof types can compose using & and |, we can create more complicated relationships out of them.

For example, let's say that we want to test that two types are related (one is a subtype of the other), but not equal. That is, we need a Related<A, B> proof, but also a NotEq<A, B> proof. We could write this as follows:

testRel<
    Related<A, B> & NotEq<A, B>,
    "check that A and B are related but not the same"
>(refl);

The testRel function is powerful; you can use it to define all of the other provided testing functions. For example:

testRel<
    Sub<A, B> | Super<A, B>,
    "same as testRelated<A, B>"
>(refl);

testRel<
    Sub<A, B> & NotEq<A, B>
    "same as testStrictSub<A, B>"
>(refl);

Examples

Basic examples

Let's write some basic sanity checks to show how leibniz tests work:

testEq<
    string,
    string,
    "a type should be equal to itself"
>(refl);

testSub<
    number,
    number,
    "a type should be a subtype of itself"
>(refl);

// This will fail to compile
testSub<
    number,
    3,
    "number is not a subtype of a literal type"
>(refl);

testEq<
    number[],
    { foo: number }["foo"][],
    "equality of derived compound types"
>(refl);

One useful application of type testing is to check that your type inference behaves the way you expect it to. For example:

let x = 3;
testEq<typeof x, number>(refl);
// passes (compiles without error)

const y = 3;
testEq<typeof y, number>(refl);
// fails! const actually infers the narrower literal type '3'

const z = 3;
testEq<typeof z, 3>(refl);
// passes

If you're writing an API with complicated inferred types, it's essential to make sure that types are inferred the way you expect them to be.

Testing for properties

As a more practical example, let's say that we have a component C, which is an object with certain properties. Let's say that the shape of C changes frequently, but the users of our API know that it should always be an object with a url: string property. We want to test that no matter what changes we make to C, we always have that property. To check that the type has this property, we can test that intersecting the keys of C with { url: string; } gives us back { url: string; }:

test<"C tests">(() => {
    testSub<
        C,
        object,
        "C should always be an object"
    >(refl);

    testEq<
        C | { url: string; }, // '|' intersects the keys of two types
        { url: string; },
        "C should always have a 'url: string' property"
    >(refl);
});

We can even abstract this into a separate helper test function:

// Takes a proof of the above form and simply returns it
function testHasProps<
    T extends object,
    P extends object,
    _doc = ""
>(proof: Eq<T | P, P>): Eq<T | P, P> {
    return proof;
}

testHasProps<
    C,
    { url: string; },
    "C should always have a 'url: string' property"
>(refl);

Now, if we make a mistake (like change the shape of C to have a URL: string instead), our tests will catch it!

Safe JSON encoding

Let's say we define a function jsonEncode which wraps JSON.stringify. Since JSON.stringify takes an any, it has unxpected behavior when called on data that can't be represented in JSON. For example, JSON.stringify([undefined]) is "[null]"!

The input type of our jsonEncode will be safe; it can only stringify data which can be represented in JSON:

// Implementing this type is left as an exercise for the reader
type JsonValue = ...;

function jsonEncode(data: JsonValue): string {
    return JSON.stringify(data);
}

We want to write some tests to make sure that it would compile if given valid JSON inputs, but wouldn't compile if given an invalid JSON input. A JSON value may be a string, a boolean, a number, null, an array of JSON values, or an object with string keys and JSON values (that may also be undefined; the keys will simply be excluded when stringifying).

One approach is to write a basic test block to make sure that it accepts some valid inputs:

test<"jsonEncode should accept valid JSON inputs">(() => [
    jsonEncode("foo"),
    jsonEncode(true),
    jsonEncode(3.14),
    jsonEncode(null),
    jsonEncode([]),
    jsonEncode({}),
    jsonEncode({ foo: undefined }),
]);

We could also directly verify that the types can be passed, by checking that the types are valid subtypes of the function's parameter. We can find the type of the argument to jsonEncode with Parameters<typeof jsonEncode>[0]:

test<"jsonEncode should accept valid JSON inputs">(() => {
    type JsonEncodeParam = Parameters<typeof jsonEncode>[0];
    testSub<string, JsonEncodeParam>(refl);
    testSub<boolean, JsonEncodeParam>(refl);
    testSub<number, JsonEncodeParam>(refl);
    testSub<null, JsonEncodeParam>(refl);
    testSub<JsonValue[], JsonEncodeParam>(refl);
    testSub<Record<string, JsonValue | undefined>, JsonEncodeParam>(refl);
});

Now, we also want to make sure that jsonEncode does NOT accept invalid inputs like undefined or undefined[]. To do this, we can check that these types are not subtypes of the parameter type:

test<"jsonEncode should not accept invalid inputs">(() => {
    type JsonEncodeParam = Parameters<typeof jsonEncode>[0];
    testNotSub<
        undefined,
        JsonEncodeParam,
        "jsonEncode should not accept undefined"
    >(refl);
    testNotSub<
        undefined[],
        JsonEncodeParam,
        "jsonEncode should not accept undefined[]"
    >(refl);
});

Now, if we later incorrectly change the type of JsonValue to accept undefined, our tests will fail to compile, and we can catch the error before release! Note that in addition to making sure that certain code will compile, leibniz can also be used to make sure that certain code won't compile.

Caveats

TypeScript's type system is not sound. By its nature, there are many deliberate holes in the type system, only some of which can be turned off. Because of this, there are two primary caveats to using leibniz as a consequence of TypeScript's type system:

1. You need strict type checking enabled. Without it, there are too many unsound type system holes, like bivariant parameter checking, that make it impossible to soundly prove anything with the type system.
2. Like pineapple in gelatin, leibniz proofs dissolve whenever an any is introduced, since it's an intentional hole in the type system. leibniz works off of type equality, and any can be equal to any type. For example:

const lemma: Eq<any, any> = refl;

// fails, since number != string
const proof1: Eq<number, string> = refl;

// succeeds, because 'any' is evil
const proof2: Eq<number, string> = lemma;

Fortunately, most users that care enough about types to want to test them will already have strict type checking enabled. With respect to avoiding any, it's best to prefer unknown in any circumstances where type safety matters.