Existential type?

[dead-claudia]

Here's a case where I need a few existentials. It's for a definition file, where I need to have parameters for Binding and Scheduler, but it doesn't matter to me what they are. All I care about is that they're internally correct (and any doesn't cover this), and I'd rather not simulate it by making the constructor unnecessarily generic.

The alternative for me is to be able to declare additional constructor-specific type parameters that don't carry to other methods, but existentials would make it easier.

export interface Scheduler<Frame, Idle> {
    nextFrame(func: () => any): Frame;
    cancelFrame(frame: Frame): void;
    nextIdle(func: () => any): Idle;
    cancelIdle(frame: Idle): void;
    nextTick(func: () => any): void;
}

export interface Binding<E> extends Component {
    binding: E;

    patchEnd?(): void;

    patchAdd?(
        prev: string | E | void,
        next: string | E | void,
        pos: number,
    ): void;

    patchRemove?(
        prev: string | E | void,
        next: string | E | void,
        pos: number
    ): void;

    patchChange?(
        oldPrev: string | E | void,
        newPrev: string | E | void,
        oldNext: string | E | void,
        newNext: string | E | void,
        oldPos: number,
        newPos: number
    ): void;
}

export class Subtree {
    constructor(
        onError?: (err: Error) => any,
        scheduler?: type<F, I> Scheduler<F, I>
    );

    // ...
}

export class Root extends Subtree {
    constructor(
        component: type<E> Binding<E>,
        onError?: (err: Error) => any,
        scheduler?: type<F, I> Scheduler<F, I>
    );

    // ...
}

[dead-claudia]

Note: Attrs above is implicitly existential (like function type parameters) with an additional F-bounded constraint - it's mathematically equivalent to exists<A extends {C: ObjectComponent<A>}> A, and so after a little reduction it becomes exists<A extends {C: exists<S> m.Component<A, S>}> A. And it's that existential within the constraint that mucks everything up and makes it not simply reducible to only things with never or unknowns.

(This is also why System F-sub is so difficult to check - it's these kind of polymorphic dependencies that make it extremely difficult.)

[masaeedu]

Code like this is generally invalid as state isn't checked for compatibility

this is a case where exists<T> F<T, U> is not equivalent to either F<unknown, T> or F<never, T>

etc.

This is because Component is invariant in its state parameter. If it weren't (i.e. if it was covariant or contravariant) never/unknown would suffice.

---

Regarding the snippet itself, this is another rather tremendous example when you include the library definitions, but as far as I understand it from skimming: Attrs can be inlined to:

interface Attrs { C: m.Component<this, unknown> }

If we want to replace the unknown with an existential, we can use the standard duality trick:

interface Attrs<X> { C: m.Component<this, X> }
type SomeAttrs = <R>(f: <X>(c: Attrs<X>) => R) => R

And now we have:

export const ProxyComp: m.Component<SomeAttrs, State> = {
  oninit(vnode) {
    this.n = 1;
    vnode.attrs(({ C }) => C.oninit?.call(this, vnode)) // doesn't typecheck
  },
  oncreate(vnode) {
    vnode.attrs(({ C }) => C.oncreate?.call(this, vnode)) // doesn't typecheck
  },
  ...
}

Whether the failure to typecheck is good or bad I can't say, because I don't understand what the code is supposed to be doing. A simpler/more library agnostic example might help.

[dead-claudia]

@masaeedu Attrs as is used in Mithril's type defs are covariant in some respects, but not all. You can use a superset of attribute keys without issue, but the inner state parameter is invariant. Also, functions aren't accepted as parameters (and never have been), so I can't exactly just do that. (Plus, there's perf concerns with that.)

It's hard to give a library-agnostic one because I've rarely encountered them outside libraries, frameworks, and similar internal abstractions. But I hope this explains better what's going on.

[masaeedu]

Also, functions aren't accepted as parameters (and never have been), so I can't exactly just do that.

Interesting. Are records containing functions accepted as parameters?

[dead-claudia]

@masaeedu Yes, but they're parameterized at the record level.

Specifically, vnode.state is identical across all lifecycle methods, both within attributes and within components. And while it's rare for people to use the vnode.state defined in components (it's identical on both sides of that boundary, too), it's not that uncommon for people to use it within DOM nodes as a quick state holder for third-party integrations when creating a whole new component is overkill. Think: things like this:

return [
    m("div.no-ui-slider", {
        oncreate(vnode) {
            vnode.state.slider = noUiSlider.create(vnode.dom, {
                start: 0,
                range: {min: 0, max: 100}
            })
            vnode.state.slider.on('update', function(values) {
                model.sliderValue = values[0]
                m.redraw()
            })
        },
        onremove(vnode) {
            vnode.state.slider.destroy()
        },
    }),
    m("div.display", model.sliderValue)
]

This is rather difficult to type soundly without existential types within Mithril's DT types itself, and you'd have to give several explicit type annotations. Though the more I dig into this, it's possible with a type parameter on m as it is technically covariant on this end.

So the invariance issue is only with components' state, and specifically when used generically (like via m(Comp, ...)).

[dead-claudia]

Okay, from #1213, I've stumbled across another case where this is needed.

type Prefixes<A extends any[], R> = (
    A extends [...infer H, any] ? Prefixes<H, R | H> : R
);

type Curried<Params extends any[], Result> = {
    (...args: Params): Result;
    <A extends Prefixes<Params, never>>(...args: A):
        Params extends [...A, ...infer B] ? Curried<B, Result> : never;
};

function curried<F extends (...args: any[]) => any>(
    fn: F
): F extends ((...args: infer A) => infer R) ? Curried<A, R> : never {
    return (
        (...args: any[]) => args.length == fn.length - 1
            ? curried(rest => fn(...args, ...rest))
            : fn(...args)
    ) as any;
}

function a<T>(b: string, c: number, d: T[]) {
  return [b, c, ...d];
}

const f = curried(a);

const curriedF: (<T>(rest: T[]) => Array<number | string | T>) = f('hi', 42);
const appliedF: Array<number | string> = f('hi', 42, [1, 2, 3]);

In the above snippet, appliedF should work, but doesn't. This is because the generic constraint of a vanishes when passed into curried, getting normalized to unknown rather than making Curried<A, R> existentially qualified as `exists Curried<[T[]], (number | string | T)[]>. While this doesn't itself require new syntax to resolve, it does require keeping the type existentially qualified throughout, meaning this would need to happen regardless of whether there's syntax.

The concrete issue can be stripped down a lot further.

declare function clone<F extends (a: any) => any>(
    fn: F
): F extends ((a: infer A) => infer R) ? ((a: A) => R) : never;

function test<T>(a: T): T {
  return a;
}

const appliedF: number = clone(test)(1);

In this case, appliedF fails to type-check as the parameter and return value are both assumed to be unknown, and the parameterization is lost due to the lack of true existential types.

I left out the implementation of clone, but it's afflicted with similar issues.

What this translates to is a couple things:

• I can't wrap generic functions while keeping them generic, because TS isn't able to propagate the generic parameters beyond just the immediate function. (This also comes into play with things like promisifying Node functions.)
• I can properly type currying non-generic functions without issue, but I cannot properly type curried generic functions.

Fixing this essentially means you have to have existential types, whether you provide syntax for it or not, because there really isn't any other way that isn't essentially just that but more complicated and/or haphazard.

(cc @masaeedu - I know you were looking for things outside the purview of DOM frameworks, and this counts as one of them.)

[masaeedu]

I went straight to the second snippet because I'm having a bit of a hard time wrapping my head around the first one. As far as the second one goes, I'm not sure what role we'd want existential types to play. AFAICT the problem is that:

type ConditionalTypesDontWorkWithGenerics<F> = F extends ((a: infer A) => infer R) ? (a: A) => R : never

function test<T>(a: T): T {
  return a;
}

type Result = ConditionalTypesDontWorkWithGenerics<typeof test>
// Result = (a: unknown) => unknown

