Simple types

\[ \gdef\code#1{\mathtt{#1}} \gdef\typeof#1{\left<{#1}\right>} \gdef\par#1{\left({#1}\right)} \]

Take the exemplar line

\[ \code{fact}\ \code{n}\ \code{return}\ \code{:}\ \code{isZero}\ \code{n}\ \code{base}\ \code{recurse} \]

Denote the type of a parameter \(x\) as \(\typeof{x}\) and the type of a closure as \(\par{a_1, a_2, \dots}\) where \(a_1\) is the type of the first parameter, etc. Then the above line implies two type equations:

\[ \begin{aligned} \typeof{\code{fact}} &= \par{ \typeof{\code{n}}, \typeof{\code{return}}} \\ \typeof{\code{isZero}} &= \par{ \typeof{\code{n}}, \typeof{\code{base}}, \typeof{\code{recurse}} } \end{aligned} \]

From this it follows that there are two type constraints for every declaration.

Example

Let’s take the factorial function in Oluś Zero:

fact n return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 m: fact m step2
        step2 f: mul n f return

It has five declarations, so we obtain ten equations:

\[ \begin{aligned} \typeof{\code{fact}} &= \par{ \typeof{\code{n}}, \typeof{\code{return}}} & \typeof{\code{isZero}} &= \par{ \typeof{\code{n}}, \typeof{\code{base}}, \typeof{\code{recurse}} }\\ \typeof{\code{base}} &= \par{}& \typeof{\code{return}} &= \par{ \code{Int} }\\ \typeof{\code{recurse}} &= \par{}& \typeof{\code{sub}} &= \par{ \typeof{\code{n}}, \code{Int}, \typeof{\code{step1}} }\\ \typeof{\code{step1}} &= \par{ \typeof{\code{m}} }& \typeof{\code{fact}} &= \par{ \typeof{\code{m}}, \typeof{\code{step2}} }\\ \typeof{\code{step2}} &= \par{ \typeof{\code{f}} }& \typeof{\code{mul}} &= \par{ \typeof{\code{n}}, \typeof{\code{f}}, \typeof{\code{return}}, }\\ \end{aligned} \]

This can be simplified by substitution:

\[ \begin{aligned} \typeof{\code{fact}} &= \par{ \typeof{\code{n}}, \par{\code{Int}} }& \typeof{\code{isZero}} &= \par{ \typeof{\code{n}}, \par{}, \par{} }\\ \typeof{\code{base}} &= \par{}& \typeof{\code{return}} &= \par{ \code{Int} }\\ \typeof{\code{recurse}} &= \par{}& \typeof{\code{sub}} &= \par{ \typeof{\code{n}}, \code{Int}, \par{\typeof{\code{m}}} }\\ \typeof{\code{step1}} &= \par{ \typeof{\code{m}} }& \typeof{\code{fact}} &= \par{ \typeof{\code{m}}, \par{\typeof{\code{f}}} }\\ \typeof{\code{step2}} &= \par{ \typeof{\code{f}} }& \typeof{\code{mul}} &= \par{ \typeof{\code{n}}, \typeof{\code{f}}, \par{\code{Int}} }\\ \end{aligned} \]

Observe that \(\typeof{\code{fact}}\) appears twice on the left-hand side. Equating the right-hand sides gives \(\typeof{\code{n}} = \typeof{\code{m}}\) and \(\typeof{\code{f}} = \code{Int}\).

\[ \begin{aligned} \typeof{\code{fact}} &= \par{ \typeof{\code{m}}, \par{\code{Int}} }& \typeof{\code{isZero}} &= \par{ \typeof{\code{m}}, \par{}, \par{} }\\ \typeof{\code{base}} &= \par{}& \typeof{\code{return}} &= \par{ \code{Int} }\\ \typeof{\code{recurse}} &= \par{}& \typeof{\code{sub}} &= \par{ \typeof{\code{m}}, \code{Int}, \par{\typeof{\code{m}}} }\\ \typeof{\code{step1}} &= \par{ \typeof{\code{m}} }& \typeof{\code{fact}} &= \par{ \typeof{\code{m}}, \code{Int} }\\ \typeof{\code{step2}} &= \par{ \code{Int} }& \typeof{\code{mul}} &= \par{ \typeof{\code{m}}, \code{Int}, \par{\code{Int}} }\\ \typeof{\code{n}} &= \typeof{\code{m}} & \typeof{\code{f}} &= \code{Int} \end{aligned} \]

We have only one variable left. But we did not yet include the types of the builtin functions, which are:

\[ \begin{aligned} \typeof{\code{isZero}} &= \par{ \code{Int}, \par{}, \par{} }\\ \typeof{\code{sub}} &= \par{ \code{Int}, \code{Int}, \par{\code{Int}} }\\ \typeof{\code{mul}} &= \par{ \code{Int}, \code{Int}, \par{\code{Int}} } \end{aligned} \]

With these included, it becomes clear that the types of all procedures and parameters are:

\[ \begin{aligned} \typeof{\code{fact}} &= \par{ \code{Int}, \par{\code{Int}} }& \typeof{\code{return}} &= \par{ \code{Int} }\\ \typeof{\code{base}} &= \par{} & \typeof{\code{recurse}} &= \par{} \\ \typeof{\code{step1}} &= \par{ \code{Int} } & \typeof{\code{step2}} &= \par{ \code{Int} } \\ \typeof{\code{n}} &= \code{Int} & \typeof{\code{m}} &= \code{Int} \\ \typeof{\code{f}} &= \code{Int} \end{aligned} \]

Our factorial function has now been satisfactory type-checked.

Types

Simple types

Example

Limitations

See also