11
$\begingroup$

Quoting one of Alexis King's answers:

Many programming language researchers would call many things “type systems” that programmers probably don’t think of as type systems. Many forms of static analysis can be usefully viewed in the framework of type systems, but they may not have all that much to do with programmers’ notion of types.

It’s not clear to me why this would be true. Why is the framework of formal type systems useful for modeling other things (particularly, other static analyses besides the standard notion of type-checking)? What are some examples of things modeled in that way?

To make clear: the "standard notion" of types are things which are associated with each variable, expression or other language construct which can have, receive or produce a value, and which describe (usually lossily) or constrain the possible values those language constructs can have, receive or produce.

$\endgroup$
2
  • $\begingroup$ In C/C++, const allows verifying that data is not modified inside a function call, even if that call delegates to other functions. This is done through the type system, by pretending that non-const to const is a one-way type conversion. $\endgroup$ Aug 15, 2023 at 11:32
  • $\begingroup$ So, what is a type? (In programming languages.) A formal definition of type system is in the answers. What about the programmer's notion? $\endgroup$
    – Pablo H
    Aug 15, 2023 at 14:04

4 Answers 4

11
$\begingroup$

Formally speaking, type systems are defined as logical judgments. As described in my answer explaining the notation, inference rules are really just a fancy way of writing logical implication. This is an exceedingly general framework, and in fact it’s possible to specify any syntactic rule system using the notation of natural deduction (and plenty of PL researchers often do).

Within that extremely general logical framework, the judgments a PL researcher might call a “type system” are qualitatively identified by five things:

  1. The judgment defines a relation between terms and types, the latter of which classify terms.

    Note that these syntactic classes do not even need to be distinct—in dependent type systems, terms and types are syntactically the same. However, in all cases, the types somehow “approximate” terms, which is to say multiple terms are assigned the same type.

  2. The judgment is context-sensitive. This is represented in the iconic $\Gamma \vdash$ notation.

  3. The judgment is at least mostly syntax-directed, which is to say there is a typing rule corresponding to each production in the grammar of terms, and the nested structure of proof trees induced by the judgment mirrors the nested structure of terms.

  4. The judgment does not depend on Turing-complete evaluation.

    Generally, the typing judgment does not depend on term evaluation at all, as type systems are supposed to represent static analysis. However, excluding it completely would once again fail to account for dependent type systems, where terms can appear inside types, and those terms must be normalized, which is a form of evaluation. However, terms in those languages are usually quite restricted, so evaluation of all terms is guaranteed to terminate.

  5. The defined relation admits a type soundness theorem.

    How exactly this theorem is stated can vary considerably, but broadly speaking, the intent is to demonstrate that the defined typing rules usefully approximate some aspect of evaluation. One aphorism often stated here is that “well-typed programs can’t go wrong.” A common approach to formally stating type soundness is known as “progress and preservation”.

You’ll note that this definition is still rather vague on the matter of what exactly terms and types are and what the typing relation represents. This is what makes the framework so astonishingly useful! Many programmers would consider a “type” to be, essentially, a description of the structure of the value an expression will evaluate to. However, a PL researcher might consider types that are substantially more abstract:

There are numerous other examples, but those are just ones that immediately come to mind.

$\endgroup$
5
$\begingroup$

Control-flow effects

Consider a simple imperative language with statements as defined below; $e$, $s$ and $i$ are for expressions, statements and identifiers respectively:

$$ \begin{array}{lcl} s & ::= & \mathsf{Expr}(e) \\ &|& \mathsf{Break} \\ &|& \mathsf{Return}(e) \\ &|& \mathsf{Sequence}(s, s) \\ &|& \mathsf{If}(e, s) \\ &|& \mathsf{Loop}(s) \\ &|& \mathsf{Function}(i, s) \\ \end{array} $$

For simplicity, the "Loop" statement here is like a "while true" loop, and functions have no parameters and aren't void. (We won't concern ourselves with function return types, because we're not doing standard type-checking here.)

There are some requirements which we want to statically enforce:

  1. A break can't occur outside of a loop;
  2. A return can't occur outside of a function;
  3. A function must either return, or loop infinitely;
  4. A break, return or infinite loop cannot be followed by another statement in sequence.

To formalise these requirements, we will assign a "type" to each statement. The "types" in this system are tuples $(n, b, r)$ of booleans, where $n$ indicates whether the statement can complete normally (without breaking or returning), $b$ indicates whether it can break, and $r$ indicates whether it can return.

Now we can write the rules for determining the "type" of each statement:

$$ \begin{array}{l}\hline \vdash \mathsf{Expr}(e) : (\mathrm{true}, \mathrm{false}, \mathrm{false})\end{array} \qquad \begin{array}{l}\hline \vdash \mathsf{Break} : (\mathrm{false}, \mathrm{true}, \mathrm{false})\end{array} \qquad \begin{array}{l}\hline \vdash \mathsf{Return}(e) : (\mathrm{false}, \mathrm{false}, \mathrm{true})\end{array} \qquad \begin{array}{l}\vdash s_1 : (\mathrm{true}, b_1, r_1) \\ \vdash s_2 : (n, b_2, r_2) \\ \hline \vdash \mathsf{Sequence}(s_1, s_2) : (n, b_1 \lor b_2, r_1 \lor r_2)\end{array} \qquad \begin{array}{l}\vdash s : (n, b, r) \\ \hline \vdash \mathsf{If}(e, s) : (\mathrm{true}, b, r)\end{array} \qquad \begin{array}{l}\vdash s : (n, b, r) \\ \hline \vdash \mathsf{Loop}(s) : (b, \mathrm{false}, r)\end{array} \qquad \begin{array}{l}\vdash s : (\mathrm{false}, \mathrm{false}, r) \\ \hline \vdash \mathsf{Function}(i, s) : (\mathrm{true}, \mathrm{false}, \mathrm{false})\end{array} $$

A few things are worth commenting on:

  • For simplicity we're supposing that expressions cannot have control-flow effects. That's reasonable in a simple language which has no exceptions, and we aren't modelling exceptions in this example.
  • Break and return statements never complete normally.
  • An "if" statement can always complete normally, when the condition is false; and when the condition is true, the statement can throw or return if its body can. This conservatively assumes that the condition can be either true or false.
  • A loop can complete normally only if its body can break. Since the loop "consumes" breaks which occur within it, the loop statement itself cannot propagate a break. Hence its type is like $(b, \mathrm{false}, r)$.
  • A function body must have type $(\mathrm{false}, \mathrm{false}, r)$ meaning it cannot break (satisfying requirement 1), and it cannot complete normally (i.e. complete without returning), satisfying requirement 3). The function declaration itself completes normally without breaking or returning, because declaring a function doesn't invoke it.
  • In a sequence of two statements, the first statement's type must be $(\mathrm{true}, b_1, r_1)$ because according to requirement 4, it must be able to complete normally. So the resulting type is like $(n, b_1 \lor b_2, r_1 \lor r_2)$ because it completes normally only if $s_2$ does, but it can break or return if either $s_1$ or $s_2$ can.

Finally, we require the root statement (i.e. the top-level of the program) to have a type of the form $(n, \mathrm{false}, \mathrm{false})$. This encodes requirement 2, and the rest of requirement 1.


So, why model control-flow effects this way? Well, one reason is that it gives a formal specification which we can check our static analysis algorithm against.

Another is that the "type" of each statement becomes data which can be retained for other purposes, rather than existing only transiently during checking. That data might be useful for program transformations such as

$$\mathsf{Loop}(\mathsf{Sequence}(s, \mathsf{Break})) \mapsto s$$

