Compute type fixed point

126 Views Asked by At

Suppose we have some type-function F<T>, and we want to compute its fixed point type X = F<X>. While this might work with types that are objects

interface Tree1<T> { left: T; right: T }
interface Tree extends Tree1<Tree> {}
declare const t: Tree;
const r = t.left.right; // OK

for more generic type-functions it doesn't:

type Tree1<T> = null | { left: T; right: T }
interface Tree extends Tree1<Tree> {} // can't extend not-object

Without a deferred type-level computation given by interface, it's hard to avoid infinite instantiation. The best I could do is just delay it:

interface Tree1<T> { left: T; right: T }
type Temp1<T> = { a: null | [T[keyof T], T[keyof T]] }
interface Temp2 extends Temp1<Temp2> {}
declare const t: Temp2;
const r = t.a; // Type instantiation is excessively deep

Also it is possible to fix it by introducing extraneous nodes into the tree, but that's not what I'm after.

type Tree1<T> = null | { left: T; right: T }
type Tree = Tree1<{ref: Tree}> // OK

Neither is directly defining Tree.

type Tree = null | { left: Tree, right: Tree }

How to compute that elusive fixed point?

type Tree1<T> = null | { left: T; right: T }
type Tree = ???
const t: Tree = {left: null, right: {left: null, right: null}};
1

There are 1 best solutions below

0
On

I don't know of a way to create a literal fixed point of a type function, but you can construct type that refers to itself indirectly through a property. Depending on what you're using it for, that might be good enough.

I came to your question because I've been thinking about how to type abstract syntax trees. Specifically, I want an to type ASTs for a related family of languages. For example, we could have a type for expressions involving adding variables together, like "a + b + c", and we could have another type for expression involving variables, addition, and multiplication, such as "a*b + c".

I want these to be real static types — I don't want to just use one big AST type to rule them all. But I also want the types to be extendable. I don't want to have to re-define the whole grammar every time I add some new type of AST node.

So I was thinking, if you could have a generic parameter that corresponds to the language variant, you could define AST nodes like this:

type Plus<α extends Grammer> = { 
    kind: "plus"
    left: Expr<α>
    right: Expr<α>
}

Then you can define a generic version of the grammar like this:

type AbelianGroupBaseGrammer<α extends Grammer> = Variable<α> | Plus<α>

And turn it into a monotype by constructing a fixed point

AbelianGroupGrammer = AbelianGroupBaseGrammer<AbelianGroupGrammer>

You could extend it to larger languages like so

type RingBaseGrammar<α extends Grammer> = AbelianGroupBaseGrammer<α> | Times<α>

This doesn't work in typescript, You'll get the error Type alias 'AbelianGroupGrammer' circularly references itself

But if you hide the self-reference inside an object property, you can get the same effect. This version does type check without errors:

type Grammer = {
    "expression": unknown
}

type Expr<α extends Grammer> = α["expression"]

type Plus<α extends Grammer> = { 
    kind: "plus"
    left: Expr<α>
    right: Expr<α>
}

type Times<α extends Grammer> = { 
    kind: "times"
    left: Expr<α>
    right: Expr<α>
}

type Variable<α> = { 
    kind: "variable"
    name: string
}

type AbelianGroupBaseGrammer<α extends Grammer> = { 
    "expression": Variable<α> | Plus<α>
}

type AbelianGroupGrammer = { 
    "expression": Expr<AbelianGroupBaseGrammer<AbelianGroupGrammer>>
}

type RingBaseGrammer<α extends Grammer> = { 
    "expression": Expr<AbelianGroupBaseGrammer<α>> | Times<α>
}

type RingGrammer = {
    "expression": Expr<RingBaseGrammer<RingGrammer>>
}

const x : Expr<AbelianGroupGrammer> = {kind: "variable", name: "x"}
const y : Expr<AbelianGroupGrammer> = {kind: "variable", name: "y"}
const x_plus_y : Expr<AbelianGroupGrammer> = {kind:"plus", left: x, right: y}
const x_times_x_plus_y : Expr<RingGrammer> = {kind:"times", left: x, right: x_plus_y}

function group2ring(a : Expr<AbelianGroupGrammer>) : Expr<RingGrammer> { 
    return a
}