> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/350-type-theory/hindley-milner-type-system/algorithm-w-in-haskell.md).

# Algorithm W in Haskell

**Type inference** refers to the process of determining the appropriate types for expressions based on how they are used. It is performed on a language's expressions that are not (fully) type annotated by the user.

**Type checking**, on the other hand, checks expression that are type annotated by the user to see if the types check out.

Type inference is performed at compile time, after the source code has been parsed and arranged into AST. Here, we describe the "Algorithm W" that is a well-known algorithm for inferring the types in a PL based on Hindley-Milner type system. We skip the syntax, semantics, parsing and all that jazz, and just assume we have some expressions of some object language available as structured expressions in the meta-language, i.e. Haskell.

We're dealing with an object language that has terms (no shit) and types that classify the terms.

Like every PL, our object language (OL) has constant terms (literal or constant values) which are terms that represent themselves, and they all belong to the set of the base types. For example, `True`, `False`, `3`, `42`; and what that we have already listed all terms of base type `Bool`, and a few terms of our other base type `Int`. So, `Bool` and `Int` are in the set of our base types.

The base types are part of a more general category of types, called **monotypes**. In our language, and in general notation, monotypes are denoted by `τ`. Monotypes are concerete types, like the base types `Int` and `Bool`, but also function types on the base types, like `Int -> Bool`.

The base types are like a base case of recursion - something the recursion approaches closer with each iteration, until finally reaching it and terminating. Here, the function types are an example of types that will recursively work towards the base type. The function type are generally denoted by the form `τ -> τ`.

Then, now, techically, type variables, `α` are included in monotypes, but it is exactly type variables, either standalone (`a`) or as part of a function type (`a -> a`) that will be generalized into polytypes. Polytypes are denoted by `σ` and they subsume monotypes, plus the special "forall-type" of the form `∀α.τ`.

The rules say when a type may be generalized (made into a type scheme or a foall type), but an aditional clearity about it is left desired. Sometimes it seems that each type variable will be generalized into a forall type var. Note: the entire type is called type scheme (forall type) even though that whole business depends on the presence of type var(s), so I might slip and say that the type var is generalized. An example of a forall type is:

`apply :: forall a b. a -> (a -> b) -> b`

My inability to come up with a prompt example of a type that has type vars but is not generalized, make sits own statement.

* Types, `Ty`
  * Monotypes, `τ`
    * base types (type literals, type constants)
      * `Int`
      * `Bool`
    * function types, `τ -> τ`
      * Int -> Int
      * Int -> a
      * a -> Int
      * a -> a
      * etc.
    * type application, `C τ₀ … τₖ`
    * type variables, `α`
      * `a`
      * `b`
      * etc.
  * Polytypes, `σ`
    * monotypes, `τ`
    * type schemes, `∀ α₀ … αₙ . σ`
      * `forall a. a`
      * `∀a. a -> a`
      * `∀a b. (a -> b) -> a -> b`
* Substitution mapping, `Subst`
* Type environment, `TyEnv`


---

# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.

## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://mandober.gitbook.io/math-debrief/350-type-theory/hindley-milner-type-system/algorithm-w-in-haskell.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.