which is only valid when $s : (n, \mathrm{false}, r)$, i.e. when $s$ cannot break. It also provides a safety net to sometimes catch incorrect transformations, since we can check that the type of the original statement is equal to the type of the transformed one.

$\endgroup$
4
  • $\begingroup$ I’m curious if you know of any existing presentations that model things this way, or if this is novel. It’s a neat example! Some nitpicking: your BNF grammar should have $s$ to the left of the $::=$, not $\mathsf{Statement}$. Also, I wouldn’t use mathsf for your booleans since they seem to be terms in the metalanguage rather than terms in the language. $\endgroup$
    – Alexis King
    Aug 14, 2023 at 23:56
  • $\begingroup$ For what it’s worth, I would probably not expect to find this sort of thing represented this way, as booleans do not have very much structure. Instead, I would probably expect to see a set of labels $\overline{\ell}$ contained within a context and locally extended by $\mathbf{loop}$, and I’d expect $\mathbf{break}$ to be indexed by a label in the form $\mathbf{break}\ \ell$ or $\mathbf{break}_\ell$. $\endgroup$
    – Alexis King
    Aug 15, 2023 at 0:02
  • $\begingroup$ I also don’t entirely understand the purpose of the $r$ element of your tuples; it seems to be left unconstrained by every rule. $\endgroup$
    – Alexis King
    Aug 15, 2023 at 0:05
  • $\begingroup$ @AlexisKing Thanks for the nitpicking; I've edited to address it. The example comes from something similar I'm doing in the compiler for my language MJr, where I'm using it for inference and transformations rather than checking. Good point about labels, I just tried to keep it simple in this example; the $r$ element is required to check that you can't return from the top-level, but I wasn't sure how to encode that. $\endgroup$
    – kaya3
    Aug 15, 2023 at 0:06
4
$\begingroup$

Any static analysis that a compiler or programmer might be interested is a potential candidate for turning into a system of strong static programmer-visible guarantees.

Think of the way that some modern languages basically incorporate null reference checking into the type system, which was something that was previously an optimisation. Also consider Rust's static memory management (which was, of course, taken from Cyclone).

In Mercury, a logic language, we used a static analysis system to enforce static strong modes (i.e. dataflow) and static strong determinism.

Some ideas that have been under-explored:

  • Strong static aliasing. (Disclaimer: I tried this once, in the context of Mercury, but it would also be extremely useful in a Fortran-like language.)
  • Strong static bounds checking. It's nice for a compiler to eliminate, say, array bounds checks when it can, but wouldn't it be even nicer if the compiler could statically guarantee that array bounds checks are not needed?
  • Strong static vectorisation/loop-parallelism.

I feel like this is fertile ground for future research: compilers that guarantee that certain optimisations will occur.

$\endgroup$
4
  • 1
    $\begingroup$ "Any static analysis" sounds like a strong claim ─ in Alexis's answer there are some stipulations about it being a judgement per term in the language (as opposed to e.g. a judgement which applies only to whole programs) and it being "at least mostly syntax-directed", presumably because typing rules are defined by structural recursion on the syntax. How should I square these two answers? $\endgroup$
    – kaya3
    Aug 15, 2023 at 12:14
  • 1
    $\begingroup$ Also, could you clarify what the difference would be between a compiler being able to eliminate array bounds checks where it can, and being able to eliminate them where it can statically guarantee they are not needed? Isn't that what "where it can" means? $\endgroup$
    – kaya3
    Aug 15, 2023 at 12:15
  • $\begingroup$ @kaya3 There is a difference between an optimisation and a guarantee. An optimisation might happen with certain compiler flags if the compiler can prove that the optimisation is safe, but the programmer can't rely on it always happening. Similarly, in a dynamically typed language, a compiler may be able to infer that some variable is always an integer, and optimise accordingly (e.g. basic computations are "unboxed" and use no heap), but in a statically typed language, that might be guaranteed, so a programmer can rely on that "optimisation" always happening. $\endgroup$
    – Pseudonym
    Aug 16, 2023 at 0:48
  • $\begingroup$ Incidentally, the "at least mostly syntax-directed" qualification is likely for diagnostic reasons as much as anything. Programmers like it when errors and warnings are reported with specific reference to the program that they typed in. Nothing is more frustrating than a message which says in effect "your program is not type correct, but I have no idea what specific lines of code might be responsible". $\endgroup$
    – Pseudonym
    Aug 16, 2023 at 0:56
