<p><a href="https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/2693#2693">Answer #2693</a> introduces the notation of typing rules. That answer shows typing rules for a simple language in which all types are primitive, i.e., built into the language. Other similarly beginner-oriented materials that introduce such rules, such as <a href="https://cs3110.github.io/textbook/chapters/interp/typecheck.html" rel="noreferrer"><i>OCaml Programming: Correct + Efficient + Beautiful</i> §9.5</a>, tend also to use such simple example languages, such that I do not find examples of how typing rules look when they must permit product types and sum types defined in users' library code. <strong>What are, or where can be found, some examples of typing rules supporting arbitrary user-defined product types and sum types?</strong></p>

<types><static-typing><type-systems>
How do typing rules look if most types are user-defined?
CC BY-SA 4.0
2024-07-30T23:36:37.720Z
You should look at [*Types and Programming Languages*](https://www.cis.upenn.edu/~bcpierce/tapl/), specifically Chapter 11 on simple extensions to the simply-typed lambda calculus.
apropos
CC BY-SA 4.0
2024-07-31T02:11:04.007Z
My immediate thought is to go to W types, which generalise the concept of an inductive type (like an ADT) into one structure (therefore allowing you to just formalise that one structure instead of every possible user type), but AFAIK those require some indexing stuff that might only really make sense in a dependent context.
blueberry
<p>Funny, I remember also having this question when I was first learning how types systems work.</p>
<p>The short answer is they look pretty similar. I'll give an example somewhat taken from <a href="https://www.cis.upenn.edu/%7Ebcpierce/tapl/" rel="nofollow noreferrer"><em>Types and Programming Languages</em></a>, which is an excellent reference work for this sort of thing.
Please consider this to be extending the system laid out in <a href="https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/2693#2693">Alexis King's guide to type system notation</a>.</p>
<p>Let's consider a slightly more complicated language.</p>
<h2>Products</h2>
<p>We extend the syntax for products as such.</p>
<p><span class="math-container">$$
\begin{array}{rcll}
e \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}...\\
  &amp; | &amp;\hskip{-10mu} (e,e) &amp;\textrm{pairs}\\
  &amp; | &amp;\hskip{-10mu} \textbf{car}\ e &amp;\textrm{left projection}\\
  &amp; | &amp;\hskip{-10mu} \textbf{cdr}\ e &amp;\textrm{right projection}\\[8pt]
τ \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}...\\
  &amp; | &amp;\hskip{-10mu} τ \times τ &amp;\textrm{products}
