Type System

FPy is not statically typed. A program runs (see Language Semantics) without any type-checking, and every value carries its rounding context at run time. Static types enter only when compiling a program to a strongly-typed target, such as C++: the compiler infers a static type for each expression, and a program must type-check to be compiled — even though an ill-typed program may still run under the dynamic semantics.

This page gives the typing rules for the same core fragment as Language Semantics. The types here are context-free: a real number has type \(\texttt{real}\), with no rounding context attached. To emit code for a typed target, a separate pass refines each \(\texttt{real}\) with the rounding context it is produced under (so the backend can pick a concrete machine type — float, double, a fixed-point format, and so on). That refinement is out of scope here.

Types

The scalar types mirror the three scalar value kinds — booleans, real numbers, and rounding contexts — and are joined by list, tuple, and function types.

\[T ::= \texttt{bool} \mid \texttt{real} \mid \texttt{context} \mid \texttt{list}\ T \mid T_1 \times \cdots \times T_n \mid T_1 \rightarrow T_2\]

The real rounding context \(\R\) has type \(\texttt{context}\). Function symbols are assigned a function type \(T_1 \rightarrow T_2\).

Typing

Typing is the judgement \(\Gamma \vdash e : T\), read “under typing context \(\Gamma\), expression \(e\) has type \(T\)”. \(\Gamma\) assigns each variable a single type and is the solution of whole-function type inference — computed by unification, so library functions may be polymorphic. The rules below present the monomorphic case and state when a program agrees with that solution; statement well-formedness is written \(\Gamma \vdash s\ \texttt{ok}\). Because \(\Gamma\) is fixed, typing checks a program against it rather than building it up statement by statement.

Expressions

Constants have their scalar types; a variable has the type \(\Gamma\) assigns it.

\[\frac{}{\Gamma \vdash \texttt{true} : \texttt{bool}} \tag{T-True}\]

\[\frac{}{\Gamma \vdash \texttt{false} : \texttt{bool}} \tag{T-False}\]

\[\frac{}{\Gamma \vdash n : \texttt{real}} \tag{T-Num}\]

\[\frac{}{\Gamma \vdash \R : \texttt{context}} \tag{T-Real}\]

\[\frac{x : T \in \Gamma}{\Gamma \vdash x : T} \tag{T-Var}\]

A list is homogeneous; indexing recovers the element type. A tuple’s type records each component.

\[\frac{\Gamma \vdash e_1 : T \quad \cdots \quad \Gamma \vdash e_n : T} {\Gamma \vdash [\, e_1, \ldots, e_n \,] : \texttt{list}\ T} \tag{T-List}\]

\[\frac{\Gamma \vdash e_1 : \texttt{list}\ T \quad \Gamma \vdash e_2 : \texttt{real}} {\Gamma \vdash e_1[e_2] : T} \tag{T-Ref}\]

\[\frac{\Gamma \vdash e_1 : T_1 \quad \cdots \quad \Gamma \vdash e_n : T_n} {\Gamma \vdash (\, e_1, \ldots, e_n \,) : T_1 \times \cdots \times T_n} \tag{T-Tuple}\]

As in Language Semantics, + and < are representatives: arithmetic maps reals to a real, and comparison maps reals to a boolean.

\[\frac{\Gamma \vdash e_1 : \texttt{real} \quad \Gamma \vdash e_2 : \texttt{real}} {\Gamma \vdash e_1 + e_2 : \texttt{real}} \tag{T-Add}\]

\[\frac{\Gamma \vdash e_1 : \texttt{real} \quad \Gamma \vdash e_2 : \texttt{real}} {\Gamma \vdash e_1 < e_2 : \texttt{bool}} \tag{T-Lt}\]

\[\frac{\Gamma \vdash f : T_1 \rightarrow T_2 \quad \Gamma \vdash e : T_1} {\Gamma \vdash f\ e : T_2} \tag{T-App}\]

Statements

An assignment checks that its right-hand side’s type agrees with the pattern on the left. Because \(\Gamma\) is fixed — every variable already has its inferred type — a pattern needs no rules of its own: it is typed by the expression rules, a variable by T-Var and a tuple pattern \(x_1, \ldots, x_n\) like the tuple \((\, x_1, \ldots, x_n \,)\) by T-Tuple.

\[\frac{\Gamma \vdash e : T \quad \Gamma \vdash p : T} {\Gamma \vdash p := e\ \texttt{ok}} \tag{T-Assign}\]

\[\frac{}{\Gamma \vdash \texttt{skip}\ \texttt{ok}} \tag{T-Skip}\]

The \(\texttt{ret}\) operand may have any type; all returns in a function share one type, which becomes the function’s result type. An assertion tests a boolean.

\[\frac{\Gamma \vdash e : T}{\Gamma \vdash \texttt{ret}\ e\ \texttt{ok}} \tag{T-Ret}\]

\[\frac{\Gamma \vdash e : \texttt{bool}}{\Gamma \vdash \texttt{assert}\ e\ \texttt{ok}} \tag{T-Assert}\]

Sequencing and conditionals require their parts to be well-typed; a conditional also requires a boolean guard.

\[\frac{\Gamma \vdash s_1\ \texttt{ok} \quad \Gamma \vdash s_2\ \texttt{ok}} {\Gamma \vdash s_1\, \texttt{;}\, s_2\ \texttt{ok}} \tag{T-Seq}\]

\[\frac{\Gamma \vdash e : \texttt{bool} \quad \Gamma \vdash s_1\ \texttt{ok} \quad \Gamma \vdash s_2\ \texttt{ok}} {\Gamma \vdash \texttt{if}\ e\ \texttt{then}\ s_1\ \texttt{else}\ s_2\ \texttt{ok}} \tag{T-If}\]

The context statement requires a context-typed expression — evaluating it yields the active rounding context for the body — and binds the target to that context.

\[\frac{\Gamma \vdash e : \texttt{context} \quad x : \texttt{context} \in \Gamma \quad \Gamma \vdash s\ \texttt{ok}} {\Gamma \vdash \texttt{with}\ e\ \texttt{as}\ x\ \texttt{in}\ s\ \texttt{ok}} \tag{T-Context}\]