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>
    );

    // ...
}

[rotemdan]

Hi again :),

I'll try my best to clarify what this means (hopefully my understanding isn't flawed - at least I hope). I took a simple example as a starting point: of a generic type, and a non-generic container type. The container contains a property content which accepts a value matching any instantiation of the generic type, as long as it follows its internal "shape":

interface MyType<T> {
	a: T;
	b: T[];
}

interface Container {
	content<E>: MyType<E>
}

Of course the above doesn't currently compile, but it demonstrates another approach to a possible syntax.

The idea is that the affected property or variable is "modified" by a type parameter, which is always inferred (for the 'write' direction it is conceptually similar to a generic setter method setContent<E>(newContent: MyType<E>) where E is always inferred when called). That type parameter can be passed to any secondary generic type, or even be used to define an anonymous generic type:

interface Container {
	content<E>: {
		a: E;
		b: E[];
	}
}

One thing to note is that if no constraint is imposed over E. It can always be matched with any, meaning that perhaps surprisingly, the following might work:

const c: Container = {
	content: {
		a: 12,
		b: ["a", 6, "c"]
	}
}

Since E can be substituted with any, any type with properties a and b and where b is an array can satisfy MyType<E>.

Even if E was constrained:

interface Container {
	content<E extends number | string>: MyType<E>
}

The above example can still be matched by E = number | string (Edit: or in practice technically also E = any as well, but I was just giving that as an illustration).

Maybe what we need is an "exclusive or" type constraint, that would constrain E to be either number or string, but not the possibility of both:

interface Container {
	content<E extends number ^ string>: MyType<E>
}

const c: Container = {
	content: {
		a: 12,
		b: ["a", 6, "c"]
	}
} // <- Error this time: can't match either `number` or `string` to unify with `MyType`

Another thing to note is that the resulting container type would probably be used mostly as an abstract one, to be inherited by classes or other interfaces, or maybe serve as a constraint for type arguments. When used on its own, trying to read content would return a value whose type always falls back to its existential types' constraints.

[dead-claudia]

@rotemdan I see what you mean. That could work (provided it works for arguments, too). But how would something like this work? (My idea of type<T> Foo<T> similar to Haskell's forall a. Foo a has a similar potential issue, too.)

interface C {
  prop<T>: Array<T>;
}

let c: C = {prop: [2]}
let value = c.prop[0] // What type is this?

With the information provided, this is an opaque type AFAIK.

[rotemdan]

@isiahmeadows

My approach was just an intuitive instinct - a starting point. I can't say I'm an expert in this area but I thought it might be a meaningful contribution.

I felt it might look simple and aesthetically elegant to modify the identifier itself, though that approach still doesn't cover all possible use cases. It only covers:

Properties:

interface C {
  prop<E>: { a: E; b: E[] };
}

Variable declaration (const, let and var):

let c<E>: { a: E; b: E[] }

Function, method and constructor parameters:

function doSomething(c<E>: { a: E; b: E[] }, s: string);

interface I {
  doSomething(c<E>: { a: E; b: E[] }, s: string);
}

class C {
  constructor(c<E>: { a: E; b: E[] }, s: string);
}

This syntax doesn't provide a solution to introduce explicit existential-only type variables into other scopes like entire interfaces or classes, or functions. However since these scopes do allow for "universal" type parameters, these type parameters can be "wrapped" by existentials at the use site:

interface Example<T> {
  a: T;
}

let x<E>: Example<E>;

I'm reading about forall in Haskell (I don't think I understand it 100% at this point) and investigating the flexibility of an equivalent type <T> style syntax. I would be interested in seeing more examples for the scopes where type <T> can be used. Can it wrap arbitrary code blocks? can it wrap type aliases? entire constructors, getters and setters, etc?

[dead-claudia]

@rotemdan I'd say the easiest way to understand existentials is through Haskell's version (Haskell/etc. normally leaves it implicit). Basically, it's a lot like Scheduler<any, any>, except it still validates you're implementing Scheduler with the right internal types.

As a special case, consider polymorphic functions as an existing common special case:

// TypeScript
type Flattener = <T>(arg: T[][]) => T[];
type Flattener = type<T> (arg: T[][]) => T[];

-- Haskell's equivalent
type Flattener = [[a]] -> [a]
type Flattener = forall a. [[a]] -> [a]

[rotemdan]

• In what code positions can type<T> be used? From your examples so far it seems like it could fit in variable declarations, properties, function and constructor parameters and type aliases. What about entire interfaces, methods, constructors?

• Since TypeScript has the any type and unions like number | string. How can the compiler decide whether a literal, say { a: 1, b: [1, "x", "y", 4] } is compatible with a polymorphic type, say type <E> { a: E, b: E[] } since E can always be unified with any? (or number | string etc).

Edit: instantiation -> literal

[rotemdan]

@isiahmeadows

I apologize I forgot to answer your question about:

interface C {
  prop<T>: Array<T>;
}

let c: C = {prop: [2]}
let value = c.prop[0] // What type is this?

When I mentioned that it is "mostly useful in the write direction" I meant that in general it improves type safety only when written to. When read from, the type falls back to a supertype based on the constraint for the existential type parameter (which here is not provided, so I guess can be assumed to be T extends any). So I believe the resulting type of c.prop[0] should be any, unfortunately, unless more sophisticated flow analysis is applied (which might be able to specialize the type only for the particular variable c).

Based on what I read about 'opaque' types so far, I believe this may qualify as one.

Edit: my personal feeling about this is that it is just one more example that demonstrates the 'flakiness' of mutable variables. If all TS variables and properties were immutable, the compiler could easily keep track on the 'internal' types held within an entity bound to an existential type, since once it is first inferred, it cannot be changed anymore. Due to this and many other reasons I'm personally making an effort to come up with a plan to try to move away from mutable variables in my own programming.. ASAP :) .

[rotemdan]

I'll try to demonstrate how this can work with type inference and flow analysis:

For the type:

interface C {
  prop<E>: {
    a: E;
    b: E[];
  }
}

An instance would provide a temporary instantiation, that would be determined by type inference and flow analysis, for example, when a literal is assigned:

let x: C = {
  prop: {
    a: 12,
    b: [1, 2, 3]
  }
}

The declared type of x would remain C but the actual one would be specialized to { prop: { a: number; b: number[] } } (I'm ignoring, for now, the issues with any inference I mentioned earlier).

Trying to assign:

x.prop.b[2] = "hi";

Should fail, however, reassigning x itself with a value implying a different instantiation might work, e.g.:

x = {
  prop: {
    a: "hello",
    b: ["world"]
  }
}

If x was declared with const then the "apparent" type of x would be permanently locked to { prop: { a: number; b: number[] } }.

This is at least how I imagine it could work.

Edit: fixed code examples

---

Edit 2:

After thinking about this for a while, I'm wondering whether prop should be allowed to be reassigned with a value representing a different instantiation as well, e.g.:

x.prop = {
    a: "hello",
    b: ["world"]
}

If that would be allowed (I mean, for both the cases where x was declared as let and const), then flow analysis might need to become more sophisticated as it would need to track the change of type for 'deep' properties in the object tree of x.

[zpdDG4gta8XKpMCd]

forgive my ignorance, isn't wrapping into a closure would be a commonly accepted answer to existential types problem?

[dead-claudia]

Not in the case of declaration files, where you almost never see that.

[cameron-martin]

@isiahmeadows Surely the type of c.prop[0] in your example would be type<T> T with your proposed syntax?

[dead-claudia]

@cameron-martin

Surely the type of c.prop[0] in your example would be type<T> T with your proposed syntax?

That is the correct understanding, but it was @rotemdan's proposed syntax, not mine - I was just translating a type between the two. The main question I had was this: what is type<T> T equivalent to?

[cameron-martin]

@isiahmeadows possibly Object?

[dead-claudia]

@cameron-martin Can't be Object, since Object.create(null), an object by ES spec, should also be assignable to it, and Object.create(null) instanceof Object is false.

[pelotom]

For anyone interested in using existential types right now via the negation of universal types, the type annotation burden of doing so has been greatly reduced thanks to recent type inference improvements.

type StackOps<S, A> = {
  init(): S
  push(s: S, x: A): void
  pop(s: S): A
  size(s: S): number
}
 
type Stack<A> = <R>(go: <S>(ops: StackOps<S, A>) => R) => R

const arrayStack = <A>(): Stack<A> =>
  go => go<A[]>({
    init: () => [],
    push: (s, x) => s.push(x),
    pop: s => {
      if (s.length) return s.pop()!
      else throw Error('empty stack!')
    },
    size: s => s.length,
  })

const doStackStuff = (stack: Stack<string>) =>
  stack(({ init, push, pop, size }) => {
    const s = init()
    push(s, 'hello')
    push(s, 'world')
    push(s, 'omg')
    pop(s)
    return size(s)
  })

expect(doStackStuff(arrayStack())).toBe(2)

[cameron-martin]

@isiahmeadows I'm guessing what we're looking for here is a top type. Surely this can be build from a union of {} and all the remaining things that are not assignable to {}, e.g. {} | null | undefined.

However, it would be nice to have a top type built in.

[dead-claudia]

@cameron-martin Look here

[jack-williams]

@isiahmeadows @cameron-martin

The main question I had was this: what is type<T> T equivalent to?

The existential is only (alpha) equivalent type<T> T. You can eliminate the existential to a skolem constant T, but that will only be equivalent to itself. An existential variable is assignable, but not equivalent, to Top.

Edit: An existential is assignable -> An existential variable is assignable

[dead-claudia]

@jack-williams Yeah...I meant it as "what is the smallest non-existential type type<T> T is assignable to", not formal nominal equivalence.

[jack-williams]

Understood! By equivalence I wasn't sure if you wanted assignability in both directions.

[dead-claudia]

@jack-williams Assignability the other way (let foo: type<T> T = value as {} | null | undefined) would just be application: just let T = {} | null | undefined. (That part was implied.)

[jack-williams]

@isiahmeadows

I think I was (am) confused on the syntax, and my early comment also missed a word. It should have read:

An existential variable is assignable, but not equivalent, to Top.

I read the earlier comment:

Surely the type of c.prop[0] in your example would be type<T> T with your proposed syntax?

and starting parsing type<T> T as just a variable, but the syntax should really mean exists T. T.

In that sense what I intend is: c.prop[0] should be type T and not type <T> T, and that T is assignable to Top but not the other way round.

When you write: let foo: type<T> T = value as {} | null | undefined) and mean that type <T> T is equivalent to Top then I agree.

TLDR; I agree that type<T> T is equivalent to top, but c.prop[0] would have type T, not type<T> T. I got muddled on syntax.

Apologies for confusion.

[cameron-martin]

In that sense what I intend is: c.prop[0] should be type T and not type <T> T, and that T is assignable to Top but not the other way round.

@jack-williams I don't see how it could be T - there is no T in scope at this point.

[dead-claudia]

@jack-williams Edit: Clean this up so it's a little easier to digest.

1. I mean "structurally equivalent" in that both are assignable to each other, if that helps:

   type unknown = {} | null | undefined
   declare const source: any
   declare function consume<T>(value: T): void
   
   // Both of these check iff they are structurally equivalent
   consume<type<T> T>(source as unknown)
   consume<unknown>(source as type<T> T)

2. type<T> T is supposed to be "forall T. T", not exists T. T. True existentially quantified types would be essentially opaque, and there's not really a lot of use for that IMHO when unknown and the proposed nominal types would address 99% of use cases existentially quantified types could solve.

3. To clear up any remaining confusion regarding the syntax:

   • My proposal is adding a type<T> T as a type expression.
   • @rotemdan proposed here to instead use prop<T>: T as an object/interface property.
   • See my next comment for explanation on how these compare.

(I kind of followed the common miswording of "existential" instead of "universal", when it's really the latter. Not really something specific to TS - I've seen it in Haskell circles, too.)

[dead-claudia]

@cameron-martin (re: this comment)

interface C {
  // @rotemdan's proposal
  prop<T>: T[];
  // My proposal
  prop: type<T> T[];
}

let c: C = {prop: [2]}
let value = c.prop[0] // What type is this?

Just thought I'd catch you out on this one and point out that c.prop itself is the quantified type, not members of it.

[jack-williams]

@cameron-martin : As @isiahmeadows says, the type of prop is quantified over. To access the array to you need to eliminate the quantifier, doing this introduces a fresh, rigid type variable T.

@isiahmeadows If type <T> T denotes forall then should that not be equivalent to bottom? My understanding was that forall T. T is the intersection of all types, and exists T. T was the union. What is the difference between 'true existential types' and the existential-like types that you get from the forall encoding?

[dead-claudia]

@jack-williams

My understanding was that forall T. T is the intersection of all types, and exists T. T was the union.

Wait...you're correct. I got my terminology crossed up.

• forall T. T could be assigned to any type T, as it would just happen to be a particular specialization of it. (This makes it equivalent to never.)
• Any type could be assigned to exists T. T, as it would just specialize that type for that particular type. (This makes it equivalent to {} | null | undefined.)

Either way, you can still define that exists T. T in terms of forall T. T, using forall r. (forall a. a -> r) -> r, where a is existentially qualified. In my syntax, it'd look like this: type <R> (x: type <A> (a: A) => R) => R.

---

Note that for many cases, this is already possible in conditional types, where an infer keyword operator enables the common need to extract a return value from a function, like in here (which will become a predefined global type):

type ReturnType<T extends (...args: any[]) => any> =
    T extends (...args: any[]) => infer R ? R : any

[masaeedu]

@cwohlman Is this perhaps what you want?

type Job<T, R> = { isJob(param: unknown): param is T, run(param: T): R }

// Just moved the quantification out here
class JobsHandler<T, R> {
    jobs: Job<T, R>[] = []
    runJob(thing: T): R {
        const job = this.jobs.find(job => job.isJob(thing));
        if (!job) {
            throw new Error('No job')
        }
        return job.run(thing);
    }
    addJob(job: Job<T, R>) {
        this.jobs.push(job)
    }
}

[dead-claudia]

@cwohlman Your guard is off. It needs to constrain the job, not the parameter directly.

(Using exists here (as in "there exists") to also better clarify where the existentials are for everyone else, though of course, I'm not tied to any particular syntax provided it's not too verbose.)

interface Job<T, R> {
  isJob<U extends T>(param: U): this is Job<U, R>;
  run(param: T): R;
}
class JobsHandler {
  jobs: Array<exists <T, R> Job<T, R>> = []
  runJob<T, R>(thing: T): R {
    // Avoid a type check issue by using a loop with TS's narrowing rather than
    // `.find`, because TS isn't quite *that* intelligent.
    for (const job of this.jobs) {
      if (job.isJob(thing)) return job.run(thing)
    }
    throw new Error('No job')
  }
  addJob<T, R>(job: Job<T, R>) {
      this.jobs.push(job)
  }
}

@masaeedu The existential is needed if you want to make it fully generic - @cwohlman just elided it (either erroneously assuming broader familiarity with languages like Haskell or just by mistake is my guess).

[masaeedu]

@isiahmeadows Could you expand on what you mean by "fully generic"?

I was looking at the snippet above, and exists <T, R> Job<T, R> suggests that it is impossible to call the run method of any job in that array, and impossible to do anything with the result were we able to call it. I'm not sure why we'd want that, but if we do, we can also get it with Job<never, unknown>.

[dead-claudia]

@masaeedu I think you're conflating top/bottom types with existential quantifiers. (Wikipedia link if you want to read a little more on the math behind it) While yes, something like forall t: t is equivalent to the bottom type (as it satisfies everything) and exists t: t is equivalent to the top type (as it satisfies nothing but itself), that's only a very small subset of what existential and universal types can do.

In this case, now that I look closely and think more about the existentials in question, you could use never and unknown for this, but it moderately complicates it in this case (existentials almost trivialize it when put in the right places) and this isn't always the case in general - see my initial issue comment for an example. Another example is Mithril's object components that happen to be polymorphic - there's no function to bind type parameters to (which mathematically speaking are technically existentials as well), but you still need an existential somewhere in the mix.

Here's that code snippet with existentials removed.

interface Job<T, R> {
  // Return type is conditional as we want to break if the type hierarchy
  // isn't correct.
  isJob<T, S>(param: T): this is Job<T, R extends S ? S : unknown>;
  run(param: T): R;
}
class JobsHandler {
  jobs: Job<never, unknown> = []
  runJob<T, R>(thing: T): R {
    for (const job of this.jobs) {
      // Extra type parameters to explicitly select the return value we want
      if (job.isJob<T, R>(thing)) return job.run(thing)
    }
    throw new Error('No job')
  }
  addJob<T, R>(job: Job<T, R>) {
      this.jobs.push(job)
  }
}

[masaeedu]

While yes, something like forall t: t is equivalent to the bottom type (as it satisfies everything) and exists t: t is equivalent to the top type (as it satisfies nothing but itself)

