I thought why change more syntax than necessary when you are trying introduce something new, it makes it harder to see what is new, and what is just a syntax change because you prefer some symbols over others.
I can now see I need to focus on the union of types, as there is nothing new in the intersection of traits (at least I hope thats right?)
Oh I see. Well I am also trying to avoid readers thinking in terms of Rust's semantics because they might confuse some aspect of Rust with my explanation of my proposal. I don't want to insinuate that trait NatPost : Nat + Pos is a first-class intersection, because it is a nominal intersection. I doubt Rust's intersections Nat + Pos (i.e. without the trait name) are first-class every where?
Apologies.
I think they are, you have seen the definitions above where I specify "Iterator + Readable" in the generic function definition itself.
So how does this work? When I declare a vector do I need to define the union?
type MyType = Vec<String \/ u32>
If so how is it extensible?
Yes I had noted that, but I wasn't sure if that meant they were first-class every where that a type can be declared. Thanks.
Yes.
trait Vec<T> {
fn appendItem<A>(&mut self, A) -> Self<T \/ A>;
}
So I guess it requires HKT. Without HKT, we would have to discard the data type of the collection and replace with a trait:
trait Appendable<T> {
fn appendItem<A>(&mut self, A) -> Appendable<T \/ A>;
}
Does that look correct?
I can see what you are getting at, but types not have 'state' they are pure values so you cannot mutate a type. A type variable has to be replaced with the same type everywhere (unless it is part of a polymorphic recursion). So this:
trait Vec<T> {
fn appendItem<A>(&mut self, A) -> Self<T \/ A>;
}
is impossible because A != T / V otherwise you cannot make a transitive closure over the program.
Even if this were possible the type of the collection is now not statically checkable, but a runtime property, for example:
if b {
collection.appendItem(myString);
} else {
collection.appendItem(myU32);
}
We can when the LSP is checked and the language supports subtyping (not subclassing not needed). The return type Self<T \/ A> is a subtype of Self<T> and thus can be assigned to a Self<T> reference. But I now see the problem. The supertyped reference would not know to check all the types in the collection. Darn.
.
but then you lose track of the union and you simply regard the collection as Self, now you cannot check all types in T provide the traits you want, because you only have T.
Right. There may be a way around this though. I'll think about it for a bit.
Thanks. I will also.
The only solution I can see is immutability. But perhaps we can do it without copying the entire vector, at least for simple operations such as append. For more complex operations where the self type needs to be mutable, then T can't be changed by the operation. My proposal is more amenable to List.
Well that is good, so maybe we don't need subtyping.
I remember now that long ago I had reasoned out that my idea required immutability when adding data types to the union of the collection ValueType. And I had also realized it eliminated the need for subtyping. Actually it requires there be no subtyping. I had forgotten those details, but quickly reminded once @keean helped rediscover the issue upthread. I may have written those points publicly some where in the past.
Essentially afaics my proposal is combining first-class type unions, first-class trait intersections, a global (or scoped?) hash dynamic dispatch, and optional immutability to allow for first-class heterogeneous collections which are open in both dimensions of Wadler's Expression Problem, i.e. can add new data types and new interfaces orthogonally without recompiling nor boilerplate from before what one already has at any location in the source code. And this apparently eliminates subtyping entirely (which typeclasses didn't have any way, e.g. Haskell, Rust, and PureScript).
But I wrote that only immutability can be allowed with my proposal for first-class union types. And subtyping can't be allowed and won't be required if immutability is required. So your stated problem doesn't exist in my proposal.
A boxed trait is open to extension w.r.t. to the traits that can be applied to the collection without rebuilding another copy of the collection. That is a boxed trait is open in both directions of the Expression Problem. I have already explained this several times.
You are conflating the orthogonal issues of scoping, inference, and the Expression Problem. My proposal is to enable extension in both dimensions of the Expression Problem. It is orthogonal to those other two issues. There is nothing you can propose on the other two issues which can solve the Expression Problem, because they are orthogonal issues (an abstract analysis convinces me of this orthogonality but you may need to convince yourself by trying and rejecting numerous proposals).
That belies understanding of why the Expression Problem is fundamental. We can't solve the Expression Problem with scoping, analogous to that we can't substitute scoping for first-class functions and retain the same composability.
The scoping you proposed only constrains when adding to add collection, but it doesn't allow (nor adequately substitute for) the degree-of-freedom of later binding the matching of data types to implementations when we want to apply the collection or one of its element items as the input to a function which requires a trait. You are requiring that the caller of that stated function is also the creator of that collection or has required that trait on his caller. But that defies dependency injection, which is a fundamental golden rule of composability. Even your Sort example upthread is employing dependency injection (yet you only can vary along one dimension of the Expression Problem because you don't have my proposal implemented in any language on earth yet).
If you still retain that same stance after this post, please provide rationale for why solving the Expression Problem is not an important problem ???
The motivating example is as I had stated upthread, that any time one needs a heterogeneous collection and they want composability to be open in both directions of the Expression Problem, i.e. they can call any function that the union of data types implements on the required trait. Whereas, without my proposal then there can't be dependency injection in terms of which traits a collection's element type (aka upthread ValueType) can implement. It is really elementary and simple. And I am quite perplexed why no one in computer science has entertained such an idea and solution.
But I wrote that only immutability can be allowed with my proposal for first-class union types. And subtyping can't be allowed and won't be required if immutability is required. So your stated problem doesn't exist in my proposal.
I don't think you understand the problem. Try typing this (what is the type of the container):
let container = Container::new();
loop {
appendItem(container, "A");
}
That belies understanding of why the Expression Problem is fundamental. We can't solve the Expression Problem with scoping, analogous to that we can't substitute scoping for first-class functions and retain the same composability.
I think you misunderstand my proposal, the scoping limitation is to keep things reasonable. You can ignore it for now if you want to convince yourself of the equivalence of the two methods. Lets say the following:
You can extend Shape with a new trait "HasHeight" anywhere you like in the program. If a function requires HasHeight is called on the collection then all types that are a member of Shape have to prove they implement HasHeight (as viewed from the call site of the function).
If you agree this is equivalent I will explain why the restrictions are desirable.
The motivating example is as I had stated upthread, that any time one needs a heterogeneous collection and they want composability to be open in both directions of the Expression Problem, i.e. they can call any function that the union of data types implements on the required trait. Whereas, without my proposal then there can't be dependency injection in terms of which traits a collection's element type (aka upthread ValueType) can implement. It is really elementary and simple. And I am quite perplexed why no one in computer science has entertained such an idea and solution.
This is an abstract motivation, not a concrete motivating example. You need to provide examples of real world programs that people are implementing and that are running into problems with this. For example pick a real problem like implementing a chess player, or a painting program, or something, anything, and start implementing it. When you find you cannot do something, or find that something is really ugly because of this problem then you have a motivating example. Either you will have lots of examples from your own programming history where this has caused you actual problems, or you can search the internet and forums and find other developers developing real programs that have found this to be a problem.
I said appending when changing the union is immutable. Thus your example code above won't typecheck as it requires a mutable reference but the method signature is:
Let me clarify that based on the discussion that followed that quoted example:
trait Vec<T> {
fn appendItem(&mut self, T) -> Self<T>;
fn appendItem<A>(&self, A) -> Self<T \/ A>;
}
Afaics that isn't sound, because this requires the linker to be a compiler. In short, you need to compile all the linked modules at the same time. There can't be any more modularity in code. I could write some new code that breaks code that used to compile in another module.
Even though afaics it can't be sound, I am still interested to read your thoughts about advantages.
I said appending when changing the union is immutable. Thus your example code above won't typecheck as it requires a mutable reference but the method signature is:
Isn't a collection you cannot change a bit useless? How can I do anything with it?
Afaics that isn't sound, because this requires the linker to be a compiler. In short, you need to compile all the linked modules at the same time. There can't be any more modularity in code. I could write some new code that breaks code that used to compile in another module.
No, its fine, it just needs the header files to list the types that implement each trait. The compiler automatically generates a header/interface for each file it compiles. This contains encoded versions of the type signatures of the public functions in a module (otherwise it could not type check when you import a module without repassing the source code). If we extend the interface generated with trait information, which types implement which traits, and which traits are bounds on which other traits, then the compiler can complete these checks in the link phase.
Edit: If you think about it, some, if not all, of this information must be there, so that when you use a module it knows which types inside that module implement which traits (whether defined in that module or another). This is done without recompiling the used modules (unless it has changed since the last compile).
In any case this is no less sound than your own suggestion which would be required to build the 'union' of types across all source modules. In effect the trait represents the union of types that implement that trait.
Remember soundness is the property of a type system to prevent programs that go wrong at runtime from passing the type checker. So with the unions, if you have to check whether a type in the collection implements the trait at runtime, your static type system is unsound.
I don't know why you repeat this incorrect assumption, when I have explained upthread that this is not the case presuming the type system is not allowing subtyping, which means per my example then the type system must enforce immutability when adding an item that has a new data type to the first-class union of the heterogeneous collection. Perhaps you meant in the case that immutability is not enforced by the type system, but as we showed upthread that wouldn't be sound, so I wouldn't create a type system that allows it.
Note even when instead of a first-class union of data types, we employ the conjunction of traits as the ValueType (which btw is not open to both dimensions of the Expression Problem as we explain upthread) then still can't employ subtyping because Self<T /\ A> is not a subtype of Self<T>:
trait Vec<T> {
fn appendItem(&mut self, T) -> Self<T>;
fn appendItem<A>(&self, A) -> Self<T \/ A>;
fn appendItem<A>(&self, A) -> Self<T /\ A>; // Note this can't never be called any way, bcz a conjunction of traits can't be extended bcz we've erased the data types so compiler can't enforce if implementations exist in scope for the added traits
}
So subtyping will never be used in the proposed programming language. Subtyping doesn't exist in Rust now, except for the corner case of lifetimes (which my abstract intuition leads me to believe I will eventually show Rust's lifetimes is an anti-pattern model).
As I showed in my prior example, operations (including appending) which are not adding a new type to the first-class union VaueType (that is the element type of the heterogeneous collection), will type check with a mutable reference to the collection. And as I also showed in my prior example, operations (including appending) which are adding a new type to the first-class union VaueType, will not type check with a mutable reference to the collection.
Additionally, when appending an item which adds a new type to the first-class union VaueType, it is not required to not copy the entire collection in some cases of collection types, e.g. a List and other types of collections which are inherently encapsulated after append w.r.t. to the ValueType. It is even possible to make a DiffArray function like an array for random access, yet make it function like a List for immutability of ValueType. I had posted in 2011 a rough conceptual idea which sort of illustrates the conceptual strategies which can be employed to model mutability of arrays in an immutable context. The Clojure collections exhibit other strategies. There does appear to be at least a logarithmic performance penalty for immutability, but again note the distinction here is that I am only proposing to incur that penalty when adding a new data type to the union which is the ValueType (aka element type) of the collection. So with my proposal we get extension in both directions (dimensions) of the Expression Problem, yet we don't prematurely erase the union of data types and pay no penalty for not erasing them, until if ever we need to do dependency injection extension along the data type direction of the Expression Problem by actually adding a new data type to preexisting element type of a preexisting collection which we couldn't otherwise do (this dependency injection) in the current way Rust, Haskell, and PureScript (typeclass languages) are. Of course subtyping+subclassing languages such as C++, C#, Scala, OCaml, etc.. are hopeless anti-patterns.
It is difficult to explain where it is unsound because afaics you have not specified all the details such a design will require, e.g. how can the compiler convey to the linker that adding a data type to a collection was dependent on a change to the collection's element type at a particular scope. Essentially you have just converted the linker into a compiler, which was my point before. Afaics there simply isn't any way to remove the invariant that the data types that were already in the collection have been erased from the compiler's AST by the time you need to add the new trait to conjunction which is the element type. I am 99.9% confident when you work through the details, you will discover it is unsound and can't be fixed.
How many do you want because the list of use case examples is unbounded. 
For example the web browser's DOM has collections and they are typed according to the known element types, but if we want to make a typed interface with a typeclass language (i.e. not the subtyping+subclassing anti-pattern). So if we want to extend on top of the DOM our own data types, but be interoperable with preexisting code, we could not do it without my proposal. Of course currently the DOM is not modeled with a typeclass language structure, so there are no such preexisting code, but I am speaking about the current way to do it once I'm done replacing the web browser (my current project goal which is why I need a new programming language).
Note again that modeling the DOM with the subtyping+subclassing anti-pattern also does not allow for extension on both directions (dimensions) of the Expression Problem.