Hindley-Milner Type Inference in Small Words

in this writing i explain a way to guess the kind of information used in computer jobs using the most used ten-hundred words in the language you're reading right now. I got this idea to use a lot of small words from the book thing explainer.

in computers we need to tell them what to do. sometimes this is very hard, because we do not know everything a computer can do. what we tell the computer and what it does are sometimes different, and it is important to make sure that this is not the case.

so, how do we make the ways a computer can make no-nos smaller? One way is to make sure it only uses the right kind of information. there are a lot of long words that people use to talk about the kind of information computers can use, but we will keep things simple here.

a computer job has a lot of way to take information in and then change it. this job is a small set of smaller jobs, and must tell the computer what kinds of information it knows how to use. Most of the time, you have to tell the computer all the kinds of everything, but this can feel stupid because the computer should know the kinds of jobs it is going to do, right?

A long time ago, some people were thinking about this, and they found an answer! they were not working on the problem together, but they got the same answer. very cool!

so what answer did they find? when ever we run a computer job on some information, we know that that job is made up of smaller jobs. and if we can find the kind of those smaller jobs, and how they work together, maybe we can find the kind of the bigger job.

this way to guess the kinds of information for computer jobs has three steps:

first, we pretend we don't know the kind of any job, and just give everything a different kind.
then we look at how the smaller jobs work together to guess how all the different kinds work together
knowing how different kinds work together, we can guess the real kind of the jobs.

In real life, these steps are usually all done at the same time. but we will look at them alone to figure out how they work together

step one: different kinds

so far we have just been talking about kinds of jobs in a soft way, but we need to write some hard meanings down before we go any farther. We will be using a simple language to talk about the kinds of information and jobs. In fact, our language will only have five different things in it:

24 is 'information', in our language we can only talk about numbers
name is a 'name' which means some information
a -> a is a 'job', that takes some information and makes some more
a i is a 'call', that gives runs the job a with the information i |
name = thing is a 'let', which lets us use a name to mean another thing

this is a very simple group of things, but the stuff we learn can be used to make harder groups of things.

what about the kinds of different things? A kind can be:

a number, like 24
a job, like a -> a
many, like i

The thing here that we need to understand is 'many'. many is a kind that can be different, but the same many means the same thing. so, the job:

identity  -> a

which does nothing (just gives us the information we put into it)

So, how do we find the kind of the bigger job. there are three main steps:

first,