P.S.: Basically, I think we have been misled.  What we have been
trying to achieve is to reflect certain algorithmic pre- and
postconditions in the Scheme runtime type system, which cannot
generally work. (In C++20, we have concepts but these are outside the
runtime semantics; in Scheme, they could find their place in its
syntactic system). Apart from immutability, there are other
interesting conditions where, however, it seems much more obvious that
inventing new types for them is dubious, like a special type for
sorted vectors or for pure procedures.

Am Sa., 23. Mai 2020 um 12:57 Uhr schrieb Marc Nieper-Wißkirchen
<xxxxxx@nieper-wisskirchen.de>:
>
> John, thank you for putting again so much effort into this SRFI
> although my initial question that started this thread was a bit
> belated.
>
> Am Sa., 23. Mai 2020 um 02:00 Uhr schrieb John Cowan <xxxxxx@ccil.org>:
>
> > I have come to agree that making pairs and ipairs disjoint, when they were permitted to overlap before, is too big a change for a PFN.  What is more, it's neither necessary nor even a good idea.
>
> > So I've decided to revert almost entirely to the original approach.  In my latest PR, I once again permit unchangeable pairs to be ipairs, only clarifying that ipair? must not return #t on any pair that can in fact be mutated.  So (pair? '(1 . 2)) returns #t and (ipair? '(1 . 2)) may return #t or #f, but (ipair? (cons 1 2)) is guaranteed to return #t and (ipair? (ipair 1 2)) is guaranteed to return #t.
>
> What are the requirements about (pair? (ipair 1 2))? Is this allowed
> so that an implementation may make ipairs a subtype of pairs (where
> "subtype" is defined through the predicates)? With the new approach, I
> think this would be what we want. It is probably a good idea to spell
> out the requirements, the implications, and the unspecified cases
> explicitly.
>
> > I have also struck out the paragraph about the Liskov Substitution Principle, which is really not applicable to dynamically typed languages.  That also removes the contradiction that this paragraph claimed disjointness whereas the Quotation section said that overlap was permitted.
>
> As the Liskov Substitution Principle has been cited several times in
> the context of immutable strings, I am wondering whether we should
> review that discussion as well. Per Bothner's objections of the
> current state of (immutable) strings in R7RS-large can't be denied.
> Even if we stick to the texts of SRFI 135, the same discussion we have
> been having about ipairs and immutable pair literals can be applied to
> texts and truly immutable string literals.
>
> > Comments?
>
> The newest PR improves the situation, I think. Nevertheless, I am not
> convinced that we have found the optimal solution yet. Regular pairs
> are so deeply integrated into the language and the other libraries
> that I find it hard to believe that SRFI 116 will see much of
> adoption. From a theoretical point of view, there is some motivation
> to have immutable pairs; from a practical point of view, they don't
> seem to add much. By that, I mean: If I have a program that uses SRFI
> 116 and if I replace all occurrences of the SRFI 116 procedures by
> their SRFI 1 counterparts and ipairs by pairs, the resulting program
> will most likely be still correct (unless ipair? is used to
> distinguish pairs from ipairs) and will, with a high probability, run
> faster on most Scheme implementations.
>
> (This cannot be compared with, say, SRFI 101, which has deep
> algorithmic consequences.)
>
> I don't know the ideal way out of this situation, though. What's on my
> mind is something that would work roughly as the const type qualifier
> in C99 (not necessarily in C++). Objects declared with const-qualified
> types would correspond to literals.
>
> This idea would get rid of ipair?, thus removing the ability to detect
> immutability at runtime, which makes a lot of sense as even
> "immutable" values may be mutated (through some non-standard
> procedures). Instead, immutability would just be a semantic
> qualification of objects: When the specification of a procedure says
> that it yields an immutable pair (string, ...), it simply means that
> it is an error to mutate that object afterward. When the specification
> of a procedure says that it accepts an immutable pair (string, ...),
> it simply means that the procedure won't mutate the object. (Whether
> it shall be an error to henceforth mutate that object outside of the
> procedure will have to be stated explicitly.)
>
> The usual procedures like apply, car, cdr, etc. would be applicable to
> immutable pairs.
>
> With this model, one implementation (for example one, whose literal
> pairs can be mutated) may not make any difference to mutable and
> immutable pairs internally (!) (and thus use the same binding for the
> cons and the ipair procedure).
>
> Some other implementation, however, can use its tagging system to tag
> immutable pairs as much as it tags mutable ones.
>
> In both cases, some SRFI 116-equivalents of the SRFI 1 procedures may
> be implemented more efficiently because less copying has to be done
> (because they only have to work under the assumption that
> immutable-qualified objects are not modified).
>
> Illustrating this with C99, the SRFI 116 procedures would be
> equivalents of SRFI 1 procedures with const qualifiers sprinkled here
> and there. (I would have loved to give a good example, but no
> procedure of SRFI 1/116 currently comes to my mind where immutability
> allows for a faster algorithm; for (immutable) strings, there are
> better examples, but the principle would be the same).
>
> All in all, I think this solution is theoretically and from a
> practical point of view quite pleasant. (If we go this way, some
> slight additions should be made; for example linear update variants of
> replace-icar and replace-icdr.)
>
> Marc