Could the compiler guess a part of the program I am currently writing? It’s impossible in general, but it may be possible, and hopefully interesting, in special cases. For a start, I am interested in a situation where there is only one possibility: at the expected type, there is only one possible program – modulo (an approximation of) program equivalence.
In a fixed environment, a type is a singleton type if it has only one inhabitant. How widespread are those? Would a language feature to infer their inhabitants be useful? Can we have more interesting singleton types by enriching the type system?
Don’t expect a structured story with a happy ending: this is only a writing-ideas-down session for something I have been thinking about lately.
PS: See the next post for more details on the idea.
From erasable coercions to singleton types
I started to think about this kind of singleton types seriously when
discussing with one of our fellow students at Gallium, Julien Cretin. Julien has
been working on coercions for long enough that, if you listen to him,
basically anything in a type system is a coercion in disguise. But for
the most part he has worked on erasable coercions, that are
terms from a type
A to a type
B that are just
the identity function (once you erase the type annotations that make
One example in System F is the coercion
λ(f:A→∀α.B). Λα.λ(x:A). f x α
∀α.(A→B). Note that if you
erase all the type annotations (including type abstractions and
applications), this becomes just
λfλx. f x, which is an
η-expansion of the identity function. Those identities are “erasable” in
the sense that, after the type-checking phase, you can just drop them
from your program and you will never notice: they do not affect the
runtime semantics of the program.
Erasable coercions are fairly interesting as a way to structure and explain type systems. For example, they allow to understand various variants of System F (System Fη, Fsub, and MLF) as instances of a general version of System F enhanced with abstraction on coercions, whose formal study is surprisingly challenging. You can learn about this in Julien’s 2012 paper with Didier Rémy (long version).
But what would be a notion of non-erasable coercion? My
suggestion was to consider terms that may not exactly be the identity,
but that are unique at their type. This is actually a fairly different
concept: some coercions (for example
int → int) are not
unique in their types, and some unique inhabitants (for example in
∀αβ.(α*β)→(β*α)) have a runtime behavior that is fairly
different from the identity.
Singleton types in practice
As a thought experiment, imagine adding the keyword
the syntactic class of expressions of your programming language. The
? is as follows: at typing time, it can take
absolutely any type and will never raise a type error. After the program
has been verified to be type-correct, we look at each occurrence of
? and its inferred type. If the type is a singleton (assume
we know how to check this), we replace
? with the unique
inhabitant, otherwise we fail with an error.
That’s an inference-centered point of view. In languages with less
robust type inference than ML languages, we could have a more robust
feature with a construction
(? : σ) that is given a precise
type, which should later turn out to be a singleton. A simple
? is then explained as
(? : _), where
_ means “infer me” at the type level.
Consider for example those lines of OCaml or Haskell code found in the wild (in fact in the OCaml type-checker and in GHC):
(List.map (fun (name, smty, smodl) -> (name, smty)) zipWith3M f xs ys zs = zipWithM (\x -> \(y,z) -> (f x y z)) xs (zip ys zs)
The functions passed to
zipWithM here are the typical kind of boilerplate that is
boring to write. Provided that “the types are distinct enough”, they are
also singleton types:
fun (x,y,z) -> (x,y) is a
singleton type as long as the types for
z are distinct (in this example I checked and they
are), likewise in the second example. Wouldn’t it be nice to be able to
(List.map ?) zipWith3M f xs ys ys = zipWithM (? f) xs (zip ys zs)
The hope is that some of the case where you think “This is dumb, I should not have to write it” may turn out to be, when looking at them the right way, inferrable through singleton types.
Singleton types precisely
What does it mean for a type to be a singleton type? We have to make a choice on four aspects:
The type system we consider (the static semantics). Are we looking for singleton types in ML, in System F, in a dependently typed calculus? All those choices have merit, but for the purpose of the demonstration I will mostly use examples in System F.
The language of the terms we infer (the dynamic semantics). If we consider the full term language of OCaml (or Haskell) as the space of our search, no interesting type is a singleton because of non-terminating terms inhabiting any type. We want to restrict ourselves to a pure (including total) lambda-calculus. For a start, just the obvious explicitly typed thing with variables, lambdas and applications will be fine.
Our notion of program equivalence: if we consider
(λx.x) tas two different programs, we will have trouble finding unique inhabitants. On the other end, observational equivalence is often undecidable for realistic languages, so we may have to pick reasonable restrictions. I will just imagine I can perfectly decide observational equivalence for now.
The typing context where inhabitants live: I am asking whether a type
σhas a unique inhabitant
t : σ. To consider this properly I need to pick a typing context
Γand ask about
Γ ⊢ ? : σ. We could imagine giving the user some freedom to specify the context in which the search should take place. A good starting choice is to consider the super-empty context: a context with no variables, but also no constants: forget about
0, 1, 2, true, false, etc., to get even more singleton types (
bool → int → bool, for example). Other reasonable choices include the empty context with constants, the current context of the program, or a restriction of the current context with only the variables that have been marked “implicit” of sorts.
The restriction to an empty context is why I wrote
in the previous example:
zipWithM3 f xs ys zs = zipWithM (? f) xs (zip ys zs)
If I just write
zipWithM ? xs .., this tries to infer
code at the type
(a → (b, c) → m d), which is not inhabited
in an empty context. On the contrary, the
(? f) has type
(a → b → c → m d) → (a → (b, c) → m d), which is a
singleton type. This shows that this construct can actually be used for
partial term inference, just add the hints as parameters to
?. (Another possibility would be to add syntax to specify a
context by hand, eg.
(f,g |- ? : σ).)
Similarly, it can also be used for plumbing: if you cannot remember
y comes first as a parameter to
f, and they have different types,
(? f x y)
can do the job. (If they don’t have different types there is a potential
for non-statically-catchable error and that’s bad. OCaml’s labeled
arguments are very nice when used to fight this, but it’s orthogonal
to the present considerations.)
I know of surprisingly little work on the topic of “code inference” (looking for this search string on Google Scholar for example brings up very little hits), and would welcome pertinent pointers. There is a paper at PLDI last year, Type-Directed Completion of Partial Expressions by Daniel Perelman, Sumit Gulwani, Thomas Ball and Dan Grossman, but it is much more practically oriented: “let’s look for completions using typing hints and see how often we were right in ranking highly a suggestion to the user”. In the limit, you get something fuzzy and interactive and machine-learning-based, where type-correctness is just one ranking criterion among others, as you can find in Sean McDirmid’s work on touch-based programming or calls to Programming as collaborative reference, but that is not where I want to go now. The idea here more to study the mathematical structure of singleton types, which is quite a different subject.
Of course, “singleton types” is just a special case: it could also be interesting for code inference to determine which types have only two inhabitants; the compiler then wouldn’t choose automatically (that would break principality) but instead give the choice to the user. Joe B. Wells has a paper with Boris Yakobowski (which is, incidentally, a former Gallium PhD student), Graph-based proof counting and enumeration with applications for program fragment synthesis, that does exactly this: count the number of inhabitants of types in an intuitionistic type theory, and devise a term enumeration algorithm out of it. It is the most pertinent previous work that I know of, and was done with program synthesis in mind.
Singleton types and programming experience
I’ve mentioned that singleton types is only one specific case in the
wider setting of “please find me the inhabitants of this type”. I think
however that focusing on singleton types is maybe not as ad-hoc at is
looks like: if a type has a finite number of inhabitants, it can
probably be decomposed as a sum of singleton types. Maybe we could tell
to the user of our
? construction that “you’re not a
singleton yet, you have to make a choice between this type and this
type”, and let him add just enough information to determine which
situation she’s interested in. That would be potentially even more
useful than enumerating the full terms and letting the user choose one,
? may be more robust in the face of code maintenance
than system-spewed boilerplate.
More robust, or more fragile: being a singleton is not stable by
instantiation. The type
∀αβ. α*β → β*α is a singleton, but
α:=int, β:=int breaks this property. (Note
that it is interesting in practice only if the type is inferred, because
it is just as long as the term.). People are surprised/dismayed by this
aspect when I give them examples of singleton types, but I think it’s
fine: we are checking singletons after type inference, where
type abstractions and applications have been fully determined. Yet I
don’t know how robust those
? would be in practice. I think
the idea of doing all this after type inference is a sane
protection: I have this intuition that we probably don’t want a system
that tries to infer simultaneously the types of some part of
our program, and the terms of another.
Note that it is possible to see the work on type classes as a
specific instance of the idea of singleton types. Using an operation of
a type class would add a
? to synthesize the expected
dictionary. Instance declarations are function declarations (instance
dependencies being function arrows) that populate the context of search.
The coherence relations that reduce ambiguities in Haskell are a way to
ensure unicity of inhabitants. Finally, inference of class predicates
Eq a => gets added to an inferred function type
if you use
(==) inside the body of the function) is a way
to ensure that there is always an inhabitant.
This is not a realization of the highest importance, because it actually tells us little new about type classes; singletons are a rather general way to look at everything that involves some form of “guessing code” that is a bit principled (and doesn’t just produce code at random); this recasting should work for other features that can be expressed as code inference. It tells us, however, that some particular forms in the design space for putting singleton types in practice have already found themselves useful enough for programmers. I think that justifies looking at the concept at a wide angle.
A temporary ending – or delay
This post is getting quite long, so I’ll temporarily conclude here. Stay tuned for another blog post with even more ramblings about singleton types !
PS: The next post is now out.