Types

This post explores the types and functions tutorial by @typeclasses. Their tutorials have this a bit different kind of teaching method, besides pure formalism they seem to try to teach by talking about things, but then at the same time thinking with and through types seem to be very conducive to a different kind of teaching method, different kind of wisdom in which without explicitly stating the set of instructions, for example what needs to go where and when, without merely pointing into the horizon, types take on a much more receptive role and invite the student and the teacher to a different kind of mental state, a much more intuitive, slower state in which there seems to be much more thinking involved within more precisely formed units. Also each definition could have an infinite number of teaching methods or vehicles which might illuminate certain aspects of it, at the same time there is an infinite number of past or future analogies one could use, for example think of the identity or a boolean value. Still, at the same time because of the functional purity and referential transparency and because no information seems to be discarded within imperative lossy flows, higher and more complex abstraction could be realized by composing these basic abstraction units. So something such as a functor is essentially one of the most precious things there is, and once a student learn about these transformations the student realizes that there are more of those types of transformations. Upon realizing such structures an emotional inspiration arises precisely because these abstraction contain themselves within themselves, so to say they scale perfectly in unison, and so one feels empowered more and more while retaining knowledge to a much higher degree, essentially purifying the view within the mind, or to use the term garbage collecting any knowledge. You could say there is not much garbage to be purified while thinking in pure functions since each and every one of them, totally return what they are asked for.

We can think of types as being like sets. When we think about numbers, for example - "numbers" is not itself exactly a set. There are different sets of numbers that are useful for different things.

But this brings to mind that there might actually be an infinite limitless number of these sets of numbers, because there are so many ways to count things, some more, some less useful than others. Besides the usefulness of a counting action, the process of numbering things or objects, we also can analyze how many there are ways to count. But then comes the question could there also be a way to count a finite set of numbers using an infinite amount of numbers, basically never reaching the last finite number of the set? But why would anyone do that? This could be like using every possible real number from the number line to count from 1 to 10, we might never reach even the number 2! We notice there is a certain shape how the counting process evolves, what is this actual movement of the counting process, some numbers seem to flow so to say evenly in the sense that there seems to be an equal distance between each numeral of the counting range, like from 1 to 2, from 2 to 3 and so on while some numbers seem to progress in a different way, seemingly going deeper as in 1.1, 1.11, 1.111.. but then I wonder is this really counting? I read about surreal numbers which are like progressing in a really fascinating way, like they have dual nature, one part of them counts in one way, the other one in a different and both parts of one number consist of one count, as if one number had two numbers within in order to make the count, but I should read more about these surreal numbers, I have no idea how they work. Still sometimes we take for granted the notion of a number and we spend our lives counting with naturals but there is nothing natural about natural numbers, even the name seems confusing at first, why are they called natural, is it just because we have five fingers on each hand? Or twelve little joints on each hand too?

Still to continue the pursuit, if there are numerous ways to count things, and if there are numerous sets of these numbers then there are also an infinite number of types as well! But still, the mere mention of a certain type we seem to forget about the size of the set but begin to think about what such a set could contain, how could it be described, because types seem to be described in a much more detail than just a simple number.

What we call numbers are not a fixed set of things, but a group of sets that have some things in common. For example, we can do addition with members of any of these sets - we can add integers, we can add natural numbers, and we can add rational numbers..

So there are all these operations which we can use with different kinds of numbers, which in turn produce different results, depending on how we want to count something. Hmm, what about these operations then? So there are different types of numbers, different types of things which could have potentially an infinite number of operations defined over them so that means there are also types of collections of operations that could be defined over our space of a variety of number types. How would

Now comes the kicker. In the next paragraph it says that In Haskell, the concept of "being a number" is represented through a typeclass. OK, I actually thought that the concept of a number would be represented as a type since for example a type natural contains all the naturals and a type rational contains all the rational numbers and so on but here I stumble on something else. It continues with We have types in Haskell which are like sets, and we have classes - which is sort of a larger concept - that defines some operations that multiple sets have in common.

