Sum types - Why in Haskell is `show (Int | Double)` different than `(show Int) | (show Double)`

Question

Why are these not equivalent?

show $ if someCondition then someInt else some double

and

if someCondition then show someInt else show someDouble

I understand that if you isolate the if ... else part in the first example to an expression by itself then you can't represent its type with an anonymous sum type, the kind of Int | Double, like something you could do easily in TypeScript (mentioning TypeScript because it is the langauge I used often and that supports Sum types), and would have to resort to using the Either data then based on it would call show.

The example I gave here is trivial but to me it makes more sense to think "Okay we are going to show something, and that something depends on someCondition" rather than "Okay if someCondition is true then show someInt otherwise show someDouble", and also allows for less code duplication (here the show is repeated twice but it could also be a long function application and instead of an if ... else there could be >2 branches to consider)

In my mind it should be easy for the compiler to check if each of the types that make the sum type (here Int | Double) could be used as a parameter to show function and decides if the types are correct or not. Even better is that show function always returns a string no matter the types of the parameters, so the compiler doesn't have to carry with it all the possible "branches" (so all the possible types).

Is it by choice that such a feature doesn't exist? Or is implementing it harder that I think?

Answer 1

There are product types with lightweight syntax, written (,), in Haskell. One would thing that a sum type with a lightweight syntax, something like (Int | String), would be a great idea. The reality is more complicated. Let's see why (I'm taking some liberties with Num, they are not important).

if someCondition then 42 else "helloWorld"

If this should return a value of type like (Int | String), then what should the following return?

if someCondition then 42 else 0

(Int | Int) obviously, but if this is distinct from plain Int then we're in deep trouble. So (Int | Int) should be identical to plain Int.

One can immediately see that this is not just lightweight syntax for sum types, but a wholly new language feature. A different kind of type system if you will. Should we have one?

Let's look at this function.

mysteryType x a b = if x then a else b

Now what type does mysteryType have? Obviously

mysteryType :: Bool -> a -> b -> (a|b)

right? Now what if a and b are the same type?

let x = mysteryType True 42 0

This should be plain Int as we have agreed previously. Now mysteryType sometimes return an anonymous sum type, and sometimes it does not, depending on what arguments you pass. How would you pattern match such an expression? What on Earth can you do with it? Except trivial things like "show" (or whatever methods of other type-classes it would be an instance of), not a whole lot. Unless you add run-time type information to the language, that is, so typeof is available — and that make Haskell an entirely different language.

So yeah. Why isn't Haskell a TypeScript? Because we don't need another TypeScript. If you want TypeScript, you know where to find it.

Answer 2

All parts of an expression must be well-typed. The type of if someCondition then someInt else someDouble would have to be something like exists a. Show a => a, but Haskell doesn't support that kind of existential quantification.

Update: As chi points out in a comment, this would also be possible if Haskell had support for union/intersection types (which are not the same as sum/product types), but it unfortunately doesn't.