2
$\begingroup$

Curry-Howard correspondance

Type systems can be used to model formal logic, and this is the basis of the "Curry Howard correspondence".

Each type represents a logical proposition, and an instance of the type represents a proof of the proposition. Function types represent "if"/"implies" statements (which is why the syntax of function types uses -> in many languages), product types (structures with multiple fields) represent conjunctions (AND), and sum types ("enums" with multiple variants) represent disjunctions (OR). FALSE is represented by a type with no instances (an enumeration with no variants), and TRUE is represented by a type with one instance (the unit type, a struct with no fields).

-- Basic rules
data True = True
data False
data And a b = And a b
data Or a b = OrL a | OrR b

-- We can define (type-safe) functions which are valid propositions
anythingImpliesTrue :: a -> True
anythingImpliesTrue anything = True

falseImpliesAnything :: False -> a
-- How does this typecheck? Here we do "standard" case analysis on `False`,
-- except it has no cases! Since there are no cases, every case returns an
-- instance of `a` (`∀ f, all f [] = true`), thus the entire case expression
-- is an instance of `a`
falseImpliesAnything False = case False of {}

-- We can compose predicates, do everything a regular language supports
trueAndFalseImpliesFalse :: And (True False) -> False
trueAndFalseImpliesFalse (And true false) = falseImpliesAnything false

-- We can also compose types
type Not a = a -> False
trueOrFalseDoesntImplyFalse :: Not (Or (True False) -> False)
trueOrFalseDoesntImplyFalse f = falseImpliesAnything (OrL True)

-- However, we can't define functions which are invalid propositions
-- UNLESS we cheat with a value like `error msg`
trueImpliesFalse :: True -> False
trueImpliesFalse True = error "cheating"

-- OR write a function which never terminates
trueImpliesFalse' :: True -> False
trueImpliesFalse' True = trueImpliesFalse' True

Sticking to this representation, we can only create type-checking values which are valid propositions, we can't create values which type-check and represent invalid propositions. Except for:

  • Operations which may error (exceptions, undefined behavior)
  • Failable type-casts or type-casts which may invoke undefined behavior
  • Unsound typing rules (see: Counterexamples in Type Systems)
  • Functions which might never terminate

These are serious exceptions in most languages like C/C++ and TypeScript. Even if you ignore exceptions, functions like exit, and explicit casts, these languages have unsound holes in the type system (trivial example: in non-strict TypeScript, you implicitly cast a union A | B | C to any one of its variants e.g. B). Most of all, they lack termination checking, and functions which don't trivially terminate are extremely common; even "functional languages" like OCaml and Haskell don't warn you if you define non-terminating functions.

// You can also model logic in more traditional languages like C++
struct True {};
enum class False {};
template<typename A, typename B> struct And { A a; B b; };
// Although some of these are much more verbose
template<typename A, typename B> class Or {
    using Data = union { A a; B b; };
    bool tag;
    Data data;
    Or(bool tag, Data data) : tag(tag), data(data) {}

  public:
    static Or left(A a) { return Or(false, { .a = a }) }
    static Or right(B b) { return Or(true, { .b = b }) }

    template<typename T> T visit(std::function<T(A)> ifLeft, std::function<T(B)> ifRight) {
        return tag ? ifRight(data.b) : ifLeft(data.a);
    }
}