Fascinating! So basically types are just like images, or like certain actors within some domain and a typeclass is like a collection of these types, these actors and some number of operations or events that are possible to happen between them. So in our number case the type would be a natural or a rational and these types of numbers would then belong to a larger all pervasive Num typeclass, which is a collection of different types of numbers, different instances of one typeclass. The unique thing that connects them is simply that they are all types of numbers with some operations defined over these numbers because we need operations if we want to do something else besides simply counting from the lowest to the highest number. We naturally come to define other operations when our conditions change. If we were to count how many people are in a room we would start counting 1,2,3 until we reach the last person and so on but if suddenly 10 people were to leave we might just want to simply subtract those 10 from the total number of people instead of counting again from the beginning. This is especially useful if there are a million people in the room and 10 people leave, who would want to start the count all over again? But then does the computer actually count again from the beginning? Is a list of people being counted from the beginning and then if some are to be erased will the computer count again from the beginning? How does the program count the list of people then if it can't see that 10 people are missing from the room? This is a question that has to do with how lists, a basic data structure is implemented and how the computer constructs these structures.

What if you could not count at all? What would be the simplest possible way you could count things? You could simply say a word, like "DA", and then "DA" over there, and then "DA" and all the numbers would be "DA". This is very simple, like seeing every thing in the world as a toy you reach out point towards it and happily say "toy!", this is a "toy"! and so on. So this is like a type that is not numeric in the previous sense but that has only two values within, called Bool. So instead of DA this type can describe things with True and False which actually seems like the minimum amount of abstract movement one can make within ones mind. Something could be here or there, something could be true or false, but is it really like that? Is our Bool something like a simple DA? Well maybe it is not, since it contains two symbols. The DA would seem to be some kind of identity which does not even affirm the thing being pointed at, it merely repeats the same thing over and over again without regard to which thing we provide it. So if we give it an apple it says DA, if we give it a string it says DA, is this some kind of an identity? But an identity would be like identity :: a -> a and in our case this seems more like da :: a -> da. What is this then? Aha! This might be that super cool type called Void which always returns void. But why void, is it because it makes no sense and only introspects within itself like a black hole, like some void without any bottom anything that we throw at it becomes simply void? So like DA, void is a form of DA, fascinating!

But can we think of a typeclass, maybe, that could include both character types and numbers? What could a set of characters and a set of numbers have in common?

Yes! When we use numbers we often like to use words too, words that have meanings so what would such a type look like that would contain both words and numbers within. One needs to be a bit more precise because when we say words and numbers what we actually mean are characters and numbers, because characters form words not the other way around, but then some words do form our character too, now that might be confusing, but so words are, they are awfully confusing with many meanings! But let's come back to the question of What could a set of characters and a set of numbers have in common? Well this is deep, I am kinda staring into the darkness and thinking...

So I look into the other window and there it says,

...they can be put into an order. There's a typeclass for that, called Ord. That's where the comparison operations like greater thn (>) and less0than (<) are. One value is less than another (x < y) if x comes before y in ordering.

Now what is actually happening here? We are actually not counting now but it seems to me we are arranging the counting numbers into an order, as if we already did the count and now the numbers got all mixed up so we rearrange them again into the counting order. But the thing with order is that it seems we do not have to do the count again, we just have to order them, we put the smaller number before a larger number or maybe do any ordering operation we like. Why are we ordering things? Well we order things all the time, even our thoughts come completely in an unordered form in o ur heads and then we suffer mentally because we are unable to order our thinking so that we don't suffer. Maybe all suffering consists of unordered thought and our brains which love types and mathematics cannot stand that, they cannot stand that some thoughts are larger and some are smaller and then it wants to order things. There is something beautiful and all encompassing when we look at an ordered field, it somehow looses the individual particularities, those numbers that jump out or fall back. An ordered field is like an empty space, each individual unit is like being aware it is a part of something greater than itself, each number is at the right place at the right name. We also understand things much better when we order them and have a better sense of their individual characteristics when we order them.

