[Iris-Club] Constructivism: necessity or preference?

[Ralf Jung]

Hi,

> I think one of the design principle behind the Iris logic is
> constructivism, because:
> 
> - In the ICFP 2016 paper is said "Dockins et al. introduced multi-unit
> separation algebras [14], which, unlike PCMs, only demand the existence
> of a possibly different unit ua with ua · a = a for any element a. A
> crucial difference between multi-unit separation algebras and RAs is
> that we present the monoidal operation and core as a function, whereas
> they represent these as relations."  I think the reason the authors
> think function and relation have a crucial difference is, they care
> constructivism.

Well, more practically speaking, functions are just much more useful in
Coq than relations.  It would be possible to build Iris entirely on a
relational form of RAs (even constructively, I think); however, this
would be a huge pain -- we could no longer write "a ⋅ b ⋅ c", instead
we'd have tons of existential quantifiers and witnesses of the relation...

So, really, this is mostly a proof engineering decision.

> - In the Iris 2.0 documentation, a COFE is defined as a tuple of the
> form (T, =_n, lim: chain(T) -> T).  It is stronger than requiring just
> existence of the limit; it actually requires a function that maps a
> chain to its limit.
> 
> 
> My question is: is this constructivism necessary in the development of
> the Iris logic?  Or is it a preference?
>     - A subquestion is: is the constructivism related to the freedom
> from all the axioms in the development?
>     - A remark: it seems that constructivism is applied somewhere, and
> isn't elsewhere.  For example the (CMRA-extend) rule merely requires the
> existence of the decomposition, and not the construction of the
> decomposition.

I think there are two separate (but related) points you are bringing up
here: Constructivism and using functions vs. using relations.

We are working in Coq, which is a constructive logic.  We generally try
to design things such that we don't need to assume any axioms in Coq
(and so far, this worked -- Iris is axiom-free).  This means that
everything we prove is constructive, including properties stated as
relations, like CMRA-extend.  So, in that sense, we are guided towards
constructivism by our desire to not assume any axioms.
  (This is particularly valuable for the core logic; it means that users
of Iris have the freedom to pick any axioms consistent with Coq and
don't have to worry about compatibility with axioms that Iris needs itself.)

Furthermore, when working in Coq, there is a design decision to be made
in many places whether something is written as a relation or as a
function. In some cases (like composition and limits), it is just so
much nicer to have a function (and the relation would have to be
functional anyway) that we decided to go with that. In other cases, a
relation is good enough and/or there is no good reason to enforce
functionality, and then we go with existential quantifiers and define a
relation.

Of course, if we were to assume a strong form of Choice, functions and
functional relations would be equivalent, so the two points above are
related.

Kind regards,
Ralf