// True -> (A \/ A) -> A
template<typename A> std::function<A(Or<A, A>)> trueImpliesAOrAImpliesA(true: True) {
    return [](Or<A, A> aOrA){ return aOrA.visit([](A a){ return a; }, [](A a){ return a; }) });
}

// Of course, many C++ features let you break this
False aFalse = (False)42;
template<typename A> False aImpliesFalse(A a) {
    std::abort("not true");
}

But there are special "theorem-proving languages" where there are no erroring functions, no unsound type casts, and and all functions must be inferred or explicitly proven to terminate; thus, when code in these languages typechecks, it defines theorems which are guaranteed (up to some "obvious" fundamental axioms) to be true. The "theorems" in these languages are types, and the "proofs" which guarantee their correctness are instances.

(* This is 100% valid coq code *)
Theorem n_plus_n_is_n_times_2 : forall n : nat, n + n = n * 2.
Proof.
(* This "proof" is more or less unreadable, you must use the IDE like CoqIDE
   or proof general to step through it. But it proves the above is true *)
  intros n.
  induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite <- IHn'. reflexivity.
(* The IDE will not let you step past this and coq won't compile this if the
   above doesn't prove that the theorem holds *)
Qed.

(* This is the actual "proof" value, which is even uglier *)
Print n_plus_n_is_n_times_2.
n_plus_n_is_n_times_2 =
fun n : nat =>
nat_ind (fun n0 : nat => n0 + n0 = n0 * 2) (eq_refl : 0 + 0 = 0 * 2)
  (fun (n' : nat) (IHn' : n' + n' = n' * 2) =>
   eq_ind (S (n' + n')) (fun n0 : nat => S n0 = S (S (n' * 2)))
     (eq_ind (n' + n') (fun n0 : nat => S (S (n' + n')) = S (S n0)) eq_refl (n' * 2) IHn')
     (n' + S n') (plus_n_Sm n' n')
   :
   S n' + S n' = S n' * 2) n
     : forall n : nat, n + n = n * 2

Often the proofs/instances are very complicated and unreadable, so the developer constructs them with the aid of an IDE, and proof automation in the form of tactics) which partially or fully infer and construct an instance for a given type. You also have dependent types, which are types that include values and value expressions, like forall n, Eq (collatz n) 1, as well as functions which take one type and return another (like UpTo : (P : Nat -> Type) -> (n : Nat) -> forall n', n' < n -> P n'). As you can start to see, the types get really complicated, and they can represent really complicated proofs; this is the power of the Curry-Howard correspondence. Incredible projects like CompCert (a C compiler proven to have equivalent semantics to a C AST interpreter), sel4 (a microkernel proven to not crash, barring hardware issues), and the first known proof of the Four-Color Theorem were created using Coq, all proven using the Curry-Howard correspondance, some fundamental axioms, and very advanced type-checking.


Lastly, I want to go back to "traditional" non-theorem proving languages, just to note that while it's not feasible to use them to write advanced proofs or code guaranteed to be correct with high confidence, their type systems can still be used to verify properties of your program. For example, if you define a type which can only be created from an operation (e.g. AuthorizedUser which can only be created by a call to Option<AuthorizedUser> login(String name, String password) with the correct arguments), you can create functions which can only be used in a type-safe way if they have that value (e.g. String getSecretData(AuthorizedUser user), which can't be called unless we create an authorized user, which we can't do unless we enter the correct name and password). This is especially important when designing an API, though it veers away from "how to use type systems for theorem proving" and towards "how to effectively use type systems in general".

$\endgroup$
1
  • 2
    $\begingroup$ I’m not sure that this really answers the question, though I don’t think it’s totally unrelated, either. The question is about using the metatheoretical framework of type systems to model things that are not conventionally considered type systems, but the Curry–Howard correspondence is about embedding propositions into a type system satisfying certain properties. This is not really the same thing. $\endgroup$
    – Alexis King
    Aug 15, 2023 at 1:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .