## Singleton types for code inference

- December 29, 2012
- Last updated on 2012/12/30

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 them useful).

One example in System F is the coercion

```
λ(f:A→∀α.B). Λα.λ(x:A). f x α
```

from `A→∀α.B`

to `∀α.(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 `?`

in the
syntactic class of expressions of your programming language. The
semantics of `?`

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 `List.map`

and `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 `x`

,
`y`

and `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 write:

```
(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

`t`

and`(λx.x) t`

as 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 `(? f)`

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 `?`

in `(? 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
which of `x`

or `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.)

## Related Work

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, as `?`

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
instantiating `α:=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
(the way `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.