# A Naive Substitution-based Polymorphic Type Inferencer

In this lesson you learn how little it takes to turn a naive monomorphic type inferencer into a naive polymorphic one, basically only changing a few characters. In terms of the K framework, you will learn that you can have complex combinations of substitutions in K, both over expressions and over types.

Let us start directly with the change. All we have to do is to take the LAMBDA type inferencer in Lesson 4 and only change the macro

```
rule let X = E in E' => (lambda X . E') E [macro]
```

as follows:

```
rule let X = E in E' => E'[E/X] [macro]
```

In other words, we are inlining the beta-reduction rule of
lambda-calculus within the original rule. In terms of typing,
the above forces the type inferencer to type `E`

in place for each
occurrence of `X`

in `E'`

. Unlike in the first rule, where `X`

had to get
one type only which satisfied the constrains of all `X`

's occurrences in
`E'`

, we now never associate any type to `X`

anymore.

Let us `kompile`

and `krun`

some examples. Everything that worked with
the type inferencer in Lesson 4 should still work here, although the
types of some programs can now be more general. For example, reconsider
the `nested-lets.lambda`

program

```
let f1 = lambda x . x in
let f2 = f1 in
let f3 = f2 in
let f4 = f3 in
let f5 = f4 in
if (f5 true) then f2 else f3
```

which was previously typed to `bool -> bool`

. With the new rule above,
the sequence of lets is iteratively eliminated and we end up with the
program

```
if (lambda x . x) true then (lambda x . x) else (lambda x . x)
```

which now types (with both type inferencers) to a type of the form
`t -> t`

, for some type variable `t`

, which is more general than the
previous `bool -> bool`

type that the program typed to in Lesson 4.

We can also now type programs that were not typable before, such as

```
let id = lambda x . x
in if (id true) then (id 1) else (id 2)
```

and

```
let id = lambda x . x
in id id
```

Let us also test it on some trickier programs, also not typable before, such as

```
let f = lambda x . x
in let g = lambda y . f y
in g g
```

which gives us a type of the form `t -> t`

for some type variable `t`

,
and as

```
let f = let g = lambda x . x
in let h = lambda x . lambda x . (g g g g)
in h
in f
```

which types to `t1 -> t2 -> t3 -> t3`

for some type variables `t1`

, `t2`

, `t3`

.

Here is another program which was not typable before, which is trickier than the others above in that a lambda-bound variable appears free in a let-bound expression:

```
lambda x . (
let y = lambda z . x
in if (y true) then (y 1) else (y (lambda x . x))
)
```

The above presents no problem now, because once `lambda z . x`

gets
substituted for `y`

we get a well-typed expression which yields that `x`

has the type `bool`

, so the entire expression types to `bool -> bool`

.

The cheap type inferencer that we obtained above therefore works as
expected. However, it has two problems which justify a more advanced
solution. First, substitution is typically considered an elegant
mathematical instrument which is not too practical in implementations,
so an implementation of this type inferencer will likely be based on
type environments anyway. Additionally, we mix two kinds of
substitutions in this definition, one where we substitute types and
another where we substitute expressions, which can only make things
harder to implement efficiently. Second, our naive substitution of `E`

for `X`

in `E'`

can yield an exponential explosion in size of the original
program. Consider, for example, the following classic example which
is known to generate a type whose size is exponential in the size of
the program (and is thus used as an argument for why let-polymorphic
type inference is exponential in the worst-case):

```
let f00 = lambda x . lambda y . x in
let f01 = lambda x . f00 (f00 x) in
let f02 = lambda x . f01 (f01 x) in
let f03 = lambda x . f02 (f02 x) in
let f04 = lambda x . f03 (f03 x) in
// ... you can add more nested lets here
f04
```

The particular instance of the pattern above generates a type which
has 17 type variables! The desugaring of each `let`

doubles the size of
the program and of its resulting type. While such programs are little
likely to appear in practice, it is often the case that functions can
be quite complex and large while their type can be quite simple in the
end, so we should simply avoid retyping each function each time it is
used.

This is precisely what we will do next. Before we present the classic let-polymorphic type inferencer in Lesson 9, which is based on environments, we first quickly discuss in Lesson 8 an intermediate step, namely a naive environment-based variant of the inferencer defined here.

Go to Lesson 8, Type Systems: A Naive Environment-based Polymorphic Type Inferencer.