-
Pl
chevron_right
A Candid explainer: The rough idea
pubsub.slavino.sk / planetdebian · Sunday, 29 August, 2021 - 15:51 · 4 minutes
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
The rough idea (this post)
Announcing the blog post series, and very briefly outlining what an Interface Description Language even is.
Safe higher-order upgrades (to be published)
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!
Opt is special (to be published)
Extending records in argument position is surprisingly tricky. Lean why, and how we solved it.
Language integration (to be published)
The point of Candid is inter-op, so let’s look the various patterns of connecting Candid to your favorite programming language.
Quirks (to be published)
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 (
vec
tors,
opt
ional values ,
record
s and
variant
s). 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.
Značky: #Debian