\end{array}
$$</span></p>
<p>Here, we are restricting ourselves to a limited form of products: <em>pairs</em>. There are other types that can be interpreted as a product - structs, tuples, records (if you draw such a distinction)... but I'm sticking with pairs as they are the simplest to work with. (If you are interested in other minutely different systems, check out TAPL.)</p>
<p>Historically left and right projection is known as &quot;car&quot; and &quot;cdr&quot; respectively (from Lisp - <a href="https://en.wikipedia.org/wiki/CAR_and_CDR#Etymology" rel="nofollow noreferrer">etymology</a>): though in languages with infix notation you will more commonly see something like <span class="math-container">$e.1$</span> or <span class="math-container">$e[1]$</span>. I have bolded <span class="math-container">$\textbf{car}$</span> and <span class="math-container">$\textbf{cdr}$</span> above to emphasize that they are <em>destructors</em>. They are taking in a pair, and <em>deconstructing</em> it: <span class="math-container">$\text{car}\ (e_1, e_2)$</span> gives you <span class="math-container">$e_1$</span>, and <span class="math-container">$\text{cdr}\ (e_1, e_2)$</span> gives you <span class="math-container">$e_2$</span>. On the other hand, <span class="math-container">$(e_1, e_2)$</span> is a <em>constructor</em>: it is returning a pair.</p>
<p>But on to the typing rules. They are as follows:</p>
<p><span class="math-container">$$
\begin{array}{l}
Γ ⊢ e : τ_1 × τ_2 \\
\hline
\hskip{5mu}
Γ ⊢ \text{car}\ e : τ_1
\end{array}
\quad \quad
\begin{array}{l}
Γ ⊢ e : τ_1 × τ_2 \\
\hline
\hskip{5mu} 
Γ ⊢ \text{cdr}\ e : τ_2
\end{array}
$$</span></p>
<p><span class="math-container">$$
\begin{array}{l}
Γ ⊢ e_1 : τ_1
\hskip{25mu} 
Γ ⊢ e_2 : τ_2 \\  
\hline
\hskip{20mu} 
Γ ⊢ (e_1, e_2) : τ_1 × τ_2
\end{array}
$$</span></p>
<p>These look pretty similar to function types, with their <span class="math-container">$τ_1$</span> and <span class="math-container">$τ_2$</span> type variables. Indeed, they can be thought of as <em>user-definable</em> in the same way. Just like one can define an arbitrary amount of function types of the form <span class="math-container">$τ_1 → τ_2$</span>, one can <em>also</em> define an arbitrary amount of product types of the form <span class="math-container">$τ_1 × τ_2$</span>.</p>
<p>But what about product types with more than two entries?</p>
<p>There are two approaches that can be taken. One, stick with our binary product types, treat <span class="math-container">$τ_1 × (τ_2 × τ_3)$</span> as <span class="math-container">$τ_1 × τ_2 × τ_3$</span> by convention, and define <em>syntactic sugar</em> for direct field access (<span class="math-container">$e.1, e.2, e.3$</span>) that desugars to the more formally-specified <span class="math-container">$\text{car}$</span> and <span class="math-container">$\text{cdr}$</span> deconstructors. This is a perfectly valid approach. Two, use an <em>extension</em> of standard type system notation to explicitly specify semantics for products of arbitrary size. This is somewhat of a bad idea: it is much easier to reason about typing rules when you have a finite set of constructors and destructors. To quote TAPL: <em>&quot;such notations [of arbitrary arity] are always a bit problematic, as there is some inevitable tension between rigor and readability&quot;</em>.</p>

<p>But what if we wanted to label the entries of our product types?</p>
<p>Again, we should consider <em>why</em> we want to deal with this in our typing rules. It is perhaps a better idea to not. But, a valid approach would be to define a new class of <em>labels</em>: <span class="math-container">$l ::= l_i \in \mathcal{L}^{i \in 1..n}$</span> for some <span class="math-container">$n$</span>, and extend our typing rules with them. (This notation is arbitrary. I am not aware of any standard notation.)</p>
<h2>Sums</h2>
<p>Now let us consider sum types. These are a little more confusing.</p>
<p><span class="math-container">$$
\begin{array}{rcll}
e \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}...\\
  &amp; | &amp;\hskip{-10mu} \text{inl}\ e &amp;\textrm{left tag}\\
  &amp; | &amp;\hskip{-10mu} \text{inr}\ e &amp;\textrm{right tag}\\
  &amp; | &amp;\hskip{-10mu} \textbf{case}\ e\ &amp;\textrm{case} \\
  &amp;   &amp; \textbf{of}\ \text{inl}\ x ⇒ e\\
  &amp;   &amp; \textbf{of}\ \text{inr}\ x ⇒ e\\[8pt]
τ \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}...\\
  &amp; | &amp;\hskip{-10mu} τ + τ &amp;\textrm{sums}
\end{array}
$$</span></p>
<p>You will notice the <span class="math-container">$\text{inl}$</span> and <span class="math-container">$\text{inr}$</span> constructors. Those probably don't look like anything you've seen before. That is because we are similarly restricting ourselves to a limited form of sums here: our sums here may <em>only</em> be identified by the &quot;left&quot; and &quot;right&quot; tags. (<span class="math-container">$\text{inl}$</span> and <span class="math-container">$\text{inr}$</span> come from &quot;injection&quot; + &quot;left&quot; / &quot;right&quot;.)</p>
<p>The <span class="math-container">$\text{case}$</span> statement should provide a hint as to how they are used: our case expression explicitly is defined for <em>fixed</em> tags: instead of user-defined tags (ex. <code>Just</code>, <code>Nothing</code>, <code>Some</code>...) common in real-world languages with sum types. This means our constructors (and destructors) are finite, and so we do not need to extend the type system notation itself. And in a similar fashion to our treatment of products of arbitrary-arity above, we can treat <span class="math-container">$τ_1 + (τ_2 + τ_3)$</span> as <span class="math-container">$τ_1 + τ_2 + τ_3$</span> by convention, and define syntactic sugar atop.</p>
<p>Our typing rules are as follows:</p>
<p><span class="math-container">$$
\begin{array}{l}
\hskip{30mu} 
Γ ⊢ e : τ_1 \\
\hline
Γ ⊢ \text{inl}\ e : τ_1 + τ_2
\end{array}
\quad \quad
\begin{array}{l}
\hskip{30mu} 
Γ ⊢ e : τ_2 \\
\hline
Γ ⊢ \text{inr}\ e : τ_1 + τ_2
\end{array}
$$</span></p>
<p><span class="math-container">$$
\begin{array}{l}
\hskip{100mu}
Γ ⊢ e : τ_1 + τ_2 \\
\hskip{25mu}
Γ,x_1 : τ_1 ⊢ e_1 : τ 
\hskip{25mu} 
Γ,x_2 : τ_2 ⊢ e_2 : τ \\  
\hline
Γ ⊢ \text{case}\ e\ \text{of}\ \text{inl}\ x_1 ⇒ e_1\ \text{of}\ \text{inr}\ x_2 ⇒ e_2 : τ
\end{array}
$$</span></p>
<p>There are a few items of note here. <span class="math-container">$\text{case}$</span> is deconstructing some term of type <span class="math-container">$τ_1 + τ_2$</span> into a third type <span class="math-container">$τ$</span>. This is necessary in order for the case expression to be of a consistent type. Also, the rules for the <span class="math-container">$\text{inl}$</span> and <span class="math-container">$\text{inr}$</span> constructors introduce new types <span class="math-container">$τ_2$</span> and <span class="math-container">$τ_1$</span> not previously introduced above the bar: these are arbitrary types and are in practice necessarily determined by explicit type annotations.</p>