Whereas you'd want Result = typeof test = <T>(a: T) => T. That's a universally quantified type, not an existential one.

[masaeedu]

In general I'm not sure it makes much sense to expect this to work without having some explicit quantifier in the conditional type. There is no substitution of (a: _) => _ that is a supertype of <T>(a: T) => T (which is the type your usage of appliedF suggests you'd want the expression clone(test) to be ascribed).

If you do put in an explicit quantifier things work out nicely:

type GF = <T>(a: T) => T

declare function clone<F extends (a: any) => any>(
    fn: F
): F extends GF ? GF : never;

function test<T>(a: T): T {
  return a;
}

const appliedF: number = clone(test)(1);

Regardless, I still don't see the connection with existential types here.

[dead-claudia]

I went straight to the second snippet because I'm having a bit of a hard time wrapping my head around the first one. As far as the second one goes, I'm not sure what role we'd want existential types to play. AFAICT the problem is that:

type ConditionalTypesDontWorkWithGenerics<F> = F extends ((a: infer A) => infer R) ? (a: A) => R : never

function test<T>(a: T): T {
  return a;
}

type Result = ConditionalTypesDontWorkWithGenerics<typeof test>
// Result = (a: unknown) => unknown

Whereas you'd want Result = typeof test = <T>(a: T) => T. That's a universally quantified type, not an existential one.

@masaeedu While that's true, universal and existential quantifiers can be defined in terms of each other, not unlike de Morgan's laws, and so this would actually need to exist together with negated types. Specifically:

• To disprove a "for all T" proposition, all you need to do is find a T where the predicate doesn't hold.
• To disprove a "there exists a T" proposition, you have to show that the predicate is false for all T.

Or to put it in terms of my proposal and negated types, these two types must be equivalent:

• forall<T> Foo<T> must be equivalent to not exists<T> not Foo<T>
• exists<T> Foo<T> must be equivalent to not forall<T> not Foo<T>

And in addition, parameterization must be kept together when extracting conditional types. These three must all be equivalent:

• (<T>(a: T, b: T) => unknown) extends ((...a: infer A) => unknown) ? A : never
• Parameters<<T>(a: T, b: T) => unknown> (beta expansion of the above)
• forall<T> [a: T, b: T]

Of course, we could theoretically just do a forall, but that doesn't cover the other driving reason I created this issue (which works in the opposite direction).

Edit: fix type inconsistency

[masaeedu]

forall<T> Foo<T> must be equivalent to not exists<T> not Foo<T>

There are more constructive ways of relating these things. That said, why would we prefer to work with not exists<T> not (a: T) => T instead of just <T>(a: T) => T in the example above?

And in addition, parameterization must be kept together when extracting conditional types. These three must all be equivalent:

(<T>(a: T, b: T) => void) extends ((...a: infer A) => unknown) ? A : never

...

<T>(a: T, b: T) => void takes the form <T> F<T>, where F is contravariant. So it's equivalent to F<unknown> = (a: unknown, b: unknown) => void. And that's just what TS unifies it with: the first entry in your list evaluates to the type [a: unknown, b: unknown], which seems fine to me.

It seems like you want the substitution (...a: <T> [T, T]) => ... instead, but it's unclear to me why that's desirable. That type is equivalent to (a: never, b: never) => ... and inequivalent to <T>(a: T, b: T) => ....

[dead-claudia]

@masaeedu A better way to put it is that <T>(a: T) => T should be equivalent to forall<T> ((a: T) => T) - the generics should simply be sugar for an enclosing forall constraint. And here's how the math would work out for the previous example per my proposal here:

Step	Action	Result
1	Initial	Parameters<<T>(a: T, b: T) => unknown>
2	Desugar generic to forall	Parameters<forall<T> ((a: T, b: T) => unknown)>
3	Beta reduce	forall<T> ((a: T, b: T) => unknown) extends ((...args: infer P) => any) ? P : never
4	Desugar arguments to tuple	forall<T> ((...args: [T, T]) => unknown) extends ((...args: infer P) => any) ? P : never
5	Lift forall constraint	((...args: forall<T> [T, T]) => unknown) extends ((...args: infer P) => any) ? P : never
6	Pattern-match type	((...args: forall<T> [T, T]) => unknown) extends ((...args: infer P) => any) ? P : never where infer P = forall<T> [T, T]
7	Substitute value	((...args: forall<T> [T, T]) => unknown) extends ((...args: forall<T> [T, T]) => unknown) ? forall<T> [T, T] : never
8	Beta reduce conditional type	forall<T> [T, T]

The current math looks like this:

Step	Action	Result
1	Initial	Parameters<<T>(a: T, b: T) => unknown>
2	Beta reduce	(<T>(a: T, b: T) => unknown) extends ((...args: infer P) => any) ? P : never
3	Resolve generic to supertype	((a: unknown, b: unknown) => unknown) extends ((...args: infer P) => any) ? P : never
4	Desugar arguments to tuple	((...args: [unknown, unknown]) => unknown) extends ((...args: infer P) => any) ? P : never
5	Pattern-match type	((...args: [unknown, unknown]) => unknown) extends ((...args: infer P) => any) ? P : never where infer P = [unknown, unknown]
6	Substitute value	((...args: [unknown, unknown]) => unknown) extends ((...args: [unknown, unknown]) => unknown) ? [unknown, unknown] : never
7	Beta reduce conditional type	[unknown, unknown]

Note the difference between step 2 of each and the addition of the lifting the forall constraint step - it's subtle, but significant.

Sorry, it's hard to go into much detail without diving into type theory and mathematical logic. This gets complicated and hairy really, really fast.

Edit: Correct a couple swapped steps in the current math.

[masaeedu]

Thanks, that's much more explicit. The "Lift forall constraint" step where you turn this:

forall<T> ((...args: [T, T]) => unknown) extends ((...args: infer P) => any) ? P : never

into this:

((...args: forall<T> [T, T]) => unknown) extends ((...args: infer P) => any) ? P : never

is actually wrong. <X> ((x: X) => Whatever) is not the same type as (x: <X> X) => Whatever. The first one is equivalent to (x: unknown) => Whatever, and the second to (x: never) => Whatever.

---

As far as I'm aware, your assessment of the "current math" is also wrong, in that the unknowns for the parameters aren't introduced until we try to unify <T>(a: T, b: T) => unknown with (...args: infer P) => any in expanding the conditional type. Or at least, if you write a different conditional type, the quantification survives just fine, and it is possible to show that conditional types respect the upper bounds of quantifiers for generic function types.

But I'm less confident on this point, probably someone more familiar with the implementation can comment.

[dead-claudia]

@masaeedu I'm not a computer scientist, so I probably didn't nail everything first try. 🙃

But I will point out one thing that might have gotten missed in the shuffle:

• forall<X> X is equivalent to the top type unknown.
• exists<X> X is equivalent to the bottom type never.

I think you got confused, where I've up until this point only really referred to exists and not forall. (It's also why I started explicitly denoting the two - I'm trying to not be ambiguous in my intent.) So yes, forall<X> ((x: X) => Whatever) is equivalent to (x: forall<X> X) => Whatever and thus also to (x: unknown) => Whatever.

You are right in that I screwed up in the current math, though, and I've corrected that in my comment.

[masaeedu]

But I will point out one thing that might have gotten missed in the shuffle:

• forall<X> X is equivalent to the top type unknown.
• exists<X> X is equivalent to the bottom type never.

Unfortunately I don't think this is correct either, it's precisely the other way around. And no, forall<X> ((x: X) => Whatever) is not equivalent to (x: forall<X> X) => Whatever. You're welcome to experiment with this in other type systems with polymorphism (e.g. Haskell), or you could conduct a roughly analogous experiment in TypeScript with <T>(x: () => T) => unknown vs (x: <T>() => T) => unknown.

[dead-claudia]

I think we're both partially, but not fully correct, with you more correct than me.

