2
$\begingroup$

I am wondering how you could possibly define the implementation of an imperative function as a type. Is it possible? Currently I only see the input parameters and output result used in the definition of a function type, but how could you also include the implementation in the type definition?

$\endgroup$
2
  • $\begingroup$ If you want to have a function f: A -> C, which does operations fst: A -> B and snd: B -> C, then you can essentially declare a class: class MyFun { C f(x: A) { return snd(fst(x)); } abstract B fst(x: A); abstract C snd(x: B) }. Is this what you want? Of course, instead of abstract methods, you can always pass implementations as constructor parameters. $\endgroup$ – Dmitry Oct 11 '20 at 22:23
  • $\begingroup$ In general, expressions of a language & any relevant abstract things in the semantics are what are assigned types. $\endgroup$ – philipxy Oct 13 '20 at 2:13
6
$\begingroup$

The seminal paper on this topic is Linear Types Can Change the World! by Phil Wadler.

Of course, with a title like that, you know it has to be a Wadler paper. It's a pun, the implication being that linear/uniqueness type system allows you to represent operations which mutate the world state.

You can use linear types today in languages such as Clean. See, for example, Aachen et al, High Level Specification of I/O in Functional Languages.

In logic languages, you can do the same thing with strong modes rather than strong types, such as in Mercury. (Full disclosure: I'm one of the original Mercury developers.) See Fergus Henderson's honours thesis, Strong Modes can Change the World!

EDIT

I think I may have misinterpreted the question, which I thought was about types for imperative code.

The answer to your question is "yes, absolutely". There is a tradeoff between types and programs. At one end of the spectrum, you have a completely dynamic type system, where every program has the same type. At the other end, you have a hyper-static type system, where every type only has one program that is of that type, with the type essentially encoding the program.

In the middle ground, there are many programming languages whose type systems are Turing-complete, including Haskell, Java, TypeScript, and Rust.

$\endgroup$
1
  • 1
    $\begingroup$ Linear types are one way to apply type theory to programs with side effects (monads and effects are others). But in themselves, they only have a very limited ability to characterize how a function is implemented $\endgroup$ – Gilles 'SO- stop being evil' Oct 13 '20 at 18:34
3
$\begingroup$

I'll admit I'm confused about the details of your question: you want the implementation of a program to appear in its type? Usually types talk about behavior. That's why they're useful!

The idea of having the full specification of a procedure appear in types is very suggestive of dependent type theory. Traditionally these theories only apply to languages without mutability, which might be the point of your question.

But computer scientists have been working diligently to integrate well-known methods of analyzing imperative languages into theories of dependent types. One example is Hoare Type theory, see e.g. the paper Hoare Type Theory,Polymorphism and Separation.

$\endgroup$
1
  • $\begingroup$ Dependent types allow giving very precise specifications, but they don't directly help to describe how a function is implemented: $\Pi_x. T(x)$ only characterizes the type of the result as a function of the value of the argument (as opposed to being a constant with simple types, or being a function of the type of the argument (or something a little more general) with polymorphism), it doesn't characterize how the result is calculated. (Dependent types can help indirectly because if you encode implementation aspects in the type, you're soon going to want precise types.) $\endgroup$ – Gilles 'SO- stop being evil' Oct 13 '20 at 18:33
3
$\begingroup$

Yes. Before I give the answer, let me set the stage.

Giving types to expressions and functions

Historically, programming languages started to have types to qualify memory locations: does the memory cell where x is stored contain an integer or a floating-point value? Type enforcement is then to check (or coerce) that the value that gets stored into x has the correct type. x := <expr> is well-typed if the value of the expression expr has the same type as x. This generalizes typing from values to expressions: the type of an expression is the type of its value.¹

So we'll consider type systems that assign types to expressions. A statement that the expression $M$ has the type $T$ is written $\Gamma \vdash M : T$, where $\Gamma$ is an environment (also called context) that lists the types of the variables that are present in $M$.

When reasoning about expressions and their values, it's often useful to consider not only the expression and the value, but the evaluation rules that lead from one to the other. The most common way to describe the evaluation rules of a program is through reduction rules that define how an expression can be reduced (simplified) to another. A value is an expression that cannot be reduced any further. A reduction rule has the form $$ M \longrightarrow M' $$ stating that $M$ can be reduced in one step to $M'$.

If you define both reduction rules and a type system for a language, they had better be compatible. The property that defines their compatibility is type preservation (also called subject reduction): if an expression has a certain type, then what it reduces to still has that type. In mathematical notation: if $\vdash M : T$ and $M \longrightarrow M'$ then $\vdash M' : T$.

Let's see what type preservation can tell us about the types of functions. The rule to reduce a function application is beta reduction: $$ \underbrace{(\lambda x. M)}_{?} \, \underbrace{\strut N}_{U} \longrightarrow \underbrace{M[x \leftarrow N]}_{T} $$ For type preservation, if the right-hand side has the type $T$, we want the left-hand side to have the type $T$ as well. Given an argument of type $U$, we want $\lambda x.M$ to have a type that ensures that $M$ will have the type $T$ once we replace $U$ with a value of type $U$. To keep things simple, let's stick to functions that require their argument to have a specific type: assuming that $x$ has the type $U$, $M$ must have the type $T$. The type of $\lambda x. M$ is the type of functions that map values of type $U$ to values of type $T$, which we'll write $U \rightarrow T$. And the function $\lambda x.M$ has the type $U \rightarrow T$ if $M$ has the type $T$ under the assumption that $x$ has the type $U$: $$ \dfrac{x : U \vdash M : T}{\vdash (\lambda x. M) : U \rightarrow T} $$

(Note that I'm not saying that this is the only way to define a type system for functions and function application. I'm just showing one way to make it work, without covering all the details. What I'm showing is the simply typed lambda calculus.)

Effect types

So far we've seen how to type expressions and functions if the only thing that interests us about the type of an expression is the type of the value that it reduces to. Now let's extend that to encode other information about an expression in its type.

If the semantics of an expression is more than its value, we'd better encode that in the runtime semantics. So let's add labels to the reductions. Labels encode information about the behavior of the expression. The most common use of labels is to encode side effects. For example, let's consider a language with a print function that doesn't return anything. The “expression-value type” of print is $\mathsf{char} \rightarrow \mathsf{unit}$ (it returns a value of the unit type, which carries no information). The expressions print('a') and print('b') both evaluate to the unit value (), which is pretty boring. What's interesting is what they print, so let's annotate the reduction relation with what gets printed. $$ \mathtt{print}(c) \xrightarrow{c} () $$ The sequence of labels in a sequence of reductions is called a trace. For example $$ \mathtt{print}(\mathtt{'a'}); \mathtt{print}(\mathtt{'b'}) \xrightarrow{\mathtt{'a'}} \mathtt{print}(\mathtt{'b'}) \xrightarrow{\mathtt{'b'}} () $$ is a sequence of two reductions with the trace $(\mathtt{'a'}, \mathtt{'b'})$. In this toy example, the trace of the reductions of an expression is what it prints. More generally, the trace of the reductions of an expression describes its runtime behavior.

If we want to capture the runtime behavior of an expression in its type, we need to convey the trace in the typing. The usual way to do it is to add an effect annotation to typing statement: $\Gamma \vdash M :_e T$ states that given the types of the variables in the environment $\Gamma$, the expression $M$ has the type $T$ and the effect $e$. (Notations can vary.) The name “effect system” comes from the fact that the most common use is to track side effects of expressions. In its most basic form, $e$ would be the trace of $M$, but the point of a type system is usually not to know all the details, just relevant details. So just like we usually work on types like int and char which are sets of values (or at least which stand for sets of values), the effect annotation $e$ is a set of traces, or more generally it represents a set of traces. For example, the effect of $\mathtt{print}(c)$ is $\{c\}$, because the only possible trace of this expression is the one-character string $c$. In mathematical notation: $\vdash \mathtt{print}(c) :_{\{c\}} \mathsf{unit}$.

What does this mean for functions? As before, we want the type of a function to contain enough information to determine the type of its result. For this example, let's stick to call by value: the argument $N$ is a value, and evaluating it has an empty trace (by definition of a value, the sequence of reductions from it is empty). Reducing the function application has no side effect: any side effect from the evaluation will come from further reductions of the body. $$ \underbrace{(\lambda x. M)}_{?} \, \underbrace{\strut N}_{U} \longrightarrow \underbrace{M[x \leftarrow N]}_{\xrightarrow{e} T} $$ In order for the right-hand side to be well-typed, we want the fact that the left-hand side is well-typed to guarantee that $x : U \vdash M :_{e} T$. So the type of $(\lambda x. M)$ should guarantee that its effect is $e$, in addition to guaranteeing that its result has the type $T$: $$ \dfrac{x : U \vdash M :_{e} T}{\vdash (\lambda x. M) : U \rightarrow_{e} T} $$ We've annotated function types with effects: $U \rightarrow_{e} T$ is the type of functions that take an argument of type $U$ and return an argument of type $T$ after having the effect $e$.

Here's a sketch of the definition of a different, extremely simple effect system that just indicates whether an expression is pure (no side effect) or impure (might have side effects). The grammar of effects is just $e ::= \mathsf{P} \mid \mathsf{E}$. We define the combination of two effects as $e_1 \sqcup e_2 = \mathsf{P}$ if $e_1 = e_2 = \mathsf{P}$ and $e_1 \sqcup e_2 = \mathsf{E}$ otherwise: the combination is pure only if all the parts are pure. The typing rules for lambda abstraction and for function application are $$ \dfrac{\Gamma, x:U \vdash M :_{e} T} {\Gamma \vdash (\lambda x.M) :_{\mathsf{P}} U \rightarrow_{e} T \} \qquad \dfrac{\Gamma \vdash M_1 :_{e_1} U \to T \qquad \Gamma \vdash M_2 :_{e_2} T} {\Gamma \vdash M_1 \, M_2 :_{e_1 \sqcup e_2} T} $$ A lambda abstraction is always pure: the effects of the function are only unleashed when the function is applied to an argument.

Effect systems can be very simple or very complex, depending on what aspects of the runtime behavior you want to model and how precise the model you want to be. They're a very general framework for reasoning about the behavior of programs. Here are a few examples of behaviors you can model with an effect system:

  • The exceptions that an expression might raise (as Java does).
  • The I/O that an expression might perform.
  • The channels over which a process might communicate (this is usually what's of interest when typing process calculi).
  • Whether an expression might not terminate (it's sometimes advantageous to treat non-termination as a side effect).
  • How long it takes to evaluate an expression (for real-time systems).

Singleton types

You asked how to “define the implementation of an imperative function as a type”. Effect systems let us capture aspects of the behavior of the function. But effect systems usually don't capture all the aspects of the behavior, because that would be too unwieldy. If you need to express “exactly this function, and not just something with similar behavior”, type theory has a concept for that: singleton types.

A singleton type is a type that contains a single value. The expression $M$ has the singleton type $\mathsf{S}(V)$ if and only if the value of $M$ is $V$. (More generally, with non-termination, $M$ might have the type $\mathsf{S}(V)$ if its only possible value is $V$; if $M$ doesn't terminate, it has the type $\mathsf{S}(V)$ for every $V$.)

With functions, it's usually impossible for a compiler to decide whether two implementations of a function are identical, so in order for a function to have a singleton type $\mathsf{S}(\mathtt{foo})$, the compiler has to be able to track that the specific function $\mathtt{foo}$ was passed around. With data types, a compiler might have a chance of allowing $2+2$ to have the type $\mathsf{S}(4)$.

Singleton types aren't very interesting on their own, but they become interesting when combined with other language features. Here are a few examples of uses of singleton types.

  • If you can take the union of singleton types, you can express that the value of an expression is in a finite set, for example to constrain the range of an integer expression.
  • The Ocaml module system has a form of singleton types for modules.
  • In Haskell, singleton types are often used used to sneak dependent types into the language.
  • Rust has singleton types for functions, called function item types.

¹ There are many common generalizations, such as subtyping, polymorphism, coercions, etc. but I won't go into them unless they're relevant to the question at hand. So if you're reading this and thinking “this isn't the whole story”, yes, this isn't the whole story. I'm writing an answer, not a treatise.

$\endgroup$
1
$\begingroup$

You could use the singleton types, see the paper Extensional equivalence and singleton types by Robert Harper and Christopher Stone and Chapter 9 of Advanced Topics in Types and Programming Languages.

Briefly, the idea is to extend the type system with singleton types $\{A \mid t\}$ which intuitively means "the type of values of type $A$ that are equal to $t$". For example, $\{\mathtt{nat} \mid 2 + 3\}$ is the type of natural numbers equal to $2 + 3$.

The singleton types are used in modules to express sharing constraints.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.