> Typescript actually has an insanely powerful type system

I think you are conflating expressivity with complexity here. You do not need a complex type system to get a very expressive language. For instance, the typing rules of dependent type theory are fairly simple compared to the amount of trickery needed to make TypeScript work.

At constant expressivity, a simple type system is always preferable to a complex one. So I am not amazed by the fact that TS needs advanced PLT debauchery to kind of work. It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.

I think Typescript has both a complex and expressive type system. When I say "advanced" I'm talking about expressiveness. It is more expressive than Scala and (absent a laundry list of GHC extensions) Haskell.

I agree that Typescript certainly seems like a tower of hacks next to Idris.

Yet somehow it's pulled off a reputational miracle: having a more expressive type system than Haskell but not being regarded as an "advanced" language. Unfortunately I think that's mainly due to the ways the type system can be undermined, but it's still a useful nugget I ponder from time to time.

> It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.

HM by itself doesn't give you strong guarantees (see e.g. the ML family of languages which have comparatively weak guarantees next to Haskell). That's really due to other language and standard library decisions acting in concert.

HM type systems are often the sweet spot for static typing not because of the guarantees they offer, but because of the global type inference it yields. More expressive extensions of HM often break global type inference in some way.

Can you explain how you view Typescript’s type system as ‘more advanced’ than Haskell’s type system? I am working on a language currently and wonder what gives you that impression as a user who seems knowledgeable and demes to have a preference for one style verses the other.

Typescript has all sorts of type-level computation goodies that Haskell doesn't have (unless you turn on insane amounts of GHC extensions).

Stuff like mapped types, keyOf, typeOf, ReturnType, literal types, conditional types etc. all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations (this is how e.g. in Typescript we can have type signatures that capture all sorts of very dynamic Javascript function signatures).

On top of this Typescript also has a strong structural type system augmented by union types and intersection types. You can fairly easily emulate a nominal type system like what Haskell has on top of this system, especially with Typescript's string literal types, but it's quite difficult to go the other way.

The only big thing I can think of that both Haskell and Scala have that Typescript doesn't is higher-kinded types.

I also want to strongly caution that I don't think a more advanced type system is necessarily a better type system! E.g. I'm not convinced that Typescript really needs HKTs.

Likewise I have previously programmed quite happily in Elm despite its paucity of type-level features in comparison to Typescript.

> Stuff [...] all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations [...].

I think this is a wrong use of the term "dependent types". For example, you can't write this in TypeScript (yet):

    function concat<alen: number, blen: number>(
        a: ArrayOfLength<alen>,
        b: ArrayOfLength<blen>,
    ): ArrayOfLength<alen + blen> {
        return [...a, ...b];
    }

Sure, you can have a type-level object that corresponds to the numbers and use the type-level expression to compute the equivalent of alen + blen, but they are not dependent types. You have just shifted values to the type level. The type-level expression is awesome---but not because they are dependent types.

TypeScript is also not a typical type system you can compare with others. Most famously it is intentionally unsound [1], meaning that it can mostly but not entirely prevent a certain class of runtime errors, because it can't guarantee the behavior of external JS code anyway. Most static type systems are or at least try to be sound because that's what users expect them to be: preventing a wrong code beforehand. Dependent type systems are complex because they also want to be sound. TypeScript has an entirely different goal for a reason and you can't compare it with other type systems not sharing that goal.

[1] https://www.typescriptlang.org/docs/handbook/type-compatibil...

Actually, this is mostly possible.

Except for some issues regarding the stack size when resolving the types. (But I think there are more efficient implementations using more copy and paste, making this actually work)

playground link:

https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAO...

No, you are creating a literal type which is not same to the corresponding literal. This is evident when you try to use alen and blen (respectively named n and m in your code) in the function code: they are strictly type-level constructs.

Also, probably I should have written my example as follows:

    function concat(
        alen: number,
        blen: number,
        a: ArrayOfLength<alen>,
        b: ArrayOfLength<blen>,
    ): ArrayOfLength<alen + blen> {
        return [...a, ...b];
    }

My original code did distinguish two sets of arguments because that's the TypeScript syntax closest to currying (and I was lazy to check its implication), but the point of dependent typing is that alen and blen are not necessarily known to the compiler. The compiler may have to deal with the following code then:

    let abc = concat(a, concat(b, c));
    abc = concat(concat(a, b), c);