CC BY-SA 4.0
2024-07-31T08:11:07.597Z
2024-07-31T08:19:17.723Z
2024-07-31T08:19:17.723Z
apropos
<p>You store user-defined data types in the context as bindings for types and values; you then look up value constructors when they occur in expressions similarly to how you look up let-bound variables in the context when they are used.</p>
<p>A full example is <a href="https://smlfamily.github.io/sml97-defn.pdf" rel="nofollow noreferrer">The Definition of Standard ML</a> by Milner et al..  Inference rules are on pages 23-31 (pages 37-45 of the PDF). The types of the metavariables (C for contexts, TE for type environments, VE for value environments, etc.) are given on page 18, and the rest of Chapter 4 defines the operations and notations used in inference rules.</p>
<p>When you define a data type,</p>
<pre><code>datatype my_ty = MyCon of int
</code></pre>
<p>the identifiers <code>my_ty</code> and <code>MyCon</code> are respectively introduced in the type environment and value environment. This involves two declaration-level rules, simplified below (pages 26-27): rule 17 generates bindings from a single datatype declaration, and rule 24 accumulates the bindings from one declaration to typecheck the subsequent declaration(s):</p>
<p><span class="math-container">$$
\begin{array}{c}
C \oplus \mathit{TE} \vdash \mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE}
\\ \hline
C \vdash \mathbf{datatype}\;\mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE} \;\;\mathrm{in}\;\mathit{Env}
\end{array} (17)
$$</span></p>
<p><span class="math-container">$$
\begin{array}{c}
C \vdash \mathit{dec}_1 \Rightarrow E_1 \quad C \oplus E_1 \vdash \mathit{dec}_2 \Rightarrow E_2
\\ \hline
C \vdash \mathit{dec}_1;\mathit{dec}_2 \Rightarrow E_1 \oplus E_2
\end{array} (24)
$$</span></p>
<p>The following rule shows how one of those bindings is generated. A data type declaration introduces <em>value constructors</em>, which are basically functions. For example, the clause <code>MyCon of int</code> above introduces a constructor <code>MyCon</code> of type <code>t0 -&gt; my_ty</code>. This is handled by rule 29, where the resulting binding is <span class="math-container">$\{\mathit{tid} \mapsto (\tau'\to\tau, \mathtt{c})\}$</span>---it is a map with key <span class="math-container">$\mathit{tid}$</span> and associated value <span class="math-container">$(\tau'\to\tau, \mathtt{c})$</span>. The binding also contains a tag <span class="math-container">$\mathtt{c}$</span> to remember that <code>MyCon</code> is a constructor, as opposed to a plain value. In ML, constructors are either nullary or unary. For brevity, we only consider unary constructors:</p>
<p><span class="math-container">$$
\begin{array}{c}
C \vdash \mathit{ty} \Rightarrow \tau'
\\ \hline
C, \tau \vdash \mathit{tid}\;\mathtt{of}\;\mathit{ty} \Rightarrow \{\mathit{tid}\mapsto (\tau'\to\tau, \mathtt{c})\}
\end{array} (29)
$$</span></p>
<p>Constructors can be used in expressions in two ways: as values, and in patterns to decompose values. As values, we use the same rule for constructors as for regular (let-bound) values (rule 2). In words: to infer the type of <span class="math-container">$\mathit{longvid}$</span> in context <span class="math-container">$C$</span>, look up the identifier <span class="math-container">$\mathit{longvid}$</span> in <span class="math-container">$C$</span>, it should be bound to some type scheme <span class="math-container">$\sigma$</span>, monomorphize it to <span class="math-container">$\tau$</span>.</p>
<p><span class="math-container">$$
\begin{array}{c}
C(\mathit{longvid}) = \sigma \quad \sigma \succ \tau
\\ \hline
C \vdash \mathit{longvid} \Rightarrow \tau
\end{array} (2)
$$</span></p>
<p>Patterns occur in lambdas (anonymous functions). The typing rule for lambdas is rule 12; lambdas are sequences of matches (rule 13), where a match is of the form <code>pat =&gt; exp</code> (rule 14). The last relevant rule is the rule for constructors in patterns, rule 41 below (or rule 35 for nullary constructors). For example, in the expression <code>fn MyCon(x) =&gt; x</code>,  the pattern <code>MyCon(x)</code> would be typed by an instance of this rule with <code>MyCon</code> as <span class="math-container">$\mathit{longvid}$</span> and <code>(x)</code> as <span class="math-container">$\mathit{atpat}$</span>. The condition <span class="math-container">$\mathit{is}\neq \mathtt{v}$</span> ensures that <span class="math-container">$\mathit{longvid}$</span> is not a regular value; the tag <span class="math-container">$\mathit{is}$</span> must be either <span class="math-container">$\mathtt{c}$</span> or <span class="math-container">$\mathtt{e}$</span> (for exceptions, which behave like constructors). <span class="math-container">$\mathit{longvid}\;\mathit{atpat}$</span> has type <span class="math-container">$\tau$</span> when <span class="math-container">$\mathit{longvid}$</span> has type <span class="math-container">$\tau'\to\tau$</span> and <span class="math-container">$\mathit{atpat}$</span> has type <span class="math-container">$\tau'$</span>. (The <span class="math-container">$\mathit{VE}$</span> in the result contains the variables bound by the pattern, like <code>x</code> in <code>MyCon(x)</code>.)</p>
<p><span class="math-container">$$
\begin{array}{c}
C(\mathit{longvid}) = (\sigma, \mathit{is}) \quad \mathit{is} \neq \mathtt{v} \quad \sigma\succ \tau' \to \tau \quad C\vdash \mathit{atpat} \Rightarrow (\mathit{VE}, \tau')
\\ \hline
C \vdash \mathit{longvid}\;\mathit{atpat} \Rightarrow (\mathit{VE},\tau)
\end{array} (41)
$$</span></p>

CC BY-SA 4.0
2024-08-06T18:30:00.187Z
2024-08-06T19:28:15.487Z
2024-08-06T19:28:15.487Z
Li-yao Xia
# How do typing rules look if most types are user-defined?
Posted by: username_0 on 2024-07-30
[Answer #2693](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/2693#2693) introduces the notation of typing rules. That answer shows typing rules for a simple language in which all types are primitive, i.e., built into the language. Other similarly beginner-oriented materials that introduce such rules, such as [*OCaml Programming: Correct + Efficient + Beautiful* §9.5](https://cs3110.github.io/textbook/chapters/interp/typecheck.html), tend also to use such simple example languages, such that I do not find examples of how typing rules look when they must permit product types and sum types defined in users' library code. **What are, or where can be found, some examples of typing rules supporting arbitrary user-defined product types and sum types?**
**Tags:** types static-typing type-systems
> **Comments:**
> **username_1**: You should look at [*Types and Programming Languages*](https://www.cis.upenn.edu/~bcpierce/tapl/), specifically Chapter 11 on simple extensions to the simply-typed lambda calculus.  
> **username_2**: My immediate thought is to go to W types, which generalise the concept of an inductive type (like an ADT) into one structure (therefore allowing you to just formalise that one structure instead of every possible user type), but AFAIK those require some indexing stuff that might only really make sense in a dependent context.  
---
## 2 answers
### Answer by username_1 on 2024-07-31. Score: 3
Funny, I remember also having this question when I was first learning how types systems work.

The short answer is they look pretty similar. I'll give an example somewhat taken from [*Types and Programming Languages*](https://www.cis.upenn.edu/%7Ebcpierce/tapl/), which is an excellent reference work for this sort of thing.
Please consider this to be extending the system laid out in [Alexis King's guide to type system notation](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/2693#2693).

Let's consider a slightly more complicated language.

## Products

We extend the syntax for products as such.

$$
\begin{array}{rcll}
e \hskip{-10mu}
&::=&\hskip{-10mu}...\\
& | &\hskip{-10mu} (e,e) &\textrm{pairs}\\
& | &\hskip{-10mu} \textbf{car}\ e &\textrm{left projection}\\
& | &\hskip{-10mu} \textbf{cdr}\ e &\textrm{right projection}\\[8pt]
τ \hskip{-10mu}
&::=&\hskip{-10mu}...\\
& | &\hskip{-10mu} τ \times τ &\textrm{products}
\end{array}
$$

Here, we are restricting ourselves to a limited form of products: *pairs*. There are other types that can be interpreted as a product - structs, tuples, records (if you draw such a distinction)... but I'm sticking with pairs as they are the simplest to work with. (If you are interested in other minutely different systems, check out TAPL.)

Historically left and right projection is known as "car" and "cdr" respectively (from Lisp - [etymology](https://en.wikipedia.org/wiki/CAR_and_CDR#Etymology)): though in languages with infix notation you will more commonly see something like $e.1$ or $e[1]$. I have bolded $\textbf{car}$ and $\textbf{cdr}$ above to emphasize that they are *destructors*. They are taking in a pair, and *deconstructing* it: $\text{car}\ (e\_1, e\_2)$ gives you $e\_1$, and $\text{cdr}\ (e\_1, e\_2)$ gives you $e\_2$. On the other hand, $(e\_1, e\_2)$ is a *constructor*: it is returning a pair.

But on to the typing rules. They are as follows:

$$
\begin{array}{l}
Γ ⊢ e : τ\_1 × τ\_2 \\
\hline
\hskip{5mu}
Γ ⊢ \text{car}\ e : τ\_1
\end{array}
\quad \quad
\begin{array}{l}
Γ ⊢ e : τ\_1 × τ\_2 \\
\hline
\hskip{5mu}
Γ ⊢ \text{cdr}\ e : τ\_2
\end{array}
$$

$$
\begin{array}{l}
Γ ⊢ e\_1 : τ\_1
\hskip{25mu}
Γ ⊢ e\_2 : τ\_2 \\
\hline
\hskip{20mu}
Γ ⊢ (e\_1, e\_2) : τ\_1 × τ\_2
\end{array}
$$

These look pretty similar to function types, with their $τ\_1$ and $τ\_2$ type variables. Indeed, they can be thought of as *user-definable* in the same way. Just like one can define an arbitrary amount of function types of the form $τ\_1 → τ\_2$, one can *also* define an arbitrary amount of product types of the form $τ\_1 × τ\_2$.

But what about product types with more than two entries?

There are two approaches that can be taken. One, stick with our binary product types, treat $τ\_1 × (τ\_2 × τ\_3)$ as $τ\_1 × τ\_2 × τ\_3$ by convention, and define *syntactic sugar* for direct field access ($e.1, e.2, e.3$) that desugars to the more formally-specified $\text{car}$ and $\text{cdr}$ deconstructors. This is a perfectly valid approach. Two, use an *extension* of standard type system notation to explicitly specify semantics for products of arbitrary size. This is somewhat of a bad idea: it is much easier to reason about typing rules when you have a finite set of constructors and destructors. To quote TAPL: *"such notations [of arbitrary arity] are always a bit problematic, as there is some inevitable tension between rigor and readability"*.

But what if we wanted to label the entries of our product types?

Again, we should consider *why* we want to deal with this in our typing rules. It is perhaps a better idea to not. But, a valid approach would be to define a new class of *labels*: $l ::= l\_i \in \mathcal{L}^{i \in 1..n}$ for some $n$, and extend our typing rules with them. (This notation is arbitrary. I am not aware of any standard notation.)

## Sums

Now let us consider sum types. These are a little more confusing.

$$
\begin{array}{rcll}
e \hskip{-10mu}
&::=&\hskip{-10mu}...\\
& | &\hskip{-10mu} \text{inl}\ e &\textrm{left tag}\\
& | &\hskip{-10mu} \text{inr}\ e &\textrm{right tag}\\
& | &\hskip{-10mu} \textbf{case}\ e\ &\textrm{case} \\
& & \textbf{of}\ \text{inl}\ x ⇒ e\\
& & \textbf{of}\ \text{inr}\ x ⇒ e\\[8pt]
τ \hskip{-10mu}
&::=&\hskip{-10mu}...\\
& | &\hskip{-10mu} τ + τ &\textrm{sums}
\end{array}
$$

You will notice the $\text{inl}$ and $\text{inr}$ constructors. Those probably don't look like anything you've seen before. That is because we are similarly restricting ourselves to a limited form of sums here: our sums here may *only* be identified by the "left" and "right" tags. ($\text{inl}$ and $\text{inr}$ come from "injection" + "left" / "right".)

The $\text{case}$ statement should provide a hint as to how they are used: our case expression explicitly is defined for *fixed* tags: instead of user-defined tags (ex. `Just`, `Nothing`, `Some`...) common in real-world languages with sum types. This means our constructors (and destructors) are finite, and so we do not need to extend the type system notation itself. And in a similar fashion to our treatment of products of arbitrary-arity above, we can treat $τ\_1 + (τ\_2 + τ\_3)$ as $τ\_1 + τ\_2 + τ\_3$ by convention, and define syntactic sugar atop.

Our typing rules are as follows:

$$
\begin{array}{l}
\hskip{30mu}
Γ ⊢ e : τ\_1 \\
\hline
Γ ⊢ \text{inl}\ e : τ\_1 + τ\_2
\end{array}
\quad \quad
\begin{array}{l}
\hskip{30mu}
Γ ⊢ e : τ\_2 \\
\hline
Γ ⊢ \text{inr}\ e : τ\_1 + τ\_2
\end{array}
$$

$$
\begin{array}{l}
\hskip{100mu}
Γ ⊢ e : τ\_1 + τ\_2 \\
\hskip{25mu}
Γ,x\_1 : τ\_1 ⊢ e\_1 : τ
\hskip{25mu}
Γ,x\_2 : τ\_2 ⊢ e\_2 : τ \\
\hline
Γ ⊢ \text{case}\ e\ \text{of}\ \text{inl}\ x\_1 ⇒ e\_1\ \text{of}\ \text{inr}\ x\_2 ⇒ e\_2 : τ
\end{array}
$$

There are a few items of note here. $\text{case}$ is deconstructing some term of type $τ\_1 + τ\_2$ into a third type $τ$. This is necessary in order for the case expression to be of a consistent type. Also, the rules for the $\text{inl}$ and $\text{inr}$ constructors introduce new types $τ\_2$ and $τ\_1$ not previously introduced above the bar: these are arbitrary types and are in practice necessarily determined by explicit type annotations.
---
### Answer by username_3 on 2024-08-06. Score: 3
You store user-defined data types in the context as bindings for types and values; you then look up value constructors when they occur in expressions similarly to how you look up let-bound variables in the context when they are used.
A full example is The Definition of Standard ML by Milner et al..  Inference rules are on pages 23-31 (pages 37-45 of the PDF). The types of the metavariables (C for contexts, TE for type environments, VE for value environments, etc.) are given on page 18, and the rest of Chapter 4 defines the operations and notations used in inference rules.
When you define a data type,
datatype my_ty = MyCon of int

the identifiers my_ty and MyCon are respectively introduced in the type environment and value environment. This involves two declaration-level rules, simplified below (pages 26-27): rule 17 generates bindings from a single datatype declaration, and rule 24 accumulates the bindings from one declaration to typecheck the subsequent declaration(s):
$$
\begin{array}{c}
C \oplus \mathit{TE} \vdash \mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE}
\\ \hline
C \vdash \mathbf{datatype}\;\mathit{datbind} \Rightarrow \mathit{VE},\mathit{TE} \;\;\mathrm{in}\;\mathit{Env}
\end{array} (17)
$$
$$
\begin{array}{c}
C \vdash \mathit{dec}_1 \Rightarrow E_1 \quad C \oplus E_1 \vdash \mathit{dec}_2 \Rightarrow E_2
\\ \hline
C \vdash \mathit{dec}_1;\mathit{dec}_2 \Rightarrow E_1 \oplus E_2
\end{array} (24)
$$
The following rule shows how one of those bindings is generated. A data type declaration introduces value constructors, which are basically functions. For example, the clause MyCon of int above introduces a constructor MyCon of type t0 -> my_ty. This is handled by rule 29, where the resulting binding is $\{\mathit{tid} \mapsto (\tau'\to\tau, \mathtt{c})\}$---it is a map with key $\mathit{tid}$ and associated value $(\tau'\to\tau, \mathtt{c})$. The binding also contains a tag $\mathtt{c}$ to remember that MyCon is a constructor, as opposed to a plain value. In ML, constructors are either nullary or unary. For brevity, we only consider unary constructors:
$$
\begin{array}{c}
C \vdash \mathit{ty} \Rightarrow \tau'
\\ \hline
C, \tau \vdash \mathit{tid}\;\mathtt{of}\;\mathit{ty} \Rightarrow \{\mathit{tid}\mapsto (\tau'\to\tau, \mathtt{c})\}
\end{array} (29)
$$
Constructors can be used in expressions in two ways: as values, and in patterns to decompose values. As values, we use the same rule for constructors as for regular (let-bound) values (rule 2). In words: to infer the type of $\mathit{longvid}$ in context $C$, look up the identifier $\mathit{longvid}$ in $C$, it should be bound to some type scheme $\sigma$, monomorphize it to $\tau$.
$$
\begin{array}{c}
C(\mathit{longvid}) = \sigma \quad \sigma \succ \tau
\\ \hline
C \vdash \mathit{longvid} \Rightarrow \tau
\end{array} (2)
$$
Patterns occur in lambdas (anonymous functions). The typing rule for lambdas is rule 12; lambdas are sequences of matches (rule 13), where a match is of the form pat => exp (rule 14). The last relevant rule is the rule for constructors in patterns, rule 41 below (or rule 35 for nullary constructors). For example, in the expression fn MyCon(x) => x,  the pattern MyCon(x) would be typed by an instance of this rule with MyCon as $\mathit{longvid}$ and (x) as $\mathit{atpat}$. The condition $\mathit{is}\neq \mathtt{v}$ ensures that $\mathit{longvid}$ is not a regular value; the tag $\mathit{is}$ must be either $\mathtt{c}$ or $\mathtt{e}$ (for exceptions, which behave like constructors). $\mathit{longvid}\;\mathit{atpat}$ has type $\tau$ when $\mathit{longvid}$ has type $\tau'\to\tau$ and $\mathit{atpat}$ has type $\tau'$. (The $\mathit{VE}$ in the result contains the variables bound by the pattern, like x in MyCon(x).)
$$
\begin{array}{c}
C(\mathit{longvid}) = (\sigma, \mathit{is}) \quad \mathit{is} \neq \mathtt{v} \quad \sigma\succ \tau' \to \tau \quad C\vdash \mathit{atpat} \Rightarrow (\mathit{VE}, \tau')
\\ \hline
C \vdash \mathit{longvid}\;\mathit{atpat} \Rightarrow (\mathit{VE},\tau)
\end{array} (41)
$$
---
