The rules of a type system may be given in one of several ways.

We ususually begin by defining a relation "term $t$ has type $A$" using rules of inference, like the ones displayed in the question, without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and most amenable to mathematical treatment, such as semantics. If you're designing a new type system you'd probably start here in order to not get tangled up in various algorithmic details.

We then want an equivalent formulation that indicates how we are supposed to carry out type checking. This is sometimes called "algorithmic style".

One particular kind of algorthmic style are the "syntax directed rules" – by which we mean that we can tell which rule to use by analyzing the syntax of the term $t$ that we are trying to typecheck. This is good because it tells you how to implement typechecking. Most of the time most declarative rules are already syntax-directed – but in interesting cases there are always a couple that are not.

It takes experience to know how to get the algorithmic style from declarative style. In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy.

A popular way to formulate type systems in algorithmic style is to split the relation "$t$ has type $A$" into two:

• check that $t$ has the given type $A$, and
• infer (synthetsize, compute) the type of $t$

This is known as a bidirectional type system. The checking and inferring relations (also called phases) are often mutually recursive, and they are also syntax directed – so they give an algorithm. (In case it is not clear, the algorithm is to simply look at the syntactic structure of $t$ to find out which rule should be used, more or less.)

There are many other kinds of algorithms that perform type checking and type inference. For instance, they may collect a set of equational constraints that needs to be solved. Or they may track some other information. It is traditional for such algorithms to be displayed using inference rules (rather than pseudocode that looks like Algol 68). The accompanying text will tell you which bits are to be thought of as inputs and which as outputs, and the rules will be syntax-directed so that in each situation at most one will apply. (And if none apply, you've got a type error.)

To answer your question specifically: there are a number of techniques that turn inference rules into algorithms. What is appropriate in your case depends on what your type system look like. Have you written it down? In declarative style?

The rules of a type system may be given in one of several ways.

We often begin by defining a relation "term $t$ has type $A$" using rules of inference without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and most amenable to mathematical treatment, such as semantics. If you're designing a new type system you'd probably start here in order to not get tangled up in various algorithmic details.

We then want an equivalent formulation that indicates how we are supposed to carry out type checking. This is sometimes called "algorithmic style".

One particular kind of algorithmic style are the "syntax directed rules" – by which we mean that we can tell which rule to use by analyzing the syntax of the term $t$ that we are trying to typecheck. This is good because it tells you how to implement typechecking. Most of the time most declarative rules are already syntax-directed – but in interesting cases there are always a couple that are not.

It takes experience to know how to design an algorithmic style that correspond to a given declarative style. In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy.

A popular way to formulate type systems in algorithmic style is to split the relation "$t$ has type $A$" into two:

• check that $t$ has the given type $A$, and
• infer (synthesize, compute) the type of $t$

This is known as a bidirectional type system. The checking and inferring relations (also called phases) are often mutually recursive, and they are also syntax directed – so they give an algorithm. (In case it is not clear, the algorithm is simply to look at the syntactic structure of $t$ to find out which rule should be used, more or less.)

There are many other kinds of algorithms that perform type checking and type inference. For instance, they may collect a set of equational constraints that needs to be solved. Or they may track some other information. It is traditional for such algorithms to be displayed using inference rules (rather than pseudocode that looks like Algol 68). The accompanying text will tell you which bits are to be thought of as inputs and which as outputs, and the rules will be syntax-directed so that in each situation at most one will apply. (And if none apply, you've got a type error.)

To answer your question specifically: there are a number of techniques that turn inference rules into algorithms. What is appropriate in your case depends on what your type system look like. Have you written it down? In declarative style?

The rules of a type system may be given in one of several ways.

We ususually begin by defining a relation "term $t$ has type $A$" using rules of inference, like the ones displayed in the question, without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and most amenable to mathematical treatment, such as semantics. If you're designing a new type system you'd probably start here in order to not get tangled up in various algorithmic details.

We then want an equivalent formulation that indicates how we are supposed to carry out type checking. This is sometimes called "algorithmic style".

One particular kind of algorthmic style are the "syntax directed rules" – by which we mean that we can tell which rule to use by analyzing the syntax of the term $t$ that we are trying to typecheck. This is good because it tells you how to implement typechecking. Most of the time most declarative rules are already syntax-directed – but in interesting cases there are always a couple that are not.

It takes experience to know how to get the algorithmic style from declarative style. In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy.

A popular way to formulate type systems in algorithmic style is to split the relation "$t$ has type $A$" into two:

• check that $t$ has the given type $A$, and
• infer (synthetsize, compute) the type of $t$

This is known as a bidirectional type system. The checking and inferring relations (also called phases) are often mutually recursive, and they are also syntax directed – so they give an algorithm. (In case it is not clear, the algorithm is to simply look at the syntactic structure of $t$ to find out which rule should be used, more or less.)

There are many other kinds of algorithms that perform type checking and type inference. For instance, they may collect a set of equational constraints that needs to be solved. Or they may track some other information. It is traditional for such algorithms to be displayed using inference rules (rather than pseudocode that looks like Algol 68). The accompanying text will tell you which bits are to be thought as inputs and which as outputs, and the rules will be syntax-directed so that in each situation at most one will apply. (And if none apply, you've got a type error.)

To answer your question specifically: there are a number of techniques that turn inference rules into algorithms. What is appropriate in your case depends on what your type system look like. Have you written it down? In declarative style?

The rules of a type system may be given in one of several ways.

We ususually begin by defining a relation "term $t$ has type $A$" using rules of inference, like the ones displayed in the question, without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and most amenable to mathematical treatment, such as semantics. If you're designing a new type system you'd probably start here in order to not get tangled up in various algorithmic details.

We then want an equivalent formulation that indicates how we are supposed to carry out type checking. This is sometimes called "algorithmic style".

One particular kind of algorthmic style are the "syntax directed rules" – by which we mean that we can tell which rule to use by analyzing the syntax of the term $t$ that we are trying to typecheck. This is good because it tells you how to implement typechecking. Most of the time most declarative rules are already syntax-directed – but in interesting cases there are always a couple that are not.

It takes experience to know how to get the algorithmic style from declarative style. In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy.

A popular way to formulate type systems in algorithmic style is to split the relation "$t$ has type $A$" into two:

• check that $t$ has the given type $A$, and
• infer (synthetsize, compute) the type of $t$

This is known as a bidirectional type system. The checking and inferring relations (also called phases) are often mutually recursive, and they are also syntax directed – so they give an algorithm. (In case it is not clear, the algorithm is to simply look at the syntactic structure of $t$ to find out which rule should be used, more or less.)

There are many other kinds of algorithms that perform type checking and type inference. For instance, they may collect a set of equational constraints that needs to be solved. Or they may track some other information. It is traditional for such algorithms to be displayed using inference rules (rather than pseudocode that looks like Algol 68). The accompanying text will tell you which bits are to be thought of as inputs and which as outputs, and the rules will be syntax-directed so that in each situation at most one will apply. (And if none apply, you've got a type error.)

To answer your question specifically: there are a number of techniques that turn inference rules into algorithms. What is appropriate in your case depends on what your type system look like. Have you written it down? In declarative style?