domagoj miskovic

Posted on

# Indiscernible types of Haskell Holmes

There seems to be an ambiguity in the idea, a common vibe I hear on the grid, like an excuse mentioned in some books and papers, that one of type safety's downsides it the fact that some expressions which would otherwise evaluate to a true value would be rejected on the typing grounds, the reason being that even though for example both expressions in an `if then else` may on their own evaluate to true or to some true value within a known type instance of their own, they somehow cannot exist together in a branching statement, one cannot call another one, meaning `if such expression is true then this expression is true`, meaning the second expression will take place, the second event will happen if the first evaluates to true, as if this new event that may take place is to be rejected simply because it does not follow the type in the first expression. The common example would be `if True then 1 else False` where if some boolean value in the Bool class of type values which contains two values `True` and `False` or a boolean function type such as `not :: Bool -> Bool` which is a function from one bool to another bool, sou see when you negate something you get the inverse of that thing or something else within that type universe, what else could it be? Not true is false, negate 5 is -5... now if such an expression evaluates to true we are to call a number, or any number, in this case an integer number, `1 :: Integer` that belongs to a class of numbers, `1 :: Num p => p` but you know all that. Apparently this seems to be an invalid statement, an invalid type inference between two expressions, between a bool and a number one.

Watson: Hmmm... what if instead of `False` we would have something like `otherwise "play me an ambient like Jedimind soundtrack now"`? Would that be any different than a simple `False`. What is happening here and why is this a bad thing in the first place?

Haskell: But Watson, my dear friend it is not about the rest it is about creating algebraic structure with not enough information.

Watson: What information? If something is true then give me 1. What is so strange about that. You seem to question everything, I am not surprised you named your dog Haskell for all I know.

Haskell: Watson I do not have a dog, you would be the first to know if I had one.

Watson: There, you just said if you had one I would now, could we take that as an example?

Haskell: Watson my boy you cannot just jump from one to another mathematical realm and expect not to spill any milk along the way. The obvious reason your reasoning is currently at its peak is that you are not fully aware of the way types transform from one instance to another.

To put it simply, the way a computation evolves depends on the language your structure encodes and the way to compose different structures into new ones you will have to do a lot more than a simple if then else statement! Try to see, if then else statement if we translate it into a typful universe might seem like an instance of a boolean function. I am describing it as a boolean because it is so simple, it actually goes from a bool to a bool. But hey we are Haskellers, and this is an old artefact from medieval times, I suggest you practice defining functions without such if then else statements because Watson my friend life is complicated and no if then else statement is going to save you from your puny little brain, even worse you might have to stitch together a string of such expressions, then when you look at it, you will not know right from wrong.

Watson: All right Holmes, and tell me what about the `Either` type? `data Either a b`? It also seems like an if then else statement with maybe more freedom defined since either a or b is for you to pick which could be also realized `if True then a` and `if True then b`. How about that?

Haskell: Bravo Watson, you did it again! `Either`data type does represent either one value or another, `Either a b` which we can further realize as `Left a| Right b` and it might seem like we take these lefts and rights for granted while if we had an `if then else` before either, we would be actually checking some precondition and then applying one of these eithers.

``````data Either a b = Left a | Right b

firstCondition = Left True
secondCondition = Right 1
``````

Watson: This is beyond me Haskell, how did you come up with this?

Haskell: My dear Watson let us go then you we must investigate this case immediatelly! Call a cab!