Joachim Breitner's Homepage

One of the technologies that was created by DFINITY as we built the “Internet Computer” is Candid. Candid is

• a language to describe the interface of a service, with named methods, arguments and results,
• a type system for these arguments and results that maps to many possible implementation languages, thus enabling interoperability between these languages,
• a wire format (encoding) of values of these types,
• a notion of “safe upgrade” that allows service developers to evolve their interface with the assurance that no clients break, even in the presence of higher-order composition,
• a meta-theory of safe interface description languages and a formal proof that Candid has these properties, and
• a bunch of tools and libraries.

In this in-depth blog post series I want to shed some light onto these aspects of Candid. The target audience is mainly anyone who wants to deeply understand Candid, e.g. researchers, implementors of Candid tools, anyone who wants to builds a better alternative, but no particular prior Candid knowledge is expected. Also, much of what is discussed here is independent of the Internet Computer. Some posts may be more theoretical or technical than others; if you are lost in one I hope you’ll rejoin for the subsequent post

Much in these posts is not relevant for developers who just want to use Candid in their projects, and also much that they want to know is missing. The Internet Computer dev docs will hopefully cater to that audience.

Blog post series overview

1. The rough idea (this post)

   Announcing the blog post series, and very briefly outlining what an Interface Description Language even is.

2. Safe higher-order upgrades

   Every can do first-order interface description languages. What makes Candid special is its support for higher-order service composition. This post also contains some general meta-theory and a Coq proof!

3. Opt is special

   Extending records in argument position is surprisingly tricky. Lean why, and how we solved it.

4. Language integration

   The point of Candid is inter-op, so let’s look the various patterns of connecting Candid to your favorite programming language.

5. Quirks

   The maybe most interesting post in this series: Candid has a bunch of quirks (hashed field names, no tuples but sequnces, references that nobody used, and more). I’ll explain some of them, why they are there, and what else we could have done. Beware: This post will be opinionated.

The rough idea

The idea of an interface description language is easy to begin with. Something like

service A : {
  add : (int) -> ();
  get : () -> (int);
}

clearly communicates that a service called A provides two methods add and get, that add takes an integer as an argument, and that get returns such a number. Of course, this only captures the outer shape of the service, but not what it actually does – we might assume it implements a counter of sorts, but that is not part of the Candid interface description.

In order to now use the service, we also need a (low-level) transport mechanism. Candid itself does not specify that, but merely assumes that it exists, and is able to transport the name of the invoked method and a raw sequence of bytes to the service, and a response (again a raw sequence of bytes) back.

Already on the Internet Computer we have two distinct transport mechanisms used are external calls via an HTTP-based RPC interface and on-chain inter-canister calls. Both are handled by the service in the same way. Here we can see that Candid succeeds in abstracting over differences in the low-level transport mechanism. Because of this abstraction, it is possible to use Candid over other transportation mechanisms as well (conventional HTTPS, E-Mail, avian carrier). I think Candid has potential there as well, so even if you are not interested in the Internet Computer, this post may be interesting to you.

The translation of argument and result values (e.g. numbers of type int) to the raw sequence of bytes is specified by Candid, defining a wire format. For example, the type int denotes whole numbers of arbitrary size, and they are encoded using the LEB128 scheme. The Candid wire format also contains a magic number (DIDL, which is 0x4449444c in hex) and a type description (more on that later). So when passing the value 2342 to the add, the raw bytes transported will be 0x4449444c00017da612.

Of course we want to transfer more data than just integers, and thus Candid supports a fairly complete set of common basic types (nat, int, nat8, nat16, nat32, nat64, int8, int16, int32, int64, float32, float64, bool, text, blob) and composite types (vectors, optional values , records and variants). The design goal is to provide a canonical set of types – enough to express most data that you might want to pass, but no more than needed, so that different host languages can support these types easily.

The Candid type system is structural. This means that two types are the same when they are defined the same way. Imagine two different services defining the same

type User = record { name : text; user_id : nat }

then although User is defined in two places, it’s still the same type. In other words, these name type definitions are always just simple aliases, and what matters is their right-hand side.

Because Candid types can be recursive (e.g. type Peano = opt Peano), this means we have an equirecursive type system, which makes some things relatively hard.

So far, nothing too special about Candid compared to other interface definition languages (although a structural equirecursive type system is already something). In the next post we look at reference types, and how such higher order features make Candid an interesting technology.