Another major advance for programming language design from me!
I am starting to fire on all of my cylinders as I used to do when I was prolific. Damn illness the past 4 years held me back. I am feeling pretty good.
I need to backup this info some where, in case every Rust forum private threads disappear. So I am putting this here so others can read about my design progress.
I think we should first enumerate the cases where
anonymous (as opposed to nominal
enum and nominal
trait A: B + C) unions and intersections would be useful to eliminate boilerplate and enable expression, before discussing whether and how to integrate them.
1. Intersections on nominal trait bounds. Rust already has this.
2. Unions of nominal data/function types and/or type parameters for function arguments and result types.
3. Unions for data/function types for the element type of first-class heterogeneous collections (avoids the alternative HList-style boilerplate and conflation of semantics). Subtyping subsumption or trait bound subsumption are not extensible in both directions of the Expression Problem.
4. Unions as the locally (not principle typings) inferred type of an expression, e.g. an
if-else. Otherwise all branches of a code block must have the same type or we must employ the boilerplate of a nominal
enum (which obviously can't be inferred).
Can you think of any other use cases? Especially any for intersections?
We do not want intersections of data/function types because that puts the anonymity on the outside of the type, i.e. it is no longer a data/function type and thus we introduce structural typing! Intersections of trait bounds can only be written on type parameters.
Rust matches closure functions on structure, but the structure
is always on the inside of a nominal trait bound. We don't want to introduce structural typing because it causes inference divergence and perhaps also unsoundness.
My current thinking is that you can simply leave intersection and union types out of inference, so all inferred types are monomorphic, that way the type inference can look like HM.
Exactly my thought too as evident by my prior post wherein I think I enumerated all the use cases for first-class unions and intersections and they are all explicit annotations and/or local expression inference that is constrained by the annotated function signatures, so no need to involve first-class unions and intersections in principle typings inference.
The question then would be how to introduce them. You could have first-class-polymorphism and introduce them in a datatype.
I am not thinking this is necessary, but if you can show an example where it can only be sound that way, I am interested to see it.
Really type-annotation is necessary. We can stick to the 'only infer HM' types rule, and then it would be up to the programmer to annotate as appropriate.
Yes that is what I have always been thinking I wanted. The
inference would only be for the expressions within the function body.
I just don't see global inference as desireable. I understand there are some cases where local expressions require annotations due to failure of inference, but that failure will be less like with first unions.
For example, in that Scala
example that required needless type annotation of casting a
None to
Option[Int], the
Option would not be a nominal type in my proposed language. Instead the type would be
Int \/ (). So thus combining an
Int and
() in the same expression would produce an
Int \/ () inferred type.
To keep it simple, I probably would not have traits as well, nor would i have structs and enums, as these can all be constructed from intersection types.
I have explained that we need nominal types as that is how we differentiate from the structural types, so the structural types are never inferred as principle typings (instead only function signature annotations or as intra-function body expression types).
I am trying to basically have Rust but with unions, GC, and async runtime. Will be a better Rust for high-level programming.
Then I'd like to explore our mutual idea for minimizing the need to use GC for temporary objects lifetimes correlated with the program stack.
1. I've just glanced at your cited references and of course reminded that System F isn't generally decidable for principle typings inference. If I understand correctly, all your concerns with first-class unions and intersections is due to the need to have principle typings inference. If we annotate all free standing function declarations (lambdas in function argument expressions excepted), then the concern would be vanquished. Correct?
2. You are concerned that function annotations could become very noisy because for example intersections of trait bounds could become quite large. For example, a function needs certain trait bounds for the operations it performs in the function body, plus it needs to require all the trait bounds for any functions it calls. I have an idea for a solution to this if we (or I) were to decide to abandon principle typings inference. We could have each function only declare the trait bounds that it needs in its function body, and the additional trait bounds required by functions called within the function body, would be inferred onto the calling function's trait bounds. Since those called functions explicitly declare their trait bounds, then this is decidable. It is a tree structure.
3. Afaics, the ability to exclude certain traits is inherent in my complete solution to the Expression Problem, because the dictionaries are supplied to the function orthogonal to the objects that contain the data types; thus it is impossible to cast a polymorphic data type downstream to any trait bound that wasn't annotated on the function declaration. Thus to specify NoIORead, then simply don't add a IORead trait bound to the function. But you wanted to infer the function's types, because of #2 above. Apparently one of the reasons you think the intersection of types would be so large, is because you want to infer the fully generality of the principle typings, thus you allow for a larger set than the function even desires, e.g. if the append method is employed within the function, you would infer any trait bounds with any append method. But this seems to dangerous. I prefer for the programmer to be explicit about his semantics. So if the programmer must constrain the append method, then he might as well just write that constraint as a trait bound annotation on the function signature. So really I am failing to see the benefit of principle typings inference?
4. The interaction of HRT (and I presume HKT) with first class intersections and unions complicates principle typings inference, and likely makes it undecidable if not just incredibly complicated. Another reason to abandon principle typings inference, because first-class unions and intersections are essential from my perspective in order to make the code more elegant and less boilerplate.
One of my other goals is to make the compiler as fast and as simple as possible. So not having complex inference unification solvers would be advantage. I am thinking also there is a better chance of not having corner cases in the type system and bugs in the compiler.
These points were made upthread and I am thinking they still apply.
Btw, you mentioned Ceylon but it doesn't have type classes.
Afaik, HRT (higher-ranked types) are necessary when we need to input a polymorphic function, then resolve the function application polymorphism within the function body, i.e. not monomorphic. Instead we enumerated other solutions which are monomorphic:
1. Making that polymorphic function a method of nominal trait Foo and inputting Foo.
2. Or inputting a separate function for each polymorphic variant of application in the function body.
3. Or inputting a function employing unions for the variants, when the semantics are acceptable.
Afaik, HKT (higher-kinded types) are necessary when we need to abstract over the type constructor of ourself (speaking from the perspective of a data type). So for example,
Self is a HKT when it is an result type in a trait, because this means any application of that trait requires to know which data type implemented that trait.
We can see this more clearly in Scala, where we would write:
trait Foo[Self <: Foo[Self]] {
def myself: Self = this;
}
class Bar extends Foo[Bar];
We can see that
Self is abstracted over the construction of a type instance of
Foo by the
class ... extends, which is sort of analogous (not really) to an
imp ... : in Rust.
I don't see how HKT breaks monomorphism?
I think the unsoundness in the interaction with unions or intersections would only be occurred if we try to put them in the declaration of the definition of a HKT:
trait Foo[A, Self /\ A <: Foo[Self]] {
def myself: Self = this;
}
class Bar extends Foo[Int, Bar];
But can't even see the use cases where that capability would be useful. Do you?
I am thinking of only allowing HKT on
Self.