But what happens when we see two instances of the same number, of the same thing in front of us, is this even possible? What if there are two equal things or isn't everything actually unique in itself? Are two oranges equal? Well if we are simply counting 2 oranges and 10 apples then maybe yes two oranges are equal and 10 apples are equal, it seems it all depends on what kind of an abstraction level we are standing upon. Some things seem to be equal and then those same things are not when we look at it from a different poin of view. Equality seems like a super deep question, that might be the last question there is? Could it? Well Haskell has an equality class of types called Eq which has an operator == which is tests for equality. But what is the difference between the double == and a single =? A single = seems to be forcing us to observe some result from some action while == is like simply measuring if two sides of an equation are the same. But then why the equations I did in the elementary school contained only a single equality sign and not ==? Maybe because the result was being mixed with the action itself, so some unknown variables were being added and then the result was also intermixed with some extra variables, the result was hidden, obscured so we had to extract the single unknown variable which was the result. This still seems different than the double equality sign. But then how would you judge what is equal, it seems there are infinite levels of double equality signs, meaning there are all kinds of equalities around, some more tight some loose to use a slightly loose terminology...

Functions

Now if types were to be understood as concrete images then functions would be like moving images, like movies of those images, just in our case our movie could be arranged in all kinds of ways, we would not have to go only from the beginning to the end but we could like in the recent Nolan movies Tenet go back and forth in time while at the same time some other timeline could meet us in the future. We could arrange our images into whatever we want because we are not bound by the meaning of these images. When we describe a meaning it is usually set in some temporal shape, into some timeline, this is what meaning basically means, but then the more actors we perceive, the more events we engage with the more our timeline warps into itself and introduces different time-shifts within. OK, so what are functions, these super exciting movable objects. Wait are functions objects? Or are they functions? A function is more like an action, so how would we compare an action with an object. Well maybe if we understood an action as an transformation then maybe we could call that particular type of a transformation an object? Hmm..

On the left we have numerals, on the right we have the words for numbers, and we are asked to draw a line from each numeral to how it's spelled. In our elementary schools we had to do a lot of these kinds of exercises. This is our mental picture of what defining a function is like: drawing lines from the things on the left to the things on the right, based on some rule that tells us what makes the matching meaningful. A function is a description of how an element from one set gets matched to an element in another set.

This is a really nice description of how a function works. Let's check the Wikipedia one which is a bit more formal but still the same:

A function is a process or a relation that associates each element x of a set X, the domain of the function, to a single element y of another set Y(possibly the same set), the codomain of the function.

The one before that is also a bit more compact:

a function is a binary relation between two sets that associates every element of the first set to exactly one element of the second set.

But let's return to typeclasses where a simple program is introduced! Yay enough theory!

spell :: Integer -> String

So the spell is the function name then the empty square with only corners shown or a double colon sign which symbolizes the action of saying has a type or basically what the double colon means is that it is raising the abstraction level from naming things into describing which kind of processes are to be uniquely identified with that name, so could our spell be actually an object? Could this spell function be understood as an object? Why? Because it has a name? Is every thing that has a name an object too? OK, so what does Integer and String represent here, they represent the domain of our process and the codomain, which is like the starting point of our transformation and the endpoint of our transformation. Now it might be the truth that actually the domain and codomain are basically the same thing, though they might seem different if we look at it from a temporal perspective, after all a broken egg is still an egg but it is broken only after and not before so some kind of transformation did take place. So is it then breakfast :: whole egg -> broken egg or maybe sunny side up :: whole egg -> broken egg? But let us continue with the typeclasses code example:

spell :: Integer -> String

spell int =
  case int of
     1 -> "one"
     2 -> "two"
     3 -> "four"

to be continued...