A Type System of Labeled Optional Parameters for SATySFi v0.1.0

I am in the process of changing the language design for SATySFi v0.1.0 about optional parameters. It will be a breaking change (i.e. not backward compatible with SATySFi v0.0.x), and I will introduce it here.

First appearance:

• Dec 30, 2021. SATySFi Wiki (written in Japanese)

Motivation of the Reformulation

Originally, SATySFi v0.0.x has a mechanism of non-labeled optional parameters/arguments, and it can be used with ?: like the following:

+section?:(`sec:sample`)?:(`Sample`){Sample}<
  ... the contents of the section ...
>

Optional arguments do not have a label, and thereby are distinguished by their order. In the example above, the first optional argument is a tag for the cross reference, and the second one is for the title of the section displayed in the Outline of the resulting PDF file. As well as commands, ordinary functions can take optional parameters:

let increment ?diff-opt n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
in
(increment 42, increment ?:57 42)
  % --> (43, 99)

The reason why a mechanism of non-labeled optional parameters was adopted is that the language design was inspired by that of LaTeX, where optional parameters are conventionally given in a non-labeled manner:

\parbox[c]{6em}{…}, $\sqrt[3]{2}$

It has, however, lead to the following significant inconvenience, partly because there came to be more use cases of optional parameters than expected:

• Since optional arguments are distinguished only by their order, in many cases where you use or read functions that have optional parameters it is difficult to comprehend in what order each argument should be specified.

• When you want to omit a former parameter and to give an argument to a latter one, you have to do some cumbersome workaround–to “explicitly omit” the former one by ?*.

  +section?*?:(`Sample`){Sample}<
    ... the contents of the section ...
  >

To remove this kind of burden, I came upon the idea of reformulating the mechanism of optional parameters into labeled one where one can give optional arguments like the following:

+section?(ref = `sec:sample`, outline = `Sample`){Sample}<
  ... the contents of the section ...
>

As you can see, optional arguments can be specified by ?(label1 = arg1, …, labelN = argN). You can omit the whole part ?(...) if you don’t want to specify any optional argument. Ordinary functions can take labeled optional parameters as well:

let increment ?(diff = diff-opt) n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
  end
in
(increment 42, increment ?(diff = 57) 42)

This will bring the following benefits:

• Since optional arguments are labeled, it is easy to read for what purpose each argument is specified.
• Since optional arguments can be in a ramdom order, you don’t have to do any workaround like the one using ?*.
• Because types of optional parameters/arguments can be statically inferred as usual, type errors will be reported when one gives an argument of a type incompatible to the expected one.

It seems also good to me that one can give default values as follows when defining optional parameters:

let increment ?(diff = d = 1) n =
  n + d
in
(increment 42, increment ?(diff = 57) 42)

The Detail of the Type System

Extension to Function Types, Function Abstractions, and Function Applications

Function types \(τ \to τ\) will be extended to the following form:

The traditional form \(τ_1 \to τ_2\) is equivalent to \(?()\ τ_1 \to τ_2\). Although function types will actually take a more general form explained later, it is sufficient for now to display the form above.

(Side note: function types with non-labeled optional parameters in SATySFi v0.0.x have the form \(τ \mathrel{?\!\!\to} \cdots τ \mathrel{?\!\!\to} τ \to τ\).)

Function abstractions and applications will also be extended like the following:

Similarly to the case of function types, \(\mathbf{fun}\ x \to e\) and \(e_1\ e_2\) are syntax sugar for \(\mathbf{fun}\ ?()\ x \to e\) and \(e_1\ ?()\ e_2\), respectively. Binders in abstractions can also take type annotations, but it is omitted for clarity here.

The derivation rule for typing function applications is concise, like the following:

The rule is very straightforward except that it should be noted that in \(e\) bound variables are of type \(\mathrm{option}\ τ_i\), not of \(τ_i\).

The derivation rule for function abstractions looks a bit more complicated, but is not so complex in meaning:

To see how these typing rules work, let me recall the previous increment example:

let increment ?(diff = diff-opt) n =
  match diff-opt with
  | Some(d) -> n + d
  | None    -> n + 1
  end

This function will be assigned the following type:

• increment \(\ :\ ?(\mathtt{diff} : \mathrm{int})\ \mathrm{int} \to \mathrm{int}\)

Polymorphism

The basics of the newly introduced type system has been described so far, but an additional trick is needed actually; optional parameters require a kind of polymorphism.

Consider the following example: what kind of type should be assigned to higher-order functions like the following?

let use_optional f =
  f ?(foo = 42) 57 + 1

Specifically, of what type should f be? Although you may suppose that f has a type like \(?(\mathtt{foo} : \mathrm{int})\ \mathrm{int} \to \mathrm{int}\), there is a possibility that f can take another optional parameter bar but that no argument is speficied for bar here. Handling such kind of constraints needs polymorphic types for optional parameters.

In order to express such polymorphism, the type system of optional parameters for SATySFi v0.1.0 leverages a kind of row polymorphism [1]. This may perhaps be of my own devising because I haven’t seen any paper or implementation that use a similar formalization, but it is not so particularly ingenious and has not been proved to fulfill type safety yet.

The basic concept of the type system is to regard whole optional arguments in a function application as a row. Rows are typically used for typing records, but are also utilized for typing optional parameters/arguments here by giving the following syntax:

The metavariable \(r\) represents a row, and \(ρ\) ranges over the set of row variables. The symbol \(\ast\) stands for the empty row, and \(l : τ, r\) is the row produced by appending \(l : τ\) to the row \(r\). The aforementioned form of function type \(?(l_1 : τ_1, …, l_n : τ_n)\ τ^{\prime} \to τ\) is actually the special case of function types having a row of the form \(l_1 : τ_1, …, l_n : τ_n, \ast\).

By using this type system, one can assign to use_optional the following type:

• use_optional \(\ : ∀ρ \mathrel{::} \mathrm{Row}\ \{\mathtt{foo}\}.\ ?(\mathtt{foo} : \mathrm{int}, ρ)\ \mathrm{int} \to \mathrm{int}\)

where the kind \(\mathrm{Row}\ L\) with a label set \(L\) is the one for rows that do not contain any label in L. Namely, the universal quantification in the type above means that \(ρ\) can be instantiated to any row that does not have \(\mathtt{foo}\) as a label. In this fashion, it will be verified that f, the first parameter of use_optional, must be able to take a parameter of type \(\mathrm{int}\) labeled by \(\mathtt{foo}\), but no constraint is imposed on the capability of taking the other labels.

This mechanism has already been basically implemented in a PR for developing SATySFi v0.1.0, and been verified to work fine at least for some use cases.

Conclusion

This article has introduced a mechanism of labeled optional parameters designed and implemented for SATySFi v0.1.0, and explained that it is based on the row polymorphism.

References

1. Benedict R. Gaster and Mark P. Jones. A polymorphic type system for extensible records and variants, 1996.