<p>Ocaml <code>val</code> is never used in expressions, only in signatures. If your intent is to prescribe the type of a newly introduced variable, then you should do it when the variable is introduced, i.e., in <code>let</code>-binding:
<span class="math-container">$$\frac{\Gamma \vdash e_1 : A \qquad \Gamma, x : A \vdash e_2 : B}
  {\Gamma \vdash (\mathsf{let}\, x : A = e_1 \;\mathsf{in} e_2) : B}
$$</span>
An example in OCaml:</p>
<pre><code># let x : int list = [] ;;
val x : int list = []
</code></pre>
<p>(Without the annotation, OCaml would answer that the type of <code>x</code> is <code>'a list</code>.)</p>
<p>A related concept is <em>type ascription</em>, which prescribes the type of an expressions (not necessarily a variable):
<span class="math-container">$$\frac{\Gamma \vdash e : A \qquad \Gamma \vdash A = B}
  {\Gamma \vdash (e : A) : B}
$$</span>
An example in OCaml:</p>
<pre><code># fun x -&gt; ((x, x) : int * int) ;;
- : int -&gt; int * int = &lt;fun&gt;
</code></pre>
<p>(Without the ascription, Ocaml would infer the type <code>'a -&gt; 'a * 'a</code>.)</p>
<p>Just don't try to mix <code>val</code> and <code>let</code>.</p>

CC BY-SA 4.0
2023-04-19T20:27:58.923Z
2023-04-19T20:27:58.923Z
Andrej Bauer
<p><span class="math-container">$\newcommand{\clet}{\texttt{let }}
\newcommand{\cval}{\texttt{val }}
\newcommand{\cin}{\texttt{ in }}
$</span>I have the syntax for a programming language containing both let-bindings of the form <span class="math-container">$\clet x = e_1 \cin e_2$</span> and val-bindings of the form <span class="math-container">$\cval x : t \cin e$</span>.</p>
<p>I'd like to enforce that a <code>val</code>-binding is only well-formed
if <span class="math-container">$e$</span> contains a corresponding <code>let</code>-binding. My first thought was to use a typing rule like</p>
<p><span class="math-container">$$
\dfrac{\Gamma, \;\;\cval x : t \cin e \quad x \in BV(e)}
{\Gamma \vdash x : t} \quad\textsf{wf-val}
$$</span></p>
<p>but that doesn't enforce that <span class="math-container">$x$</span> appear in a <code>let</code>-binding - only as a variable that may be unbound, in which case the rule doesn't really work.</p>
<p>What would be the most idiomatic way to express this? One thing I considered was testing if a term of the form <span class="math-container">$\clet x = \dots$</span> appears as a subterm of <span class="math-container">$e$</span>, though ideally the rule would enforce that the matching <code>let</code> appears at the same level as the <code>val</code> (i.e. not in the body of a lambda).</p>

CC BY-SA 4.0
2023-04-19T19:30:37.403Z
What is `val` supposed to be, intuitively speaking? An un-initialized variable? The rule wf-val is very odd. Is it turned upside down? What is happening with $e$ in that rule?
Andrej Bauer
CC BY-SA 4.0
2023-04-19T19:55:55.227Z
Sorry if the question is unclear, `val` is basically a replacement for an explicit annotation term like `x: t`. The name comes the `val` keyword in OCaml which you use to give the type of an expression. I want to enforce that each type declaration with `val` actually accompanies a term but I'm not sure how to express it. That's not really a problem with `: t` syntax since the term being typed is part of the expression
llilibbou
CC BY-SA 4.0
2023-04-19T20:20:00.987Z
Ocaml `val` is *never* combined with expressions, it is always part of the *signature*. The concept you are looking for is *type ascription*, and it works for any expression, not just variables. In any case, the type of a variable should be introduced at the point where the variable is introduced, not in a random place before that.
Andrej Bauer
<type-theory><pl.programming-languages>
Typing rule for corresponding `val` and `let` bindings
llilibbou
# Typing rule for corresponding `val` and `let` bindings

(Asked by: username_0 on 2023-04-19)

$\newcommand{\clet}{\texttt{let }}
\newcommand{\cval}{\texttt{val }}
\newcommand{\cin}{\texttt{ in }}
$I have the syntax for a programming language containing both let-bindings of the form $\clet x = e\_1 \cin e\_2$ and val-bindings of the form $\cval x : t \cin e$.

I'd like to enforce that a `val`-binding is only well-formed
if $e$ contains a corresponding `let`-binding. My first thought was to use a typing rule like

$$
\dfrac{\Gamma, \;\;\cval x : t \cin e \quad x \in BV(e)}
{\Gamma \vdash x : t} \quad\textsf{wf-val}
$$

but that doesn't enforce that $x$ appear in a `let`-binding - only as a variable that may be unbound, in which case the rule doesn't really work.

What would be the most idiomatic way to express this? One thing I considered was testing if a term of the form $\clet x = \dots$ appears as a subterm of $e$, though ideally the rule would enforce that the matching `let` appears at the same level as the `val` (i.e. not in the body of a lambda).

**Tags:** type-theory, pl.programming-languages

> **Comments:**
> **username_1**: What is `val` supposed to be, intuitively speaking? An un-initialized variable? The rule wf-val is very odd. Is it turned upside down? What is happening with $e$ in that rule?  
> **username_0**: Sorry if the question is unclear, `val` is basically a replacement for an explicit annotation term like `x: t`. The name comes the `val` keyword in OCaml which you use to give the type of an expression. I want to enforce that each type declaration with `val` actually accompanies a term but I'm not sure how to express it. That's not really a problem with `: t` syntax since the term being typed is part of the expression  
> **username_1**: Ocaml `val` is *never* combined with expressions, it is always part of the *signature*. The concept you are looking for is *type ascription*, and it works for any expression, not just variables. In any case, the type of a variable should be introduced at the point where the variable is introduced, not in a random place before that.  

---

## 1 answers

### Answer by username_1 on 2023-04-19. Score: 0

Ocaml val is never used in expressions, only in signatures. If your intent is to prescribe the type of a newly introduced variable, then you should do it when the variable is introduced, i.e., in let-binding:
$$\frac{\Gamma \vdash e_1 : A \qquad \Gamma, x : A \vdash e_2 : B}
  {\Gamma \vdash (\mathsf{let}\, x : A = e_1 \;\mathsf{in} e_2) : B}
$$
An example in OCaml:
# let x : int list = [] ;;
val x : int list = []

(Without the annotation, OCaml would answer that the type of x is 'a list.)
A related concept is type ascription, which prescribes the type of an expressions (not necessarily a variable):
$$\frac{\Gamma \vdash e : A \qquad \Gamma \vdash A = B}
  {\Gamma \vdash (e : A) : B}
$$
An example in OCaml:
# fun x -> ((x, x) : int * int) ;;
- : int -> int * int = 

(Without the ascription, Ocaml would infer the type 'a -> 'a * 'a.)
Just don't try to mix val and let.


---