...where the first type `ArrayOfLength<alen + (blen + clen)>` should equal to the second type `ArrayOfLength<(alen + blen) + clen>` for the assignment to be valid. Since the compiler doesn't know alen, blen or clen, this means the compiler needs to somehow understand the associativity! This is hard, considering that (a+b)+c is not even generally same to a+(b+c) thanks to floating point.

For this reason many dependently typed languages also act as proof assistants or verifiers. If this point is removed, so-called "const generics" will be classified as dependently typed.

Well... would this satisfy you? (I removed the _add part for convenience. You could still argue that `_concat` is not a literal... if by literal you mean a primitive provided by the language itself. Note that i'm not claiming that this is a dependent type system. But you can emulate some features of such a type system.)

https://www.typescriptlang.org/play?#code/C4TwDgpgBAggTnAPAO...

Uh, no? _concat is a type-level function and you can't generalize it to receive runtime arguments in any way. I do acknowledge the value of type-level evaluation, but there is a very deep gap between type-level evaluation and dependent typing.

> I think this is a wrong use of the term "dependent types".

The operative term here is "a certain amount." `typeof` in Typescript is definitely a dependent type operator (it takes a runtime value and extracts its type which can then be used as a type signature for other types).

You don't have full-spectrum dependent types a la Idris, but you do have some amount of dependent typing. See for example

    type MyResult<T extends boolean> =
        T extends true ? { tag: 'a' } : { tag: 'b' }

    function outputTypeDependsOnInputValue(
        value: boolean
    ): MyResult<typeof value> {
        if (value) {
            // replacing 'a' with 'b' is a type error
            const result: MyResult<typeof value> = { tag: 'a' };
            return result;
        } else {
            // replacing 'b' with 'a' is a type error
            const result: MyResult<typeof value> = { tag: 'b' };
            return result;
        }
    }

Now there's a good deal of limitations and hackiness here in how you call this function (in particular you need some weird overloadedness to preserve the types at call sites), but it is really some measure of dependent types! I'll include a full example at the end of this post.

> Dependent type systems are complex because they also want to be sound.

Dependent Haskell, if it lands, will not be sound (TypeInType). Idris 2.0 currently also is explicitly not sound. In the case of Idris that's mostly a matter of prioritization, but it's enough to demonstrate that soundness is, perhaps surprisingly, not a huge priority for even all full-spectrum dependently typed languages.

Full TS example:

    type MyResult<T extends boolean> =
        T extends true ? { tag: 'a' } : { tag: 'b' }

    function outputTypeDependsOnInputValue<T extends boolean>(
        value: boolean
    ): MyResult<T>

    function outputTypeDependsOnInputValue(
        value: boolean
    ): MyResult<typeof value> {
        if (value) {
            const result: MyResult<typeof value> = { tag: 'a' };
            return result;
        } else {
            const result: MyResult<typeof value> = { tag: 'b' };
            return result;
        }
    }

    function worksWithA(a: 'a'): void {}

    function worksWithB(b: 'b'): void {}

    function useOurFunction(value: boolean): void {
        if (value) {
            const result = outputTypeDependsOnInputValue<typeof value>(value);
            worksWithA(result.tag);
            // worksWithB(result.tag) is a type error
        } else {
            const result = outputTypeDependsOnInputValue<typeof value>(value);
            worksWithB(result.tag);
            // worksWithA(result.tag) is a type error
        }
    }

There are numerous other well-known terms other than "dependent typing" that describe those features better, namely flow(-sensitive) typing. I believe the implementation of those type systems is considerably different from one of dependent type systems. I do have heard calling const generics as a "dependent fragment", which is fitting given that it might be the largest feasible fragment of dependent types without actually implementing the full-featured type system. I however object to any mention of dependent typing to describe something less capable than const generics since it's pretty misleading IMO.

You are absolutely correct that soundness is not the highest priority for dependently typed languages, as it had been true for other languages as well. Still I think most languages with a complex type system (subjective) do try to minimize the number of unsound corners as circumstances permit. I'm not an Idris user by myself but for example, the recent Idris 2 0.3.0 announcement [1] clearly considers unsoundness as something undesirable. As a result I have a general expectation for the type safety of those languages; I don't have that for TypeScript however (and I don't view that as a problem, just a difference).

[1] https://www.idris-lang.org/idris-2-version-030-released.html "Removed multiplicity subtyping, as this is unsound and unfortunately causes more problems than it solves."

I mean we're talking about definitions here so ultimately there isn't a definitive answer, but I think your definition of dependent types excludes a lot of things that are commonly referred to as "some dependent typing" or "lightweight dependent types" (this includes things like GADTs and singletons, Liquid Haskell, etc.).

It's important to note that what is going on in that TS example isn't just flow typing (otherwise something like Kotlin would count as a dependently typed language). The `typeof` operator is playing a crucial role here. That's what makes this really a case of a type depending on a runtime value.

If it was really just flow typing, then you could still replicate it in something like Scala by just introducing additional layers of types and folding over them (this is also why I would agree flow typing by itself is not dependent types). But that's insufficient to replicate the full TS example.

Idris doesn't want to make its soundness situation any worse than it already it is because the community does eventually want it to be completely sound. But like I said, that's not at the top of its priority list.

EDIT: Removed "Flow-sensitive typing isn't really all that different from dependent pattern matching (the main difference is on the other side of the coin, where you need some way of generating those dependent patterns and of cascading the flow "down" so to speak, so indeed by itself flow-sensitive typing isn't dependent typing). " as the first line because it didn't seem all that relevant in retrospect.

TypeScripts type level operators are brilliant. They’re somewhat necessary to be able to type semi common JS patterns, but still, they’re brilliant.

“Brands” allow you to somewhat hack HKTs into Flow/TS, which is used by fp-ts to great effect.

Thanks for this write-up. What about ADTs and pattern matching?

Afaik, they are not available in Typescript and the emulations that I've seen are very sloppy.

TypeScript supports ADTs (discriminated unions) and not-quite-pattern matching using a combination of features: union types, literal types and control-flow based type narrowing.

Here's an example from the TS handbook: https://www.typescriptlang.org/docs/handbook/unions-and-inte....

What you need to understand about TypeScript is that it ultimately is just JavaScript. After TS 2.0 a decision was made that TS will align with standard EcmaScript and will not implement any* run-time features not part of the ES standard or ES proposals.

Because of this decision TypeScript cannot have a proper dedicated pattern matching syntax until JavaScript gets one. TypeScript does support some pattern matching using ifs and switch statements and other control flow structures, but that's as good as it gets until JS improves as well.

Here's what I use:

https://github.com/gbegher/groth/blob/460852a71859f149ecf9b5...

Did not cause any roadblocks so far.

and just as the complexity of HKTs might not add value to your team/project, other type tricks may also detract. These 'goodies' can seem 'insane' (or not) irrespective of which language they're realised in. After a while, I realised that I enjoyed Elm partly because of features it doesn't have ;)

HKTs are a lot less complex than most of Typescript; in a way they're not so much a feature as just the absence of a restriction (type parameters can have parameters just like any other type).

> Typescript actually has an insanely powerful type system, in many ways much more advanced than Scala's type system and certainly more advanced than "vanilla" Haskell (i.e. something like Haskell2010).

That's a strange claim. I mean, yeah, maybe you can say that it's more advanced than "vanilla" Haskell, but how many people use no extensions at all?

As for the comparison with Scala - maybe for Scala 2 that's true because of union- and intersection-types and Scala 2's lack of certain typelevel programming features.

But when compared to Scala 3 - is there anything major that you can do with typescript but not with Scala 3?

When I looked at typescript, my impression was that it has a lot of special rules and special syntax for certain typelevel programming features. Which is nice in many cases, but it doesn't compose and does not age very well. Still, I'm happy to see this development in a mainstream frontend language.

> That's a strange claim. I mean, yeah, maybe you can say that it's more advanced than "vanilla" Haskell, but how many people use no extensions at all?

Let me broaden that then. Typescript's type system is more expressive than even the proposed list of GHC2021 extensions. You really need to turn on "GHC and the kitchen sink" (basically your code is probably going to be using the singletons library and everything that entails) to get to the feature set of Typescript's type system. I think that's beyond what the vast majority of Haskellers use or are comfortable with.

> But when compared to Scala 3 - is there anything major that you can do with typescript but not with Scala 3?

Plenty. Part of it has to do with the fact that interfaces are truly structural types in Typescript whereas traits are still nominal in Scala 3. So for example, Typescript lets you have "complement types" (i.e. give me all the fields of A except those in B) which you cannot do in Scala 3.

Here's an example of a useful type-level thing I've found myself wanting all the time in Haskell and Scala that is very straightforward in Typescript.

Often we have a record

    data MyRecord = MyRecord
        { field0 :: Int
        , field1 :: Bool
        , field2 :: Bool
        }

that must undergo validation first before we can generate the record (e.g. parse out a bunch of strings for each field into Ints and Bools where those parse operations may fail).

It is tedious to write a whole new data type which duplicates all the fields, but just adds a Maybe in front of each type. Haskell has a design pattern known as "higher-kinded data types" that tries to mitigate that.

    data MyRecord f =
        { field0 :: f Int
        , field1 :: f Bool
        , field2 :: f Bool
        }

In its more sophisticated form we can use type families instead of normal higher-kinded types along with TypeApplications to make this fully seamless and get rid of a lot of Identity wrappers. Scala 3 allows something similar with match types (in fact you don't even need match types for getting rid of Identity wrappers due to Id in Scala being a type synonym and being able to do the equivalent of TypeApplications for higher-kinded type synonyms).

This approach, however, doesn't quite work if you have multiple validation steps that return multi-field fragments of MyRecord (e.g. one step returns a fully validated field0 and field1 and another returns a fully validated field2). You basically need to resort to writing a bunch of duplicated types again (type families can kind of save you if you happen to have all entirely distinctly types).

Typescript's mapped and conditional types handle this with aplomb, letting me generate any combination of fields wrapped in any combination of types from a single type definition.

Separately, in another comment in this same chain I give an example of (limited) dependent types in Typescript. I think you can replicate it with singletons in Haskell, but that's definitely getting into stuff that I would say "doesn't compose and does not age very well" in Haskell (ah should the blessed day that dependent Haskell lands arrive soon!). AFAIK you can't replicate that in Scala 3 because of a lack of value to type promotion mechanisms (I think even with match types it's not quite sufficient).

Actually, both your examples are possible to solve even in Scala 2. Check my repository from 4 years ago. The Readme has the examples that will be interesting for you: https://github.com/valenterry/bamboomigrate

I'm not saying it looks very elegant though - this is certainly improved a lot in Scala 3

Actually, the match types page in Scala 3 lists some of the differences with typescripts approach: http://dotty.epfl.ch/docs/reference/new-types/match-types.ht...

Ah I think we're talking about subtly different things. You can definitely use generic goodness (`Generic` in Haskell and shapeless in Scala) to create generic conversions between different types, but the result of each conversion is not itself a user-friendly type.

In the case of shapeless the general pattern is to have a starting type, use something like LabelledGeneric, do a ton of HList transformations, and then transform back. But while you're living in HList land those are in fact HLists and not, say, case classes.

Indeed, you must always write out the final type yourself (e.g. create a new case class). Even if you're using only HLists and completely eschewing case classes (which is both ergonomically painful but also has a pretty large performance hit), shapeless's functions that generate new HLists (as opposed to extracting an element) almost always require you to annotate their use sites IIRC, which is effectively the same thing as needing to write out the whole case class.

To put it another way, with shapeless in Scala 2 you could prove that a certain type was the intersection of two other types and create the generic transformation to do so. But this isn't true intersection types because you still need to write your starting types and your final type. That is in Scala 3 you `T0 & T1` is a type in and of itself; you don't need to rewrite all the fields in common between T0 and T1 and assign it to a new type (and then e.g. use shapeless to prove the relationship between your types).

In the same way what you've demonstrated here aren't mapped types, conditional types, etc., but rather a way of using shapeless to prove that a certain type is the mapped type/conditional type etc. of another type. The former is what I meant when I said "letting me generate any combination of fields wrapped in any combination of types from a single type definition."

Shapeless doesn't get rid of the problem that "Higher-Kinded Datatypes" (HKD) is trying to solve, since you still have to write all the duplicate types by hand for any reusable function.

Moreover, apart from the tedium of rewriting all these types, the bigger issue is that TS's type system lets you stay entirely at the value level, whereas shapeless requires things to become type level computations, effectively bifurcating your code into "shapeless transformations" and "ordinary functions acting on e.g. case classes."

For example, the equivalent of your library in TS would have each step just be a normal function like any other rather than a special type level computation. It can be applied to a normal object directly and can be tested and reused just like any other function.

That match types page on Scala 3 I think undersells the differences. The real power of a lot of TS's type level computations is how they interact with each other and typeof (see my other example in this thread of lightweight dependent types).

All that being said, I really like the concept behind your library and would love to see it updated for Scala 3!

Just wanted to say that I appreciated this detailed comment and your replies in the threads beneath it. Cheers.

Glad to hear it!

I think not enough people appreciate just how amazing TS type system is, I often want to use it in pretty much every other language I use.