We don't really need to be quite so modest with this claim. For any covariant functor F, exists X. F<X> is equivalent to F<unknown>, and forall x. F<X> is equivalent to F<never>. For a contravariant functor F, the situation is reversed: exists X. F<X> is equivalent to F<never>, and forall X. F<X> is equivalent to F<unknown>.

[masaeedu]

this isn't always the case in general - see my initial issue comment for an example.

Your original example is a bit large so I haven't read all of it, but at a skim Scheduler appears to be covariant in the positions you've marked as any, and so is susceptible to the same approach.

Instead of a hypothetical:

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

type Scheduler<Frame, Idle> = exists T. SchedulerT<Frame, Idle, T>

You can use:

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

EDIT: Ah, I just realized it's probably Frame and Idle that you want to existentially quantify over, I misunderstood the intent behind "(and any doesn't cover this)". If that's the case, yes, this doesn't degenerate to top and bottom types, since Scheduler is invariant in both parameters.

[masaeedu]

You can however use a binary version of the existentials-by-way-of-universals approach, which looks like this:

interface hkt2eval<a, b> { }

type hkt2 = keyof hkt2eval<unknown, unknown>

type exists2<f extends hkt2> = <r>(f: <a, b>(fe: hkt2eval<a, b>[f]) => r) => r

type some2 = <f extends hkt2>(k: f) => <a, b>(fab: hkt2eval<a, b>[f]) => exists2<f>
const some2: some2 = _ => fa => k => k(fa)

For your use case:

interface hkt2eval<a, b> {
    Scheduler: {
        nextFrame(func: () => any): a;
        cancelFrame(frame: a): void;
        nextIdle(func: () => any): b;
        cancelIdle(frame: b): void;
        nextTick(func: () => any): void;
    }
}

const myScheduler = some2('Scheduler')({
    nextFrame: () => 'foo',
    cancelFrame: s => {
        // s is known to be a string in here
        console.log(s.length)
    },

    nextIdle: () => 21,
    cancelIdle: n => {
        // n is known to be a number in here
        console.log(n + 21)
    },

    nextTick: () => { }
})

const result = myScheduler(({ nextFrame, cancelFrame, nextIdle, cancelIdle, nextTick }) => {
    const a = nextFrame(() => { })

    // `a` is not known to be a string in here
    console.log(s.length) // error

    // we can pass `a` into `cancelFrame` though (that's about all we can do with it)
    cancelFrame(a)

    // the argument of `cancelFrame` is not known to be a string
    cancelFrame('foo') // error
})

Playground link

[dead-claudia]

@masaeedu There's also Binding<T>, a different invariant type. And for Mithril (a much more real-world use case), object components (and really also closure component instances) should really be typed as exists<State> Component<Attrs, State> to be typed correctly. Code like this is generally invalid as state isn't checked for compatibility, and neither never nor unknown properly encapsulate the needed constraints:

// Mithril-related definition
import m from "mithril"
type ObjectComponent<Attrs> = m.Component<Attrs, unknown>

interface Attrs { C: ObjectComponent<this> }
interface State { n: number }

export const ProxyComp: m.Component<Attrs, State> = {
  // The only thing correct about this is `this.n = 1`. The rest will erroneously check.
  oninit(vnode) { this.n = 1; vnode.attrs.C.oninit?.call(this, vnode) },
  oncreate(vnode) { vnode.attrs.C.oncreate?.call(this, vnode) },
  onbeforeupdate(vnode, old) { return vnode.attrs.C.onbeforeupdate?.call(this, vnode, old) },
  onupdate(vnode) { vnode.attrs.C.onupdate?.call(this, vnode) },
  onbeforeremove(vnode) { return vnode.attrs.C.onbeforeremove?.call(this, vnode) },
  onremove(vnode) { vnode.attrs.C.onremove?.call(this, vnode) },
  view(vnode) { return vnode.attrs.C.view.call(this, vnode) },
}

Playground Link

While yes, valid types could be used to properly type Comp, you don't get the needed type errors from doing it the above way - you have to have existentials to correctly reject the above invalid code. In effect, it allows you to enforce better soundness in a lot of cases where you would otherwise use unknown or never, and an important part of verification is knowing it will tell you you're wrong when you're wrong.

Edit: And just to be clear, this is a case where exists<T> F<T, U> is not equivalent to either F<unknown, T> or F<never, T> - in reality you could type it as never, but as State above isn't assignable to never, that makes it impossible to type using that. And of course, unknown is explained sufficiently well above.

[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
}