declare const test1: Test1; type Test1 = <T>(x: () => T) => unknown
declare const test2: Test2; type Test2 = (x: <U>() => U) => unknown
declare const test3: Test3; type Test3 = (x: () => unknown) => unknown
declare const test4: Test4; type Test4 = (x: () => never) => unknown

// Apparent hierarchy:
// - Test1/Test3 subtypes Test2/Test4
// - Test1 is equivalent to Test3
// - Test2 is equivalent to Test4

// type Test1 = <T>(x: () => T) => unknown
// type Test2 = (x: <U>() => U) => unknown
// Result: `Test1` subtypes `Test2`
const assign_test12: Test2 = test1
const assign_test21: Test1 = test2 // error

// type Test1 = <T>(x: () => T) => unknown
// type Test3 = (x: () => unknown) => unknown
// Result: `Test1` is equivalent to `Test3`
const assign_test13: Test3 = test1
const assign_test31: Test1 = test3

// type Test1 = <T>(x: () => T) => unknown
// type Test4 = (x: () => never) => unknown
// Result: `Test1` subtypes `Test4`
const assign_test14: Test4 = test1
const assign_test41: Test1 = test4 // error

// type Test2 = (x: <U>() => U) => unknown
// type Test3 = (x: () => unknown) => unknown
// Result: `Test3` subtypes `Test2`
const assign_test23: Test3 = test2 // error
const assign_test32: Test2 = test3

// type Test2 = (x: <U>() => U) => unknown
// type Test4 = (x: () => never) => unknown
// Result: `Test2` is equivalent to `Test4`
const assign_test24: Test4 = test2
const assign_test42: Test2 = test4

// type Test3 = (x: () => unknown) => unknown
// type Test4 = (x: () => never) => unknown
// Result: `Test3` subtypes `Test4`
const assign_test34: Test4 = test3
const assign_test43: Test3 = test4 // error

It appears a reduction for the sake of conditional type matching is possible, but only from Test1/Test3 to Test2/Test4. So my reduction is sound, but I can't go in the other direction - the reduction is one-way, and it can only be done for cases where direct equivalence is irrelevant (like conditional type extraction and assignability).

[masaeedu]

I think we're both partially, but not fully correct, with you more correct than me.

Fascinating. Could you point out what I am "not fully correct" about?

[dead-claudia]

@masaeedu I'm specifically referring to the subtyping bit - you're right that they're not equivalent (thus countering almost my entire rationale), but I'm right in that it can still be reduced like that in this particular situation anyways. So essentially, I'm right about the claim it can be done, just you're right about the supporting evidence provided being largely invalid and about why it's largely invalid.

[clinuxrulz]

Workaround:

type Exists<T> = <R>(doIt: <A>(a: T<A>)=>R)=>R

That is to say, you represent the type as a callback for the visitor pattern pattern to operate on the unknown type. Unfortunately the pattern requires higher kinded types to avoid boilerplate. So you need to manually make several Exist types for each type of T.

One solid use case for the exists operator is a Properties List table holding properties of many different types each tupled with a renderer and/or editor that operates on those types.

E.g.

type Property<A> = {
  displayName: string,
  getValue: () => A,
  setValue: (a: A) => void,
  renderer: Renderer<A>,
  editor: Editor<A>,
};
type PropertyExists = <R>(doIt: <A>(a: Property<A>) => R) => R;
type PropertyList = PropertyExists[];

100% type-safe to work with. But there is boilerplate.

Using the workaround above, you can operate on the property list as follows:

function operateOnPropertyList(pl: PropertyList) {
  for (let p of pl) {
    p(operateOnProperty);
  }
}

function operateOnProperty<A>(p: Property<A>) {
  // Do stuff with it
}

Here is a syntax I would suggest if we were to have the exists keyword: type PropertyList = (<exists A>: Property<A>)[];

And the only function types that can type-safely operate on those existential types are the ones using forall.

E.g.

function operateOnPropertyList(pl: PropertyList) {
  for (let p of pl) {
    operateOnProperty(p);
  }
}

function operateOnProperty<A>(p: Property<A>) {
  // Do stuff with it
}