DEV Community: Max Heiber

Function Intersection Types Considered Surprising

Max Heiber — Sat, 23 Jan 2021 19:39:29 +0000

Function intersection types sound simple, but get less intuitive the deeper one looks.

Each of the following surprised me, and has its own section in this post:

When "or" means "intersection"
Applying an Intersection
What Erlang Does
What TypeScript Does

If you're short on time, skip to the last section, since what TypeScript does is most interesting.

Key:

& is intersection
| is union
x: T is a variable x of type T
'a1' in a type means a singleton type inhabited by only the value 'a1'.

When "or" means "intersection"

Here's an Erlang function that:

given an 'a1' returns 'r1'
given an 'a2' returns 'r2'

Mnemonic: "a" for "argument", "r" for "return"

func('a1') -> 'r1';
func('a2') -> 'r2'.

We can give it a type specification like this:

-spec func('a1') -> 'r1'; ('a2') -> 'r2'.
func('a1') -> 'r1';
func('a2') -> 'r2'.

If you ask someone whether ; means "union" or "intersection" here, they are very likely to say "union." I made this mistake, too. There seems to be "or" reasoning going on: either the first function cluase is used, or the second is used.

But here are some reasons for thinking the function is not a union: in general, one cannot use a union of T and U in a way that takes advantage of its T-ness without first proving that it is a T. Here's a TypeScript example, if I have a variable x of type number | string[], I can't do much with it until I figure out what it is. I have to do something like if (Array.isArray(x)) { /* now I can treat x as an array }. If I have a y of type number[] | string[] I can safely use y.concat because that doesn't take advantage of y's number[]-ness or string[]-ness, it uses a method that's defined for both branches of the union.

So func is an intersection, not a union, otherwise we wouldn't be able to call it on a1 without first proving that the function isn't defined on a2.

See how intuitive this is? It gets better!

Applying an Intersection

Ideally, a type checker will be able to figure out the type of an expression like f(x) based on the type of f and the type of x.

The typical rule for this sort of thing is:

x: T  and f: T -> U
-------
f(x): U

That is, "The type of f(x) is the return type of f, assuming x has the same type as f's parameter."

But the type of func above is the intersection of 'a1' -> 'r1' and 'a2' -> 'r2', which doesn't clearly tell us what to do when applying the function: it doesn't have the same shape as T -> U in our function application rule.

One can make an argument for massaging the type of func into the slightly surprising:

('a1' | 'b1') -> ('r1' & 'r2')

Or, more generally:

F1: A1 -> R1
F2: A2 -> R2
----------
(F1 & F2): (A1 | A2) -> (R1 & R2)

That is: "The type of a function intersection is a function type from the union of the parameter types to the intersection of the return types"

I'll show how the function intersection rule above is sensible, then show how it's not.

Some theoretical reasons for liking this rule are:

For any types T and U, both T and U should be subtypes of T & U. Then rule above is the only one that fits. This explanation is all you need if variance is super-intuitive to you and you remember that functions are contravariant in their inputs and covariant in their outputs.
Think of a function as like a burrito maker. Suppose my birthday is coming up and I ask you for a machine that accepts flour and turns it into burritos. And you give me a machine that can turn either flour or corn into things that are both burritos and delicious. Then I get what I wanted for my birthday, a strained metaphor.

To make things more concrete, the signature does the right thing for examples like the following. Given a spec:

-spec f('a') -> 1 | 2 | 3
      ;('b') -> 2 | 3.

Then the rule allows the following example implementation of function f:

f(a) -> 2;
f(b) -> 3.

At this point, I hope something still seems fishy.

Intersecting the return types is weird!! What was the point of having the left side of the intersection in the spec say the function could return 1 if it can't actually return 1?

Put differently, the rule for how to intersect function types makes one wonder why one would bother writing specs with functions intersections at all. By the rule above, the spec for f has the same meaning as this much simpler spec:

-spec f('a' | 'b') -> 2 | 3.

The rule for function intersections also seems to say the wrong thing about cases like our original example:

-spec func('a1') -> 'r1'; ('a2') -> 'r2'.
func('a1') -> 'r1';
func('a2') -> 'r2'.

The function intersection rule says that the function above is ('a1' | 'a2') -> ('r1' & 'r2'). But what on Earth is an 'r1' & 'r2'? Neither Erlang nor TypeScript has any values of type 'r1' & 'r2'.

Perhaps the spec for func doesn't need massaging into T -> U form. Instead, we can tweak the function application rule, splitting it into two:

Rule 1

f: (A1 -> R1) & (A2 -> R2)
x: A1
-------------
f(x): R1

Rule 2

f: (A1 -> R1) & (A2 -> R2)
x: A2
-------------
f(x): R2

That is, in order to calculate the return type of a function F applied to argument x, use the branch of the intersection with a parameter that matches the type of x. Put more verbosely:

if the type of x matches the parameter type of the left side of the function intersection, the return type of the function application is the return type of the left side of the function intersection
if the type of x matches the parameter type of the right side of the function intersection, the return type of the function application is the return type of the right side of the function intersection

This is a bit annoying in the implementation of the type checker, but a deeper problem is that we haven't yet said what to do when both of our new function application rules match. What happens when A1 and A2 overlap? I'll say more about this in the next section.

What Erlang Does

The de-facto type-checker-like tool for Erlang is Dialyzer. Erlang has very clear runtime semantics for functions with multiple heads like func and f above: go through them one by one, using the first function head that matches. But it turns out that Dialyzer doesn't care about the order of function types in an intersection type!

Nor does Dialyzer take the other option we discussed above of unioning the parameter types and intersecting the return types. Dialyzer does something closer to:

F1: A1 -> R1
F2: A2 -> R2
---------------
(F1 & F2): (A1 & A2) -> (R1 & R2)

You might wonder why Dialyzer takes the intersection of the parameter types rather than the union. There's a long answer I don't have space for here, but part of the story is that Dialyzer is more of a bug-finder (or discrepancy analyzer) than a type checker, so its rules are intentionally unsound.

This description is misleading, see Update 2.

What TypeScript Does

Here is our original example, translated to TypeScript:

declare const func:  ((arg: 'a1') => 'r1')
                   & ((arg: 'a2') => 'r2')

const x = func('a1') // type of `x` is 'r1'
const y = func('a1') // type of `y` is 'r2'

playground link

TypeScript function intersections are handled like in our Rule 1 and Rule 2: when applying a function intersection to x, pick the branch of the intersection with a parameter that matches the type of x. That's how TS is able to assign different types to x and y.

The interesting bit is that TypeScript designers had to make a choice about what happens when the parameter types of F1 and F2 overlap. Options include:

Try Rule 1 and Rule 2 in order, applying the first rule that matches
OR reject outright attempts to intersect functions with overlapping domains

The first option sounds OK at first, but it has the really surprising consequence that A & B is not equivalent to B & A. These are noncommutative intersections!

The second option sounds great, but would not be practical for TypeScript. That's because TypeScript can't generally tell, for a given x: T and y: U whether or not the x is also a U.

TypeScript makes a really interesting choice here. TS intersections both are and are not commutative! TypeScript plays fast and loose with equality, which is unsound (issue #42204), but seems to work OK in practice.

On Subtyping vs. Row Polymorphism, information loss, and actionable error messages

Max Heiber — Fri, 11 Dec 2020 17:52:17 +0000

Brian McKenna's "Row Polymorphism Isn't Subtyping" is about the distinction between row polymorphism and subtyping. Several re-readings led me to convince myself I understood, then a real-world bug to lead me to a stronger conclusion on why the distinction matters.

To help cement my understanding or misunderstanding, I'll

say more about how row polymorphism isn't subtyping.
share an example of how the information loss from subtyping can lead to hard-to-diagnose bugs

Note: Good background easy reads: TypeScript's subtyping and Elm's extensible records (row polymorphism lite).

How exactly Row Polymorphism is not Subtyping

If I interpret McKenna correctly, he's saying that all and only type systems with subtyping have the subsumption rule, which says that if T1 is a subtype of T2 and e is a T1 then e is also a T2:

Subsumption Rule


e has type T1 and T1 subtype of T2
---------therefore
e has type T2

or, using more symbols:

e: T1 and T1 <: T2
--------
e: T2

Note: Technically, I think it's a rule schema and not a rule, but I'll be sloppy

It took me some time to see how row polymorphism isn't just the <: in this rule.

I'll follow Elm and use {rowvar | a: Int, b: String} to mean "a record with at least fields a: Int and b: String. rowvar is the row variable: it stands for the other fields in the record in addition to a and b. More generally: {rowvar | k1: F1, ... kn: Fn} means "Record with at least fields k1 of type F1, k2 of type F2, etc."

It seems we can define <: (subtype of) in terms of row variables.

when T1 is {rho1 | k1: F1, ... kn: Fn, ln: Gn ...}
and  T2 is {rho2 | k1: F1, ... kn: Fn}

then T1 <: T2  (T1 is a subtype of T2)

But then the subsumption rule still doesn't follow:

Subsumption Rule

e: T1 and T1 <: T2
----------------
e: T2

The extra work the subsumption rule is doing over rules for row polymorphism (which I did not write down) is that the subsumption rule allows an expression to have more than one type: e1 is both a T1 and a T2. What makes this interesting is that information is lost: when we see that something is a T2, we don't know whether it is also a T1.

But with row polymorphism, the row variables maintain the information that would be lost with subtyping. What I did above in defining <: in terms of row polymorphism sneakily ditched the row variable, which had the information about the other fields. Here's what happens if we don't sneak, and try to write something similar to the subsumption rule directly using row variables:

e1: T1
T1 is {rho1 | e1: F1, ... en: Fn, ep: Fp}
T2 is {rho2 | e1: F1, ... en: Fn}
rho2 is (rho1 | ep: Fp)
---------------------
e1: T2

The made-up syntax in the last premise is meant to say that rho2 has all the same fields (with the same types) as rho1 and additionally has field ep of type Fp

The above rule is useless because the conclusion is the same as the first premise: e1 has only one type since T1 and T2 are the same type. The type is just written differently in the second and third premises. When I wrote T1, I listed field ep explicitly, but when I wrote T2, field ep was included in the row variable rho2.

All this is to say that if one squints at the subsumption rule one might convince oneself it applies to row polymorphism, but one would be incorrect.

Note that the information loss with subtyping can be optional. In popular languages with subtyping, the information can be retained but requires more keyboarding. Here is a TS example of essentially treating subtyping like it's row polymorphism: function foo<A extends B>(a: A): A

The Perils of Information Loss

The information loss caused by the subsumption rule does not play well with type inference. Which doesn't worry me much, since type signatures are useful documentation).

A real-world bug I saw illustrates what I take to be a deeper issue with the information loss:

interface Animal {
    tasty: true
}

interface Cow extends Animal {
    moo: string
}

function getFromBarn(): Animal {
    const cow: Cow = {
        tasty: true,
        moo: "mooooo",
    }
    return cow
}

function speak(cow: Cow): void {
    console.log(cow.moo)
}

function main() {
    const cow = getFromBarn()
    speak(cow) // Error! Expected Cow but got Animal
}

Try the code

Note: I sacrificed realism in trimming down the example

What makes this bug interesting to me is that the type checker complains, even though:

All the type annotations are correct
The code is correct

This stinks! There are several related issues:

As an advocate of static type checking, I think we should be rewarded for writing type annotations. But there is little payoff in this case, only more work.
To n00b eyes, the error message is confusing: the function expects a cow and we gave it a cow. And cows are animals, but it's complaining.
Even to expert eyes, it's not clear how to fix the code. Should we change the getFromBarn(), main(), or speak()? It depends on the intent of the authors of each of these three functions, and how we want the codebase to evolve.

I don't know of an easy way out of the information loss problem with subtyping. Some routes:

In this particular case, a really advanced compiler could point out the information loss in getFromBarn() and say that just changing the annotation will make the problem go away, if the dev is sure that's what they want. But this won't be feasible in general.
Tweak the subsumption rule so that information loss is opt-in only: users must explicitly say they are upcasting a Cow to an Animal. Which adds yet more work for the user.

One answer I don't think is right is "Use row polymorphism instead" as the techniques are not directly comparable:

Subtyping is more general than just records, it is also useful for working with, for example, literal types and union types.
The information loss with subtyping can sometimes be desirable in order to hide implementation details so we can evolve our APIs: for example, exposing something as an Iterable so we can switch from Set to Array in future. Maybe that's what the author of getFromBarn() had in mind.

The Principle of Explosion in Ordinary Computer Programs

Max Heiber — Sat, 05 Dec 2020 15:55:11 +0000

There's normally a tight connection between programming and proving: this is known as "Propositions as Types." I found one aspect of the correspondence troubling, went down a rabbit hole, and came back less troubled.

Our most popular logical systems all include exfalso, a.k.a. The Principle of Explosion which is the principle that a contradiction implies anything at all. That is, forall B, if false then B.Which seems really surprising on the face of it: where did B come from?! I'll share my exploration of this question and an attempt at an answer.

Warning: There's nothing practical in this post.

Exfalso is easily derived in classical logic, the logic we're taught in school if we learn any logic at all. In classical logic, A -> B means (not A) or B. In classical logic, this is true by definition because if false then B means (not false) or B, which is just true regardless of what B is.

What was unclear to me was where exfalso comes from in the logic that corresponds to computation* (intuitionistic logic). It's almost a secret that exfalso is assumed in intuitionistic logic, without proof. But both intuitionists and our programming languages seem to quietly believe exfalso:

// exfalso in TypeScript is a function
// from a contradiction to anything at all
function exfalso<T>(contradiction: never): T {
    return contradiction;
}

*Note: I'm exaggerating a bit in calling intuitionistic logic the logic of computation. It's closest to how most of our programming languages seem to work most of the time. See Linear Logic: The resource interpretation and "A Formulae-as-Types Notion of Control for aspects of computation that other logics model better._

Background on Intuitionistic Logic and Programming

From a programmer's point of view, classical logic works for booleans, but otherwise rarely has much to do with our craft. That's because classical logic assumes something we cannot compute: the law of excluded middle (or an equivalent axiom), which is forall A, A or not A (each thing we can say is either true or false).

To show why assuming the Law of Excluded Middle doesn't accurately describe computation, consider this TypeScript function:

function foo(thing: Thing): number | string {
    ...
}

The type signature says that this function will return either a number OR a string. But at runtime there is no such thing as an instance of number | string that is not specifically a number or a string. In both programming and intuitionistic logic, in order to construct an instance of "number or string" we must have a number or have a string.

The correspondence with computation makes intuitionistic logic really attractive (at least to me), and this logic underlies some of our most cutting-edge programming languages (Coq, Agda, Idris).

Next I'll share where exfalso comes from in intuitionistic logic, the relationship to programming, and why everything is probably OK.

Exfalso in Intuitionistic Logic and Programming

If intuitionistic logic is the logic of what is programmable, then it's pretty strange that it says that in certain situations we can get any value we like for free (exfalso).

It wasn't obvious to me from Wikipedia or The Stanford Encyclopedia of Philosophy, but exfalso is assumed by intuitionistic logic. This is in contrast to classical logic, where exfalso is derivable. So it seems intuitionists (who assume very little) intentionally committed to this surprising principle.

To try to figure out why, I looked at what early intuitionists had to say about exfalso. Note that intuitionism came before computers, so the inventors of intuitionism did not think about it as the logic of computation, but had similar interpretations:

The logic where one judges what is constructable (Brouwer)
The logic where one finds a method of fulfilling/realizing an intention (Heyting)
The logic where one finds a method of solving a task (Kolmogorov)

Source: "Intuitionistic Type Theory" (Martin-Löf, 1980)

Brouwer basically said nothing about exfalso, but relied on it implicitly.

Heyting subtly qualified his view of implication to include the commitment to exfalso, selling this qualification as "adding precision":

As a matter of fact [exfalso] adds to the precision of the definition of implication. You remember that P → Q can be asserted if and only if we possess a construction which, joined to the construction of P would prove Q. Now suppose that ⊢ ¬P, that is, we have deduced a contradiction from the supposition that that P were carried out. Then, in a sense, this can be considered as a construction, which, joined to a proof of P (which cannot exist) leads to a proof of Q. I shall interpret then implication in this wider sense. (from "Intuitionism, an Introduction", Heyting)

Kolmogorov, to my ears at least, is clearer on the topic of exfalso:

As far as [exfalso] is concerned, as soon as [not A] is solved, the solution of A is impossible, and the problem of "A -> B" has no content. ... the proof that a problem is without content will always be considered as its solution.

Kolmogorov is not saying that a contradiction implies anything. Instead, he's saying that we can safely pretend it does. Morally, this feels like a significant difference to me: exfalso is imagination run wild, but saying we don't have any particular obligations in impossible situations sounds reasonable. However, in formal systems as well as programming, I have a tough time seeing what the difference would be between pretending exfalso and believing exfalso.

Take the following TypeScript example, noting that in programming contradiction can be thought of as unreachable code:

function example(bool: boolean): string {
    switch (bool) {
        case false:
            return "false";
        case true:
            return "true";
        default:
            // unreachable
            return bool;
    }
}

Check out the default case. If bool is of type boolean, why does TS let us treat it as having type string?

To see what's going on, try putting your mouse over bool in the last return statement in the TypeScript playground. TypeScript reports that bool is of type never on that line. never is TypeScript's name for "contradiction." Even though booleans are not numbers, you can return bool in the default case because the type checker knows that the default case is unreachable.

To me, the choice made by TS and other programming languages here helps clarify intuitionistic logic. It's not like when a contradiction is reached a genie appears, ready to grant any wish. Instead, we have no particular obligation with regard to our return types in unreachable parts of our programs. I think this gibes with what Kolmogorov was talking about when he said "the problem has no content" in cases of contradiction. "unreachable code" ~= "problem with no content."

The Heyting and Kolmogorov quotes and interpretation of them are from van Dalen's "Kolmogorov and Brouwer on constructive implication and the Ex Falso Rule"

What Makes a DSL Bad? Make, CSS, and how we can do better.

Max Heiber — Sat, 28 Nov 2020 16:29:40 +0000

There are many places where you can find arguments that DSLs (domain-specific languages) or "language oriented programming" are good. But I haven't found much on what makes them bad.

My experiences with DSLs tend to be negative. There are cases where I know exactly what I want the computer to do. I could write it in minutes in any "real" programming language, but struggle to express or approximate it in the DSL.

Here are some examples of "bad" DSLs:

Make
CSS
GitHub Actions

And here are sufficient conditions for a DSL to be bad:

Missing proper functions. By which I mean high school math functions: things that compute by turning variables into return values.
Missing proper variables. By which I mean a scoped way of naming values.
Mandatory. Regexes within a normal programming language are fine most of the time because we're not forced to use them: when things get too hard to express we can switch to writing a normal function with the full power of the programming language.

Honorable mention for a feature missing from bad DSLs: structured data.

On Make:

The Makefile DSL is mandatory for Make. You can't find out that you need a variable and function and then just do it. You have to trick Make with environment variables, or stitching together shell scripts, storing state on the file system, more and more complicated funny symbols, etc. etc. Here's an example where I needed variables and functions recently: our 'test' rule depended on our 'build' rule, but we had more than one way of building. We wanted to run the same tests for each of these different ways of building. I managed to hack around this: having the makefile re-invoke itself with an environment variable, then using that environment variable as a macro together with Makefile ternary conditional syntax. That's just silly!

On CSS:

In a stylesheet, CSS is mandatory: you can't nip out and write code in a real language, unless you count Houdini. CSS doesn't have variables and functions. Which is why in typical hand-written CSS, one repeats oneself a lot, with "magic strings" for widths, fonts, etc. The only methods of composition are to repeat yourself or rely on the cascade, which has all of the flavor of shared mutable state, such as action at a distance/no way to reason locally.

To see what CSS would look like if it had proper variables and functions, see how React Native does it: styles are just data, and can be assigned to variables, passed to functions, returned from functions, imported, distributed via package managers, etc.

There may be good performance reasons for not always executing a full-fledged programming language at runtime to style webpages. But then maybe instead of a limited language, there shouldn't be any language at all for styles: just data that is generated by ahead-of-time compilers.

If there's a perf argument for not having functions and variables in CSS, surely we can apply the same reasoning to CSS rule resolution. Rule resolution is hard work, maybe it's a bad idea for us to make browsers do it at runtime.
Most PLs without variables are doomed to eventually grow butchered variables. In CSS' case, it has at least two: custom properties and counters. The latter link goes to an entire article on how to number paragraphs with CSS. It's really an entire article showing you how to do the equivalent of this JavaScript: paragraphs.forEach((paragraph, i) => ....). (Note: the article is great, CSS is the target of my cricisism).
Even with all the power to crash the browser with var and calc, accidental Turing-completeness, ad-hockery (media query syntax, counters, more to come) it turns out people still want to style the browser using languages that have variables and functions (see SASS and CSS-in-JS).

On GitHub Actions:

In GitHub workflows, one very often has repeated names for things (such as an artifact one wants to generate and upload). One must copy and paste and then hope things are in sync. Or suppose one wants to do similar, but slightly different, things on pushing to a branch and on making a release. Copy/paste again, this time making several small tweaks to different steps.

Why do Bad DSLs happen to Good people?

If it's so awful working with these DSLs, then how and why did we get into this situation? The answer is a little different in each of these cases:

Why the Make language exists

I suspect Make has a DSL because high-level composable scripting languages weren't such a thing then. And if there were, it would be non-obvious how to mix the genuinely declarative aspects of Make with the "do this and then do that" nature of idiomatic Python. Rake seems to strike a nice balance here, though I haven't used it much. It's the mandatoriness that's the problem with Make, not the fundamental model.

Why CSS exists:

CSS: People are so used to CSS that it's hard to imagine alternatives, preprocessors aside. "The Languages which Almost Became CSS" gives some idea of constraints and alternatives. It was mainly for performance reasons that we didn't get a "real" programming language. That's fine, but it tells me that CSS makes more sense as a data format or bytecode than something for humans. See "What about SQL" below for more on what I mean here.

Why the GitHub Actions language exists:

GitHub actions are broken for no technical reason I can discern. They didn't butcher the language for performance reasons: You can write an infinite loop in a workflow with a "run" step with some Bash while true; do echo hello; done. You can waste memory and CPU all you want: GH will charge you for what you use, once you've exceeded the limits of the free tier. It's not for security reasons: Everything is sandboxed anyway, and is already side-effecty.

What about SQL?

SQL is pretty good in practice, but meets my definition of a "bad" DSL. The reason SQL doesn't seem totally broken is that it is typically generated, not hand-written. SQL is stitched together by code in real programming languages. For example, programmers of general-purpose languages write functions that generate and execute prepared statements. Parameters of functions in the general purpose language to bind parameters to the prepared statement. Or people use query builders or ORMs.

SQL could be better, of course, and I'm not just talking about all the syntactic inconsistencies. As a compile target, ideally it would be better-suited to being generated. Rethnkdb and MongoDB (in spite of its other faults) both get this right, treating queries more as data than as code in some butchered language without proper variables and functions, making query-building more composable and safe.

In the rare cases where apps are written in SQL, it's not really SQL, it's SQL+, where one has variables and functions: see the stored procedure languages for Postgres and SQL Server, which are particularly like real languages.

How can we do better?

Here are some alternatives to bad DSLs:

What's so bad about a real programming language with proper variables and functions? If your reasons are that you want something easy to learn and safe to embed, consider something like Lua. Lua seems to work well for Redis stored procedures, the video game industry (see Roblox for an example), Nginx config, etc. Guile is a similar option for audiences parentheses-sympathetic.
Would plain data meet your needs?
- Consider making it easy for app devs to write "real" code that generates the data, rather than providing them with a broken language that is somewhere between data and code.
  - eslint and webpack both enable users to write their config in either JSON or JS code that generates JSON-like objects. This has some of the benfits of a DSL, while enabling abstraction when it is needed.
  - If one wants static guarantees about the data generated by code, one can go a lot further in refining the code-that-generates-data approach (disclosure: I currently work at the company behind that paper, opinions are my own).
- If there are strong reasons to control side-effects and enforce limited modes of indirection, consider Dhall, if your audience is ML-syntax-sympathetic
As soon as you find yourself reinventing variables, loops, and functions with your "plain data" STOP STOP and consider one of the alternatives above. It isn't plain data anymore, it's a bad programming language.

May our tools be bicycles for the mind.

Update: I rewrote the section on CSS in response to feedback.

The Type of a `type` in Typescript

Max Heiber — Mon, 16 Mar 2020 21:42:16 +0000

I'll present four puzzles and two solutions about TypeScript classes and types.

The cover image is from another article.

These are just puzzles I find fun, but reading this might have the happy side effect of getting you out of a TS jam in the future. All four puzzles have come up in real-life situations that I've been asked about.

Puzzle 1

TypeScript has a neat feature, type-level typeof. It's probably inspired by the distinct value-level JS feature also called typeof:

typeof null;       // "object" 
typeof class A {}; // "function"

TypeScript's type-level typeof thing gives you an alias for the type of the variable thing:

const thing = 3 * 2;
type Num = typeof thing;

const y: Num = 1; // OK

But what is the type of Num?

type TypeType = typeof Num; // error: 'Num' only refers to a type, but is being used as a value here

TypeScript won't even let us ask the question.

Coq, Agda, and Idris all let you ask this type of question, but it is un-askable in TypeScript.

So we've disovered this rule: in TS, types don't have types. Fair enough. So what's going on in the following example?

class A {}
const a: A = new A();
type AType = typeof A;

The second line shows us that A is a type (we are using it to say that a is of type A).
Then the third line shows us that we can take the type of A. So it looks like we've taken the type of a type!

Puzzle 1 is: "How can types both have and not have types in TypeScript?

Puzzle 2

Puzzle 2 is: How can AA be both equal and not equal to A below?

type AA = A;
// if AA and A really are the same type,
// then we'd expect them to behave the same way
type works = typeof A;        // OK
type doesNotWork = typeof AA; // Error

When reading the example above, bear in mind the principle of Identity of Indiscernables. If A and AA really are equal, then we'd expect to be able to use AA wherever we use A. But the last two lines of the example show a case where A is allowed but AA is not.

Solution to Puzzles 1 and 2

At this point, there are two puzzles:

How could AA be both equal and not equal to A?
How can types both have and not have types in TypeScript?

The puzzles are just illusions caused by the interaction of two TS features:

TS has two worlds of things: the World of Values and the World of Types
class declarations introduce both a type and a value

Things like type aliases and interfaces live in the World of Types. Variables declared with const, let and var exist in the World of Values. You're allowed to reuse names in the same scope as long as they refer to things in different worlds:

type Thing = number;
const Thing = "hello"; // no error

But two things in the same world cannot have the same spelling.

const thing2 = 3;
const thing2 = {}; // error: Cannot re-declare block-scoped variable "thing2"

Ignore apparent violations of the rule for interface, namespace, and enum. This is the dread "declaration merging" feature I wrote about earlier.

As you saw above, we can use type to name something in the World of Types and const to name something in the World of Values. But a class declarations is magical: it simultaneously names something in the world of values and names another thing in the world of types!

The next example illustrates this double-declaration behavior. Note that:

the type C is the type of instances of C
Applying the type world's typeof operator to C gives you the type of the value-land C, which is a constructor function.

class C { a = 1 };
type CInstance = C;    // alias the `C` from the World of Types
const Constructor = C; // alias the `C` from the World of Values

const c: C = new C();
const c2: CInstance = new C();
const cons: typeof C = Constructor;

// The next line errors, because CInstance does not have the same dual-nature as `C`
// CInstance is *only* a type, so you cannot calculate its type
const cons2: typeof CInstance = Constructor;

Two puzzles solved!

Consider again an example like this:

class A {}
type AA = A;
type Z = typeof A;   // OK
type ZZ = typeof AA; // Error

Puzzle 1 was "How could AA be both equal and not equal to A?".

The answer is that there are two As: one in the world of types and one in the world of values. AA is equal to the A in the world of types, but not equal to the A in the world of values.

Puzzle 2 was "How can types both have and not have types in TypeScript?"

The answer is that we can never ask about the types of types in TypeScript. The seeming-violation of this rule was only because we were dealing with two As: a type-level A and a value-level A. We can ask for the typeof the value-level A, but TS won't let us ask about the type of the type-level A or of any of its aliases.

Puzzle 3

Puzzle 3 is: why are there no errors in the code example below?

class Klass {};
const konstructor = Klass;
const obj1: Klass = {};
const func: typeof Klass = konstructor;
const obj2: Klass = konstructor; // why no error here?

Puzzle 4

Puzzle 4 is: how can we correctly-type a function that returns a class?

For example, is there a way to get things like this to compile?

const MyClass = createClass({});
const m: MyClass = new MyClass();