A partially ordered set is a set endowed with a binary relation on such that for all we have:
2.) and implies (transitivity)
3.) and implies (anti-symmetry)
If and are partially ordered sets, we say that a function between them is monotone if for all with , we have .
Several recent research papers (for example Lasp and BloomL) propose programming frameworks which utilize monotone functions as primitives of program composition, but they provide the user with a fixed set of monotone functions to work with. A type system capable of proving program functions monotone may enable the development of extensible versions of such frameworks.
Lately, I’ve been designing such a type system, for an extension of the simply typed lambda calculus. Since the programmer only cares about the monotonicity of a select group of functions, a special syntax construct, the sfun abstraction, serves as a signal to the type checker: unlike the simply typed world outside of the sfun abstraction, the body of the sfun abstraction is type checked using a special type system, which I call the lifted type system, in which monotonicity is tracked.
Reasoning about pointwise orderings on function spaces seems a bit heavy-weight and hasn’t been necessary for any of my use cases. An sfun is therefore first order; that is, both its return type and all of its argument types must be data types rather than function types. We would like to be able to prove that a multi-argument function is monotone separately in each of its arguments; that is, for , if then , etc.
The monotonicity of an sfun is typically derived from the monotonicity of the primitives used to implement it, which are also sfuns. Here are some example sfun primitives, addition and subtraction on integers:
1.) plus :
2.) minus :
An sfun type, written with rather than , names its formal arguments and also qualifies each one. A qualifier is an argument-specific constraint on the behavior of the function. In the above types, the qualifier is associated with arguments that are separately monotone and is associated with arguments that are separately antitone. The second argument of a binary function is separately antitone if implies .
Terms outside of sfun abstractions are typed using a global typing relation, which, aside from an sfun abstraction typing rule, is not different from the typing relations we are familiar with. A global typing judgment has the following form.
A typing judgment of the lifted type system, used to type check the body of an sfun, has the following form:
Here the global type environment contains all of the variables bound outside of the sfun, the ambient type environment contains the list of the sfun’s formal arguments, and the lifted type environment contains those variables in ’s context which are bound inside the sfun. Before getting into the significance of lifted typing judgments, let’s look at a specific instance of the global typing rule for sfun abstractions, which uses a single lifted premise.
Here we type a single-argument sfun abstraction . As you might have guessed, is used rather that to distinguish this as an sfun abstraction rather than a standard one. Examine the ambient and lifted type environments used in the premise. Perhaps surprisingly, the abstraction’s bound variable is entered into both environments. When variables occur in types, they are considered references to formal arguments rather than actual arguments; that is, an occurrence of in a type (for example ) does not refer to some integer, but instead a “slot” named which expects to receive some integer from an external source. Inside the scope of the sfun abstraction, we would like the ability to refer to the abstraction’s formal argument , and therefore we add to the ambient environment. We would also like to include occurrences of as terms in the body of the abstraction; for these, we add the entry into the lifted type environment, to be used as a placeholder for the actual argument supplied to the formal argument . Because references to formal arguments occur only in types, and references to actual arguments occur only in terms, we can add entries with the same name to both the ambient and lifted environments without creating any ambiguity.
The premise of the above rule application includes the strange looking types and . Normally, we would expect occurrences of x, which serve as placeholders for the actual argument of the the function, to have type , and we would expect our abstraction’s body to have type as well. This traditional approach to typing a function abstraction characterizes the operational behavior of a single function after it has been applied. Unfortunately, this isn’t adequate for reasoning about properties such as monotonicity, which involve multiple calls to the same function. My approach instead takes the perspective of inside of a function, before it has been applied. Lifted typing then characterizes the structure of a function as the composition of its constituent parts. In the above example, an occurrence of the variable in the term has type , meaning that it is a function which takes the value provided to (the enclosing sfun’s formal argument) as an input, and produces that value unchanged as a result. We ultimately care about the input/output relation of this function, and so the concrete values which inhabit this type are set-of-pairs function representations. The type happens to be a singleton type, containing the set of pairs .
The sfun application is viewed as a function composition, where the outputs of the functions represented by the two occurrences of are forwarded into the left and right arguments of the sfun . The domain of this composite function matches the domain of the enclosing sfun, which it inherits from the two occurrences of . Since returns an , so does the composite function. The premise of the above typing rule application tells us that has type , but this premise must be derived. How do we go about proving that the composite function is monotone?
First, pretend that the two occurrences of reference different formal arguments and . Holding the left formal argument fixed gives a single-argument function , which the type signature of tells us must be monotone. , representing the identity function on integers, is clearly monotone, since for all integers with , we have . is then the composition of two monotone functions, which itself must be monotone. The same reasoning tells us that is monotone as a function of when is held fixed. is therefore monotone separately in both and . However, we are interested in , which is the function we get when we contract and into a single argument, supplying both of ’s “slots” with the same value. Contracting two arguments of a function which are both separately monotone results in a new argument which is also separately monotone, and so we can conclude that has type .
The lifted sfun application typing rule utilizes two binary operators and on qualifiers, which describe how monotonicity is propagated across function composition and argument contraction. The above example utilized the facts that is equal to and is equal to . These operators are defined as lookup tables, recording a set of predefined facts about the propagation of monotonicity.
I’ll wrap things up by leaving you with one of the central features of my calculus. Namely, that the “global world” outside of an sfun abstraction is viewed as a degenerate subset of the “lifted world” inside the sfun abstraction. A globally well-typed sfun application is viewed as a projection onto this degenerate subset. Inside the sfun abstraction, we track the way in which each term depends on the sfun’s arguments, but terms originating outside of the sfun (both literal constants and occurrences of variables from the global type environment ) depend on the sfun’s arguments in a specific way: they are not affected by them at all. So, for any sfun with ambient environment , we can view the literal integer as a constant-valued function which, given any valuation of , produces the value one as a result. Of course, constant functions are monotone, and so a lifted subtyping relation allows 1 to occur in any context where Integer-valued functions with monotone dependence on the ambient environment are expected. I view this as a weird refinement type system. Instead of starting with a simply typed system and decomposing its base types into preorders to induce a subtyping relation, I started with a simply typed system and positioned its base types as refinements of base types in a system with larger types (larger in that they denote larger sets of values). Consider the ambient environment . Letting be the type of Int-valued functions which share the enclosing sfun’s formal parameter , the following diagram decomposes the type into refinements.
The red arrows indicate that projection from into the refinement plays a special role. Still curios? See this paper for motivating examples, a full formalization, and a soundness proof.