The function should require the trait (or first-class conjunction of traits) it needs so that it can compute generically without needing to destructure the RTTI.
So rewrite that:
fn area(x : Area) { x.area(); }
When the caller invokes the function, the compiler has to check that all the data types in the first-class union implement the trait Area. The dynamic dispatch has to be a global table, else scoping will get hairy.
Tada! 
fn area(x : Area) { x.compute(); }
How is this different to:
fn area<A>(x : a) where A : Area {
x.compute();
}
I think the difference as far as I can tell is that you are proposing the implementation test takes place at runtime instead of compile time. This is unsafe as all it can do if there is a definition missing is crash (well exit the program).
I suppose I had the wrong proposed hypothetical syntax. My syntax seems to require that Area is (or is a supertype) of the disjunction of data types that the caller is supplying. Your Rust syntax is more hypothetically correct, because in Rust's syntax I understand that means Area is a trait bound. Perhaps in Rust's parlance we'd want an &Area because a first-class union of data types (that the caller supplies) will need to be boxed since it is open to extension.
The implementation of the trait Area test occurs at the call site at compile time. The compiler knows the type of the first-class union of data types the caller is supplying as input.
Boxing allows runtime polymorphism, so it has nothing to do with extension:
Vec<A> where A : Shape // is a vector of shapes where everything in the vector has the same type, and we can determine that this is a vector of Squares for example at compile time.
Vec<Box<Shape>> // is a vector of shapes where each element can be a different shape, so the shapes can vary at runtime.
When we add new items to the collection, the first-class union of the ValueType is open to extension, and thus the collection has to box its items, because it can't know a priori what Sized it will need to allocate for each item.
Since the function you showed isn't inputting a collection, then yes I guess it isn't required to be boxed. If A is the ValueType of a collection, then afaics it will need to be boxed.
Since the function you showed isn't inputting a collection, then yes I guess it isn't required to be boxed. If A is the ValueType of a collection, then afaics it will need to be boxed.
That sounds about right. But I don't see how an extensible union is better than a boxed trait?
Remember what I already explained upthread.
We need my solution so we can add new data types to the collection without needing to create a new copy of the collection, while also not prematurely throwing away the data types (from the ValueType of the collection) and subsuming them to hard-coded traits which would only be open to extension in one dimension of the Expression Problem. My solution is open to extension in both directions of Wadler's Expression Problem, as I explained upthread.
Analogous to how first-class functions enabled a new dimension in composability, I am proposing that first-class intersections and unions also do. But afaics what Scala 3 (Dotty) and Ceylon got wrong, is we need typeclass traits to make it work right. I had vaguely tried to describe this idea on the Scala discussion group last year, but I don't think I explained it well enough for anyone to understand what I was driving towards. I was very chronically ill (2012 to 2016) and so limited and also I loath the Google Groups user interface (no edits allowed, no formatting, etc). Since Rust has typeclasses and you are a Haskell expert, I seized the opportunity to leverage your knowledge to make sure Haskell can't already do what I want and to check for my errors. Hehe.
I been batting for first-class unions since 2012.
We need my solution so we can add new data types to the collection without needing to create a new copy of the collection, while also not prematurely throwing away the data types (from the ValueType of the collection) and subsuming them to hard-coded traits which would only be open to extension in one dimension of the Expression Problem. My solution is open to extension in both directions of Wadler's Expression Problem, as I explained upthread.
Right, but this is the same as traits, except I think you are suggesting you can recover the type, but this is unsound, and would represent a type escaping from existential containment.
I really don't understand this at all. I have already explained that the ValueType of the collection will be a first-class union of data types, not a trait nor trait object. That is the key point, that the compile-time test for implementation of the trait occurs later when the collection is input to a function which requires trait bounds on the ValueType of the said collection input.
In short, the complete solution to Wadler's famous Expression Problem is don't prematurely commit to a fixed set of traits and instead keep the data types on data types and only resolve trait implementations on application of functions.
The downside of my idea is that the dictionaries (vtables) can no longer be local and must be global. Or least I haven't thought of an elegant way to scope it otherwise.
That is the key point, that the compile-time test for implementation of the trait occurs later when the collection is input to a function which requires trait bounds on the ValueType of the collection input.
But if you cannot recover the individual types in the union then it seems no different to a trait, and if you can it is probably unsafe The reason it is unsafe is because which type that is part of the union is actually in there will not be known until runtime.
You are repeating the same myopia over and over. Let me try one time to explain it again. The compiler knows the type of the ValueType of the collection and it is a first-class union, e.g. u32 \/ String. A function can require a trait bound on that ValueType of say for example Comparable /\ Eq /\ ToString. The caller applies the collection to the function, and the compiler verifies that u32 and String both implement the 3 traits Comparable, Eq, and ToString. The function can invoke any methods of those traits and the dynamic dispatch comes from a global hashtable that was created by the compiler. All the types have been statically checked. It is perfectly safe.
No. The ValueType is known by the compiler. It has not been subsumed to the top type Any.
You cannot add a type to the union without rechecking the function, so it breaks separate compilation.
You can use Rust syntax for the intersection of traits: Comparable + Eq + ToString.
There is no monomorphism in my proposal. The function is calling the methods via a global hashtable. The compiler makes sure the data types have a mapping in the global table. There is only ever one copy of the function. The function isn't specialized for each input as in the case of Rust's monomorphism.
This is dependency injection.
I have explained already why that is not open to extension.
Please take some hours to think it over. Re-reading the thread may help. I have made all these points already.
Comparabe /\ Eq /\ ToString is the same as Comparable + Eq + ToString, they are both requiring something to implement all these trait bounds, right or wrong? I don't get what extension has to do with this. If my function uses '>' '=' and 'toString' it requires precisely those traits, and it is not going to change unless I edit my function.
If you are putting that as the trait bound for the function declaration, then yes I agree. But why mention that? Minute changes in syntax is not relevant right now on analyzing this proposal. And Rust can't do first-class unions and the global hashtable, so that syntax isn't an alternative way to accomplish my proposal in Rust as it current is.
I thought you perhaps were back on the old topic of needing to define nominal traits, e.g. trait NatPos : Nat + Pos from the other thread. In any case, I didn't see how it could be relevant to analyzing whether my proposal is valid and identifying that no other language on earth currently implements my proposal.
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.