# Candid explainer: First post published **URL:** \ **Category:** Language Support\ **Created:** [August 29, 2021, 3:59pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787 "2021-08-29T15:59:12Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [August 29, 2021, 3:59pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/1 "2021-08-29T15:59:13Z")
I wrote up a lengthy text explaining various aspects of Candid. I broke it up into multiple posts, the first one of which is now available: [https://www.joachim-breitner.de/blog/782-A\_Candid\_explainer\_\_The\_rough\_idea](https://www.joachim-breitner.de/blog/782-A_Candid_explainer__The_rough_idea) I’ll create new posts here when I publish the other installments, for easier commenting on the forum. Enjoy! ---
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [August 29, 2021, 4:07pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/2 "2021-08-29T16:07:53Z")
Thanks to @claudio for early feedback! ---
**Author:** ![levi](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/levi/32/22608_2.png) [@levi](https://forum.dfinity.org/u/levi)\ **Post date:** [September 5, 2021, 7:48pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/3 "2021-09-05T19:48:33Z")
Looking forward for the post bout the Option, that was a tricky one . Why is there a Null type if there is an Option type? ---
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [September 5, 2021, 8:15pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/4 "2021-09-05T20:15:42Z")
Hmm, that won’t be in that post. I think the reason for the `null` type is that the `null` _value_ ought to have a principal type, and although `opt empty` would work for that, that’s maybe too confusing. Hmm, reading that reasoning again I see how it would apply to Motoko, but I’m less sure whether it really applies to Candid. So maybe simply an artifact of co-design? It _is_ handy to have an idiomatic unit type (type with one value), for example as the argument type that we use when expressing enum types via variants (`variant {foo; bar}` is a shorthand for `variant {foo : null; bar; null}`). Although that alone is not a strong enough reason, I’d be fine with using `reserved` here (although I expect there is an interesting philosophical debate to be had about whether `reserved` is a unit type or not…) @rossberg might have a better explanation for why Candid has `null`. ---
**Author:** ![levi](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/levi/32/22608_2.png) [@levi](https://forum.dfinity.org/u/levi)\ **Post date:** [September 5, 2021, 8:36pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/5 "2021-09-05T20:36:36Z")
> [@nomeata](#): > > I’d be fine with using `reserved` here` or `variant {foo : empty; bar; empty}` ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 6, 2021, 10:19am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/6 "2021-09-06T10:19:17Z")
@nomeata, I don’t fully remember, but having a unit type probably was a reason. I don’t think `reserved` counts as a unit type – it is a top type, which isn’t the same: semantically, it contains _all_ values, not just one. Even though coercive subtyping blurs this distinction. @levi, a variant with only empty cases has no values, so is itself empty. IOW, it’s isomorphic to the empty type, not the unit type. ---
**Author:** ![levi](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/levi/32/22608_2.png) [@levi](https://forum.dfinity.org/u/levi)\ **Post date:** [September 6, 2021, 9:18pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/7 "2021-09-06T21:18:06Z")
> [@rossberg](#): > > @levi, a variant with only empty cases has no values, so is itself empty. IOW, it’s isomorphic to the empty type, not the unit type. @rossberg i could say the same thing bout the null type. A variant with only null cases is itself null, and thus is null and void. The way I see it, empty makes more sense for the variants without a type and as a unit-type because there is a lack(empty) of a **type** associated with the variant-hash-key. The variant still has a hash-key, but a lack of a type associated with it. ‘ { foo: null }’ seems like the variant-key: foo is itself null. What is the value of null by it self? The value of the Option is: it holds the possibility that a specific-value will not be returned. What is the value of null ? It is a value without a value, a negative value, a contradiction in it’s self. ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 7, 2021, 7:13am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/8 "2021-09-07T07:13:54Z")
@levi, you could say that, but it wouldn’t be correct. 😉 The type `null` is inhabited by exactly one value: the value `null`. That’s a perfectly fine value, it just carries no information, exactly because it cannot be anything else. In contrast, the empty type is not inhabited by _any_ value. These aren’t just random definitions, these are algebraic properties (in type theory, such types are often written 1 and 0). The difference is fundamental. For example, if you have a function with return type `null`, a caller knows that it will return the value `null`. If they have a function with return type `empty`, they know it cannot actually return at all, ever. It can only diverge or throw. The variant with no cases is isomorphic to the empty type as well – that’s simply a special case of a variant with all cases having empty type. Dually, a record with at least one empty field is also isomorphic to the empty type – you can construct no values for it either. And a record with all fields having type `null` is itself isomorphic to type `null`, because there is only one possible value for the entire record. More succinctly, if we write `|T|` for the number of values a type has (its cardinality), then the following holds: ```auto |empty| = 0 |null| = 1 |opt T| = 1 + |T| |variant {T1,...,TN}| = |T1| + ... + |TN| |record {T1,...,TN}| = |T1| * ... * |TN| |func T1 -> T2| = |T2|^|T1| (ignoring side effects or functions that don't return) ``` Consequently, in type theory, variants are called sum types and records or tuples are product types. Functions are sometimes called exponentials. ---
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [September 7, 2021, 10:55am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/9 "2021-09-07T10:55:45Z")
> [@rossberg](#): > > I don’t think `reserved` counts as a unit type I knew you’d say that 🙂 Would you say `record { foo : null }` is a unit type? This is getting philosophical, of course, and there is no serious disagreement here. To me, in order to count elements of a type I need a equality relation on the elements. And that depends on the type I look at them. But yeah, noncoercive subtyping blues the distinction 🙂 ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 7, 2021, 11:10am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/10 "2021-09-07T11:10:05Z")
@nomeata, not every type of cardinality 1 is the/a unit type. They’re merely isomorphic. But more importantly, the cardinality of a top type isn’t even 1, rather, it is ∞. At least semantically. The fact that this isn’t necessarily true at the representation level in Candid (due to lossy coercions) is mostly an implementation detail. ---
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [September 7, 2021, 11:33am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/11 "2021-09-07T11:33:32Z")
Oh, what’s your definition of a unit type then, if not via cardinality? Neutral element of the product type former? (But that’d be also up to some form of type equivalence.) Or maybe that it is an terminal object in the category of types and functions (but that definition seems to have the same fate)? ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 7, 2021, 1:34pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/12 "2021-09-07T13:34:48Z")
@nomeata, fair question. In the abstract, one often conveniently identifies isomorphic types (and I suppose HoTT provides a whole theory for that), but in a concrete type system that has many distinguishable types of cardinality 1, we usually pick a specific representative that is canonical in some way. Typically, it’s either terminal or the empty product type. ---
**Author:** ![nomeata](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/nomeata/32/733_2.png) [@nomeata](https://forum.dfinity.org/u/nomeata)\ **Post date:** [September 7, 2021, 2:13pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/13 "2021-09-07T14:13:04Z")
So, what’s your definition of “terminal” here? But I guess what you are saying is that the statement “type t is the unit type of Candid” isn’t based on some property of `t` that `t` has, but simply a declaration: We say (by decree or convention) that `null` is “the” unit type of Candid, and therefore it is. I can live with that. ---
**Author:** ![levi](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/levi/32/22608_2.png) [@levi](https://forum.dfinity.org/u/levi)\ **Post date:** [September 7, 2021, 9:23pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/14 "2021-09-07T21:23:55Z")
> [@rossberg](#): > > `|null| = 1` What is this 1 value that is in the null type? If you can show me 1 scenario where the Null type is needed where empty or option is not sufficient then I will concede. There is a lack of a scenario in which using the type Null is **valuable** for the people using candid. > [@rossberg](#): > > The type `null` is inhabited by exactly one value: the value `null` A value is something that is valuable for the people using it in some way. > [@rossberg](#): > > For example, if you have a function with return type `null` , a caller knows that it will return the value `null` . If they have a function with return type `empty` , they know it cannot actually return at all, ever. It can only diverge or throw. I know the difference in how it gets used, but this is inviting overcomplications in people’s code. Why would a function ever need to return Null ? When it can return empty or option. ? > [@rossberg](#): > > `|empty| = 0` Makes perfect sense for a unit-type. 0 = NEUTRAL. Theory is there to serve the facts, not the other way around. ---
**Author:** ![matthewhammer](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/matthewhammer/32/323_2.png) [@matthewhammer](https://forum.dfinity.org/u/matthewhammer)\ **Post date:** [September 7, 2021, 11:53pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/15 "2021-09-07T23:53:35Z")
> [@levi](#): > > What is this 1 value that is in the null type? I believe that the `| |` operator is giving the cardinality of the type, as if it were a set (whose members are the distinct values of that type). The 1 and only member value of type `null` is value `null`. I think it’s problematic to think of types as sets (but that operator is still fine by me) so I’d say it a bit differently: _The number of values classified by type `null` is 1, and its value `null`_. (I like “classification” rather than “containment” for the action that types do to their values.) > [@levi](#): > > A value is something that is valuable for the people using it in some way. Here, we mean “value” in the PL theory sense, not in the everyday sense (like practical utility). A value is an “introduction form” of data that: - has a type - has no “evaluation” left before being “used” (so 3 is a value, but “1 + 2” is not). To be a value with an elimination form (a “practical use”) is an extra requirement of values, and not strictly needed. `null` and unit value `()` are two (distinct) examples of values without productive elimination forms in Motoko and in Candid. > [@levi](#): > > Theory is there to serve the facts, not the other way around. What are the “facts” of PL design, I wonder? FWIW, I subscribe to a prescriptive stance for PL design, not a descriptive one. Perhaps you are arguing for a more descriptive stance? In my view, the history of PL design and implementation tells us that the prescriptive approaches are the ones whose theories are sufficiently simple enough to withstand the test of time. Following theory afterwards, as some reaction to practice, seems to invite regret onto everyone involved in the theory and the practice. ---
**Author:** ![matthewhammer](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/matthewhammer/32/323_2.png) [@matthewhammer](https://forum.dfinity.org/u/matthewhammer)\ **Post date:** [September 7, 2021, 11:59pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/16 "2021-09-07T23:59:42Z")
> [@levi](#): > > Why would a function ever need to return Null I use this typing feature of the language every single day. Step 1: Stub a function in Motoko that has a non-unit return type. Step 2: Call the stubbed function from where I want to use it. Step 3: Use the compiler to type-check the stub without implementing it. These steps are a regular pattern for my style of programming (“hole-directed”?). To get the holes to be accepted by the compiler, I use the fact that `None` (the equivalent of `empty`) exists in the Motoko type system, and can be inhabited by `loop { assert false }` (or even the less useful, simpler version `loop{}`). ---
**Author:** ![matthewhammer](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/matthewhammer/32/323_2.png) [@matthewhammer](https://forum.dfinity.org/u/matthewhammer)\ **Post date:** [September 8, 2021, 12:02am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/17 "2021-09-08T00:02:21Z")
And the base library uses this pattern for the same purpose, and so each of these return `None`: > ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 8, 2021, 7:44am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/18 "2021-09-08T07:44:08Z")
> [@levi](#): > > What is this 1 value that is in the null type? If you can show me 1 scenario where the Null type is needed where empty or option is not sufficient then I will concede. There is a lack of a scenario in which using the type Null is **valuable** for the people using candid. First of all, the technical definition of value is not dependent on usefulness of values, that would be absurd. You can construct many useless values for many types. As I said: `null` is a perfectly fine value, it just carries no information. That’s in fact the defining property of any unit type. Maybe the name `null` is misleading, because it makes you think too much in terms of low-level notions like “null pointers”. Perhaps it becomes clearer when you view `opt` as a variant type, because that’s what it really is semantically. Effectively: ```auto type opt T = variant {_null; _opt : T}; type null = variant {_null}; type empty = variant {}; ``` Now, the `null` variant is a subtype of the `opt` variant. Furthermore, it obviously has a value, namely `_null`, unlike the empty variant. ---
**Author:** ![rossberg](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/rossberg/32/795_2.png) [@rossberg](https://forum.dfinity.org/u/rossberg)\ **Post date:** [September 8, 2021, 7:48am UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/19 "2021-09-08T07:48:38Z")
[Grr, Forum giving me a 403 again when my reply was only half-done, and I can’t edit it anymore. Rest of reply follows.] Having said all that, the type `null` also is in fact useful. For example, it allows the use of variants as enums in the first place: in Candid, the type `variant {a; b}` is in fact just a shorthand for `variant {a : null; b : null}`. This way, Candid needs no special handling of such variant cases. (With that in mind, my above pseudo-definitions wouldn’t really work in practice, because they would be circular – you’d need another unit type.) This role of unit types is a general scheme when using generic types. Candid does not have generics yet, but once it has you could imagine an interface to a map canister like (making up some Motoko-style syntax): ```auto { put : (K, V) -> (); get : (K) -> (opt V); has : (K) -> (bool); } ``` Now, assume you just need a set. Then you can use this canister with type `V = null`, effectively ignoring the value part. Note that you could _not_ use `V = empty`, because then you’d never be able to call `put`. There are potential use cases without generics, e.g., when evolving some interfaces. For example, say a canister has a function ```auto foo : (bar : func (nat, opt nat) -> (nat)) -> (nat) ``` During some upgrade, the canister evolves to not using or needing the optional parameter of the callback anymore. It cannot remove it, because that would break existing clients. But it can indicate it’s unused from now on by refining the type of the callback to: ```auto foo : (bar : func (nat, null) -> (nat)) -> (nat) ``` This documents the intent while being backwards compatible with callers passing a callback that still allows an option. New clients o.t.o.h. can implement this callback with a null parameter as well, and thereby ignore it. > [@](#): > > ```auto > |empty| = 0 > > ``` > > Makes perfect sense for a unit-type. 0 = NEUTRAL. No, sorry, not at all. You can write a function with return type `null`, because there is a value for it. You cannot write a function with return type `empty`. Also see my map-as-set example above. ---
**Author:** ![levi](https://sea1.discourse-cdn.com/flex023/user_avatar/forum.dfinity.org/levi/32/22608_2.png) [@levi](https://forum.dfinity.org/u/levi)\ **Post date:** [September 15, 2021, 5:22pm UTC](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787/20 "2021-09-15T17:22:08Z")
> [@matthewhammer](#): > > Step 1: Stub a function in Motoko that has a non-unit return type. The Reserved type works perfect as a stub. > [@matthewhammer](#): > > What are the “facts” of PL design, I wonder? Good question. The facts are the factual-usage of the system by a coder/user. What are the facts of the usage. How will the coder use the candid library and how can he use it, and how simple or complex (how many steps) it takes do use it in certain ways. These are the facts. > [@matthewhammer](#): > > FWIW, I subscribe to a prescriptive stance for PL design, not a descriptive one. Perhaps you are arguing for a more descriptive stance? “Perspective stance” , “descriptive stance”. These are **VAGUE AND AMBIGUOUS** terms. The opposite of the facts. If you want to use words like that in a conversation I need the factual-terms behind those words. [Next page](https://forum.dfinity.org/t/candid-explainer-first-post-published/6787.md?page=2)