Spec: Refactor description of deserialization

[nomeata]

This is a significant rewirte of the section in the spec describing
deserialization. Some points worth noting:

• This replaces the elaboration relation with one that takes a value
  and a type as input, and returns a value. This makes it clearer that
  there is no “input type” of deeper relevance.

• One great benefit: No more long prose about how the rules assume
  these types to be principal, even if they aren’t.

  This clarifies questions like this
  one

• Also, the existing rules about “elaborating function values” were
  kinda bogus, as function values are just accepted as they are. This
  is much easier now, also good.

• Unfortuantely for this application, our textual representation has
  overloading. Instead of defining yet another abstract value algebra,
  I did a bit of hand-waving, and defined an “overloading-free
  fragment” of the textual format for this section.

• A fair number of rules becomes simpler. Promising!

• I was able to phrase some interesting properties more formally. Also
  promising! Didn’t actually prove them, though, although we should.

• Still unclear to me what we mean with “subtyping is complete”, see
  the section there.

• Decoding is still an inductive relation, so not fully algorithmic.
  This may be an issue with a stright-forward formalization; not all
  theorem provers like negative occurrences of inductive relations in
  their rules.

• Syntax of the relations up for discussion.

[nomeata]

@rossberg @chenyan-dfinity , what do you think of this?

As an implementor, I think I’d find this presentation more helpful. And if I were to prove soundess etc. formally, then too.

[nomeata]

If the diff is too confusing to read, then head to https://github.com/dfinity/candid/blob/joachim/rewrite/spec/Candid.md#decoding

[rossberg]

Good stuff, thanks!

[rossberg]

I would expect the following formulation:

(∀ v, v'. v : T /\ v :? T' ~> v') ⇒ T <: T'

Is there anything wrong with that? And should it not be a requirement?

[nomeata]

That formulation doesn't make sense to me, the antecent is never true.

Should /\ be →? Or should v' be behind some ∃?

[rossberg]

Ah, oops, wrong quantifier:

(∃ v, v'. v : T /\ v ~> v' : T') ⇒ T <: T'

[nomeata]

Now the antecent is far too weak, it says “T is a subtype of T' if some values of type T make sense at type T'). This would, for example, relate all list types (use v = [] and v' = []).

[nomeata]

How about I remove this section (so this can land if all else is fine), and we discuss this in a separate issue?

[rossberg]

Eh, you're right, I should turn my brain on. Okay, last try, if that's wrong as well, feel free to remove it. :)

(∃ v. v : T /\ ∀ v. v : T ⇒ ∃ v'. v ~> v' : T') ⇒ T <: T'

This looks a bit like monster-barring the uninhabited case, but I think it is a natural definition, saying: if serialised values exist for type T, and all such values can be deserialised at type T', then T ought to be considered a subtype of T'.

Uninhabited types tend to make everything harder...

[nomeata]

Nope, sorry still not good.

In the antecent instead of ∀ v. v : T ⇒ I am sure you ∀ v. v ~> _ : T ⇒ (i.e. not just the “canonical” values, but really “all values that can be deserialized at T). But I think that’s what you mean anyways.

But empty types still break it: This definition would still imply vec Empty <: vec t for all t.

And even then: Remember that coercion never fails for reference values (because we don't do a subtyping check when decoding and coercion), so any definition for completeness that is based on purely the _ ~> _ : _ relation will probably relate all function types, which is obviously not sound (in the non-local; IDL-Soundess.md sense).

Let’s take this into a separate issue.

[nomeata]

Moved to #132

[nomeata]

Mostly answers (and questions), will perform the changes after lunch.

[nomeata]

That formulation doesn't make sense to me, the antecent is never true.

Should /\ be →? Or should v' be behind some ∃?

[rossberg]

Btw, nit: various inference bars are too short.

[nomeata]

Ok, all comments handled one way or another

[nomeata]

I’ll give @chenyan-dfinity a chance to comment before merging

[chenyan-dfinity]

LGTM. It's indeed much cleaner!

[chenyan-dfinity]

We also need annval for null : opt _

[nomeata]

No, I am pretty sure we don't! That’s because

• On the left of ~>, it doesn't matter which null it is (any null behaves the same)
• On the right of ~>, the type is given, so again there is only no null value.

So it is fine to have a single null value in the V set.

This is not true for overloaded numbers; (5 : nat) ~> and (5 : int) ~> behave differently.

[rossberg]

In other words, null has a principal type, numbers don't. (Which makes me wonder, why do we need a special case for reserved?)

[nomeata]

Because the algebra of binary values has a dedicated reserved value (DIDL\x00\x01\x70), but our textual representation doesn’t. The (null : reserved) could just as well be ("reserved" : reserved) or (record {} : reserved); it’s arbitrary and, in a way, always lie.

For me, the conceptual “abstract value data model” has a dedicated reserved value, and I think it would be good to have it in the textual representation as well, to avoid the above wart in the formalism, but also to not force debug output to come up with such arbitrary values when decoding a message with a reserved value:

~/dfinity/haskell-candid $ cabal -v0 run hcandid -- --decode --rust "DIDL\x00\x01\x70"
((null : reserved))

[nomeata]

More evidence that it might be useful to have it: All implementations that have a “value” type seemed to feel the need to add it to their data type:

• candid/rust/candid/src/parser/value.rs

  Line 37 in 03773cc

  Reserved,

• https://github.com/nomeata/haskell-candid/blob/36202a9aef4387925c0d0de23a0e3645ed7d2b3e/src/Codec/Candid/Types.hs#L142