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
I’ll create new posts here when I publish the other installments, for easier commenting on the forum. Enjoy!
Thanks to @claudio for early feedback!
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?
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.
or variant {foo : empty; bar; empty}
@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.
@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.
@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:
|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.
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
@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.
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)?
@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.
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.
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.
A value is something that is valuable for the people using it in some way.
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. ?
Makes perfect sense for a unit-type. 0 = NEUTRAL.
Theory is there to serve the facts, not the other way around.
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.)
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:
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.
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.
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{}).
And the base library uses this pattern for the same purpose, and so each of these return None:
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:
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.
[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):
{
put : <K,V> (K, V) -> ();
get : <K,V> (K) -> (opt V);
has : <K> (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
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:
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.
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.
The Reserved type works perfect as a stub.
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.
“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.