Afaics, the issue I raised after reading the research paper @keean introduced, has nothing to do with resource lifetimes. The issue is about intersection of types and subsumption elimination.
Agree, but afaics the issue here is whether we can subsume (coerce) a mutable reference with the type Read /\ Write (aka in Rust trait ReadWrite : Read + Write) to a mutable reference with the type Read or Write.
So this tells me Rust can do subsumption elimination contrary to what I thought @keean had shown based on my prior example code. So now I need to return to my prior argument that mutable referenced subsumption elimination with intersection is unsafe. So I need to compose a new code example to show that, now that I understand how to make it compile.
That is the entire point. That the compiler allows to coerce a mutable reference for a trait object with type NatPos to type Nat to set a 0 value on a Nat, then coerce the original NatPos it to a Pos and read a value of 0 out of the Pos reference. I need to construct a code example to show that unsafety.
Are you claiming an unsigned is not a postive integer. I understand you are complaining (as if it is my fault) about the infamous Circle-Ellipse and Square-Rectangle dilemma of mutably referenced subtyping as I explained upthread. I am confident you will now agree it is just a well known dilemma and not my mistake. As I explained upthread, the unsafety can only be avoided by enforcing immutability. I am contemplating that is why Haskell doesn't have this unsafety.
As I've indicated previously, resource lifetime annotation is a feature I am currently not interested in and am avoiding learning and including in my code examples. Whether I will be later convinced of its utility is still an open question for me. I am more focused on the typing system orthogonal to the lifetimes at least for now.
I don't think you have shown any unsafety. I think you are explaining something about types and trying to apply it to constraints on types (traits), which seems like a category error to me.
If I have a Box I can only put things in that implement both Read and Write. The type of the thing in the box never changes, in fact it cannot change. All you are doing is looking at the same type through different 'lenses'.
Okay I have looked at the code and there is nothing surprising, you are trying to enforce a constraint on writing to a type that provides two interfaces, what do you expect? You can obviously write using either interface, and you don't need anything that complex to do it.
Subsumption elimination has been applied to the intersection type Nat + Pos.
Because Nat and Pos are orthogonal interfaces, which is entirely the means of composability. I expect that the compiler can't check that my invariants are disjoint, thus can't insure safety of my invariants.
You can't without a coercion to subsume from the intersection type Nat + Pos to the orthogonal types Nat and Pos of the intersection. The problem is as I stated from the start of the discussion upthread: the assumption of orthogonality is erroneous because the compiler has no way to check that the invariants of Nat and Pos are disjoint.
There is a type SomeData that is u32, and you wrote a 0 to it legitimately using write from the Nat interface, and then read it using read it using read from the Pos interface. You implemented both interfaces on the type, so its working as expected? The question is can a single thing be both Pos and Nat? I don't see unsoundness here, I just see a bad categorisation.
Whether the intersection is first-class as in the research paper you cited, or is in trait NatPos: Nat + Pos {} is afaics irrelevant. Do you have a reason to think otherwise? The point is that intersections make assumptions about disjointness of invariants which the compiler can't check in the presence of shared references and mutability. The impl NatPos for SomeData {} implements the shared reference by putting the dictionary for the each of the intersected types in the same trait object. Afaics, this is all analogous to the unsafety outlined in the research paper:
With immutability, we don't get this unsafety. Thus Haskell doesn't have this problem. Rust is attempting to do typeclasses in a mutable context, and so it does have this unsafety.
Of course all languages with intersection inheritance have this problem if they allow mutability and shared references to the intersected types. So this is an old problem, that C++, Java, Scale, etc all have too.
class Nat x where
to_nat :: Int -> x
from_nat :: x -> Int
class Pos x where
to_pos :: Int -> x
from_pos :: x -> Int
data SomeData = SomeData Int
instance Nat SomeData where
to_nat x = SomeData x
from_nat (SomeData x) = x
instance Pos SomeData where
to_pos x | x > 0 = SomeData x
from_pos (SomeData x) = x
is_some_data :: SomeData -> SomeData
is_some_data = id
main :: IO ()
main = do
x <- return $ is_some_data $ to_nat 0
putStrLn(show $ from_pos x)
*Main> main
0
Immutability can't save you from this It don't think its unsafety, its just obviously bad design if you have two write methods to the same data type, where one has a check and one has not. This is not a compiler enforced invariant, which is something not many languages have.
Yes. If there is no mutability, then there is no problem. An immutable Circle is an Ellipse. An immutable Square is a Rectangle. But an mutable Circle is not a mutable Ellipse. Mutability is the distinction of this infamous problem of maintaining invariants in the presence of subtyping.
The problem with the 'subclassing' languages is different, you can write an int, and read it as a float, IE the types are actually changing. Here the type of 'SomeData' is never in any question and there is no type coercion. SomeData is always SomeData.
Enforce a constructor on the typeclasses and then you can't do this. You are not enforcing the invariants of Pos on construction of the instance.
You've stripped away encapsulation entirely, which would be obvious if I had bothered to figure out how to enforce a constructor, i.e. enforce encapsulation of type.
Nope, NatPos is the type constructor which encapsulates the data. Actually encapsulation like in an object is not a functional concept, but where is used, it is done with modules.
Without encapsulation, then we can't enforce the invariants, so the entire discussion is pointless if we will forsake encapsulation. If you can initialize a type with any value you want violating its invariants, that is not an argument.
You've stripped away encapsulation entirely, which would be obvious if I had bothered to figure out how to enforce a constructor, i.e. enforce encapsulation of type.
What encapsulation, type classes do not provide encapsulation. My Haskell code is fine there is no problem.
What you want to do is enforce the invariant on the function that uses it. If I want a Pos I should write:
f<A>(a : A) -> A where A : Pos
Now I know whatever type you pass it provides a 'pos' interface. It is up to the implementor of Pos to make sure they honour that invariant.
This problem is really no more than this:
fn returns_a_string(i : u32) -> u32
To really enforce invariants requires applying some proof theory and statically proving invariants are not violated.
Note, the unsoundness with intersection types is far worse, as you can actually do what we have been doing with interfaces with the types themselves. IE mixing an Int with a Float, or far worse am Int with a Pointer. If you look at all the Rust and the Haskell examples the types are always constants (SomeData is always SomeData, we are just using two different interfaces to the underlying type).
With typeclasses, data is orthogonal to interface, thus we can operate on any data with the correct structure employing any its implementing typeclass interfaces, even if the data is in violation of the invariants of any of those interfaces.
Thus we can't enforce any constructor with naive typeclasses. There is no encapsulation.
In theory, perhaps we could add encapsulation by requiring that every such coercion (i.e. from a struct to a trait object) is checked by a copy constructor or is constructed with the trait's constructor method. I need to think more about this.
One of the myopias in our analysis above is that NatPos is unable to elide/override the write method for Nat. If NatPos enforces that it can't be set to 0 without first coercing it to a Nat, then afaics your counter examples fall away.
It don't think its unsafety, its just obviously bad design if you have two write methods to the same data type, where one has a check and one has not. This is not a compiler enforced invariant, which is something not many languages have.