Annotation to opt into possibly uncountable types

[vkuncak]

There has been an ambiguity whether polymorphic types in Stainless should be countable.

In a variety of scenarios it seems useful to know that there is a natural number (or a sequence of bits) associated with a value. This is the case for computable values, as we can think of them as data structures, closures, terms, etc.

However, SMT semantics for arrays by default would give arbitrary set theoretic functions, which makes such types non-countable. If we connect such arrays to more general constructs, including set theoretic reasoning, such cardinality considerations become observable in terms of theorems that hold.

We already have @mutable annotation for types that may represent mutable, so I propose that non-computable types also have such annotations.

Proposal

Keep default type parameters to denote immutable countable (possibly finite) types,

Functions are considered countable; the function type, as in System FR, denotes a set of terms.

If a function may take possibly infinite types, we just annotate it with an annotation such as @large.

Consequence

We need to check the semantics of arrays and the operations we have on them to make sure that they are consistent with countable interpretation.

Applications

Without necessarily encoding System FR semantics of Stainless, we should be able to view value of non-large types as countable sets in Lisa. We should be able to talk about equivalence classes on such sets, pick representatives of such as sets to define congruences through kernel functions, etc.

We should also use this opportunity to reconcile the semantics of sets across different solvers.

[vkuncak]

Something to seriously consider is to say that all values of variables (including first-class functions) in Stainless are countable. This is simple and goes a long way. This also means that equality of functions will be documented as non-extensional. We can provide explicit extensional equality for types at a given depth.