Comment by walterburns 14 hours ago
"But we'd like to give a type to this function. In most languages (Haskell, Typescript, C++, Rust, C#, etc.) there is no way to do that.[2] "
Can't you do this with a GADT? With a GADT, the type of the output can be specified by which branch of the GADT the input matches. Seems quite a similar idea.
No, because 1) you can't do (full) dependent types in TypeScript, 2) it's not clear what "dependent types" would even mean without type checking, and 3) using the union type you aren't giving up type checking at all.
The limitation is what comes later in the article - the dependent type can express the relationship between the argument and the returned type. But that's "out of scope" of the question of "typing a function that can return either a number or a string depending on the boolean argument". It only becomes a problem later on because to use the result you need to test the type (using `typeof`) even if you know you which boolean you passed in; that information doesn't end up tracked by the type system - although there actually are a couple of different ways to do this that satisfy this example in TypeScript, as suggested by some other comments.
Just using a union type in TypeScript isn't dissimilar to my suggestion of wrapping the result in an ADT; it's just that TypeScript makes this lightweight.
GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints.
Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on the types, and then provide proofs that it's compatible with the value-level.
Then you often need singletons for the cases that are more complex- if I have a set of integers, and an int x, and I want to constrain that the item is in the set and is also even, the GADT approach looks like:
doThing :: Singleton Int x -> Singleton (Set Int) s -> IsInSet x s -> IsEven x -> SomeOutput
Which looks reasonable, until you remember that the Singleton type has to have a representation which is convenient to prove things about, not a representation that is convenient/efficient to operate on, which means your proofs will be annoying or your function itself will hardly resemble a "naive" untyped implementation.
Dependent types fix this because your values are "just" values, so it would be something like
doThing :: (x : int) -> (s : set int) -> so (is_in s x) -> so (even x) -> SomeOutput
Here, x and s are just plain values, not a weird wrapper, and is_in and event are ordinary (and arbitrary) library functions.