Question is not whether these things are precluded, question is how you want to tackle them. It's not even stating design goals here.

The section on Types has been amended to note that these questions form a part of the ongoing work.

The salient point of this and some other features is that they make it easier to reason about a given program's properties, at the expense of making programming harder.

You put that point well.

The basic concept of subtypes is simple, but establishing a definition of "subtype" that is both useful and sound is far from trivial.

I hope that there is nothing that I've said that could be interpreted as me thinking otherwise. As you mentioned elsewhere, though, they look too appealing to ignore.

For example. mutable circles and mutable ellipses are not in a subtype relationship to each other if there is an updating "scale" operation with an x and y scaling factor (you cannot guarantee that a scaled circle stays circular).
The design space for dealing with this is far from fully explored.

I'm not sure that the language could support mutable structures but I take your point that there are complications.

Also, subtypes and binary operators do not really mix; google for "parallel type hierarchy". (The core of the problem is that if you make Byte a subtype of Word, declaring the (+) operator in Word as Word -> Word will preclude Byte from being a subtype because you want a covariant signature in Byte but that violates subtyping rules for functions. So you need parametric polymorphism, but now you cannot use the simple methods for subtyping anymore.)

Clearly there is more to be done in this area.

The key point to mention is that you want to maintain referential integrity.

The document now mentions this.

Sounds pretty much like the conseqences of having the IO monad in Haskell.

That seems fair to me although the broader impact on an entire program would be different I think.

I think you should elaborate similarities and differences with how Haskell does IO, that's a well-known standard it is going to make the paper easier to read. Same goes for Clean&Mercury.

Something like that is addressed in Related Work. Clean is already on the list but it sounds, from your comments and those of others, as if Mercury may be worth including as well.

It's hard to tell whether it is actually new, too many details are missing.

Certainly you have spotted the vagueness in the types however I think that that issue can be momentarily set aside from the point of view of novelty. The language is purely functional with respect to functions and provides out-vars as the only mechanism for dealing with IO. Let's assume for the moment that that all hangs together: if there is another language that does that, no novelty; otherwise, there is novelty.

Once again, your feedback has been useful and stimulating. Many thanks!

Regards

Rik