Here are the Boston Typescript Meetup 18/04 details.
Areas where Typescript is unsound:
- Refinement invalidation
Refinement is an if clause that checks a type:
const f = function(a: number | undefined) {
if (a !== "undefined") {
// Here, typescript knows that a must be a number
}
}
Refinement invalidation is when a side effect of an external function mutates the state of the variable. This happens on fields of objects.
- Array & Map Indexing
Indexing into an array returns a non-undefined type, even though it could be defined. Typescript doesn't acknowledge that indexing into an array could return undefined.
You could declare an array of number or undefined, which will catch these errors, but that would require an awful lot of refinement, that would be noisy:
const a = [1,2,3];
for (var i = 0; i < a.length; i++) {
if (a[i] !== undefined) {
doSomethingWith(a[i]);
}
}
Other type systems throw a runtime error when accessing an undefined part of
an array, rather than return null. Rust has an array.get
method that returns
a Maybe.
- Variance
"Here we're gonna talk about type theory" 😬
Code example too long to type.
Invariant | Covariant | Contravariant | Bivariant Here is a James Kyle article about this.
Typescript has covariant arrays, which causes runtime type errors, hence, unsoundness. Tweeter is sad.
The only sound solution would be invariant arrays. But that makes it difficult to program with arrays in typescript. Shrug emoji.
Go does the simplest possible thing - invariance. You'd have to copy your array of Squares into an array of Shapes before calling a function.
Java's typesystem does the same thing as Typescript, and errors at runtime.
Flow has a very complicated system that just figures it out somehow. They make it easier to use with mutability.
Rust has a first class concept of mutability - tracks mutability of every variable. Mutable is invariant, immutable variables are (bi?)variant.
Variance describes how the subtyping relationshipts of containers (like arrays) relates to their contents.
Typescript uses covariance for nearly everything, except functions, which uses covariance and contravariance.
Other languages are divided on what to do here.
"Why it's ok that typescript is unsound" - they made tradeoffs for completeness
- they're ok with stopping you from writing programs that would otherwise be valid.
Story of converting a large 19000 LoC Node JS Graph QL Server to TS.
- "Defer complex things"
- "types.ts" for just throwing placeholder definitons, so that you don't have to convert a very large file all at once.
export type TODO = any
- a good way to distinguish placholder types from things that are actually meant to be anany
type.- Only fix what doesn't typecheck
- You still need tests lol
- Fix latent bugs (typescript will show you where bugs exist, fix them as you go
- You will have to deal with missing types for 3rd party modules
- Fun with typing wrappers
- He's not done converting the codebase yet.
References: