You can get around this limitation with disappointing new types:
struct UuidPair<'a>(&'a Uuid, &'a Uuid);
struct IntId<'a>(i32, PhantomData<&'a ()>);
Of course I also dislike this a lot too. But this is the rock and the hard place we’re in between newtypes like this & family traits like in the previous example.
I would note that inertia may be behind this tendency.
In the absence of template aliases (introduced in C++11), template template parameters were a really pain to work with and the work-around was associated type constructors.
In C++11, one can use template template parameters easily: a template <class> class X can accept a template <typename K> using KeyedMap = std::map<K, std::string>;.
In C++03, with no template alias and with no forwarding constructors, you were stuck.
Given that C++11 is only 5 years old, and many code bases did NOT transition 5 years ago but much later (or not yet), ATC has a lot of inertia; and therefore it is difficult to know whether people lean toward ATC because it is "better", because of inertia, or both.
So yes this is fancy, but it gets the job done with minimal boilerplate.
trait Collection<A: subkind_of_type, Self: <A> -> type> { .. }
For the record, it looks like Haskell went with this route:
{-# LANGAUGE TypeFamilies #-}
class Foo m where
type A m a :: *
type B m :: * -> *
instance Foo Int where
type A Int a = Bool
type B Int a = Bool -- error
instance Foo Bool where
type A Bool a = Maybe a
type B Bool = Maybe
Below are two comments, and some side remarks, that jump to mind while reading this blog post series.
First, I think that it is written in Rust’s culture that if you have to choose between inference, expressivity or performance, then type inference is the one people are willing to give up. Some of the design considerations about HKT (and by this I mean “true HKT” which are functions from types to types, by opposition to “type constructors” as in Haskell) make inference difficult, but maybe it’s ok to ask people to add more annotations when they use an advanced feature? When there is a tension with other language design aspects, it looks like the least bad choice: you may also give up on expressivity, but that sounds bad, or you could give up on performance by turning some static knowledge into dynamic information (to simplify the type system and thus help inference), and I’m not sure Rust is the right language for this choice. In short, I would think of a good, solid, expressive design that you like on fully-annotated terms, and then worry about inference later.
Second, you are really going along the path along which the Haskell community has been walking in the last twenty years. Functional dependencies, type families (injective or not), higher-kinded type computation or type constructors, it’s all there. You can get some mileage by reading summary Haskell papers about this stuff, but why don’t you just go talk to the people that worked on all this? Send an email to Simon Peyton-Jones, go visit him, explain the design choices you have considered, and see what he thinks. I’m sure there are others in the Haskell community whose opinion would be very helpful (Richard Eisenberg, Dimitrios Vytiniotis…). Get in touch, go talk to them!
A remark: one way to understand the FooFamily transformation is that you are doing defunctionalization, but at the type level. (Defunctionalization works by collecting the list of functions used in the program, and creating a big enumeration with names for this function, with an “apply” function that takes a function name and runs the corresponding function body, and all function calls replaced f args replaced by apply name_of_f args). Type-level defunctionalization is made a bit more modular by using the fact that everyone can add new type and instance definitions, so the “enumeration of codes” is naturally extensible, but it still a relatively heavy encoding.
Another remark: “bounds on higher-kinded types” is not unheard of. For example, Mezzo has parametrized types over which rich constraints can be expressed using “facts”, such as the following:
abstract table k +a
fact exclusive (table k a)
This is part of an interface that exports table : * -> * -> * (using standard kind syntax), with the information that it is covariant in its second parameter (+a), and that for any k, a, table k a is an exclusive (non-duplicable, uniquely-owned type). Facts can also depend on other facts, such as:
fact duplicable a => duplicable (list a)
Exporting an abstract type and parametrizing over parameters is essentially the same thing, so these “facts” could naturally be found in a “where” clause (note that Mezzo itself has not explored higher-kinded parameters, so it does not support that, but it would be a natural extension to the language and not something scary/unknown).
The primary value point of "true" HKTs over ATCs is that "true" HKTs are type constructors and have the corresponding inference properties. Otherwise, the "family type" trick is necessary in some form.
Can you elaborate on what this syntax is supposed to mean? =)
Sure! Also this is probably better:
trait Collection<A :< type> for Self: <A> -> type { .. }
Collection<A> is a trait where Self has kind <A> -> type. A is a sub-kind of type. Bounds and subkinds are punned, so A: MyTrait makes sense after all as <type>: <kind> by construing the MyTrait bound is the subkind of types that implements the trait. The goal is to be able to do something like HashMap<_, V>: Collection<Hash + Eq>.
I don’t understand how this “subkind” and “punning” business is a better solution than having constraint kinds. Can you elaborate on that?
It may not be better :)! The main advantage is superficial: subkinds work around the awkwardness of having distinct but similar looking type: bound and type: kind. Also compare
Hash -> Hash
to
<I: type> -> exists<O> O where I: Hash, O: Hash
For better or worse, Rust has long sought to reduce the need for type quantification (impl Trait, implicit lifetimes, etc etc), and this punning fits squarely in that tradition.
Finally, now that I realize that HKT is going to require bounds, not having names for things means it’s hard to see how we’re going to declare those bounds. In fact, even the Iterable trait probably has some bounds; you can’t just use any old lifetime for the iterator. So really the trait probably includes a condition that
Self: 'iter, meaning that the iterable thing must outlive the duration of the iteration:
@nikomatsakis I'm not really clear about why this bound would need to be expressed. Its true that you couldn't construct an iterator that lives longer than the iterable type, but this is also true of the receiver in fn<'a>(&'a self). We don't need to say fn<'a>(&'a self) where Self: 'a.
So, clearly it'd be nice if we can avoid it, I'm not sure if we can though. But actually the question you raise is deeper than I originally thought. In particular, I think we need to do a bit more thought about what a where-clause written on an ATC means -- specifically, when will it be verified and so forth? In other words, who gets to rely on what. =)
Let me start by explaining the situation with functions in more depth. In that case, we require that fn callers verify that the types of arguments are well-formed, which then allows the callee to just assume this to be the case. This in turn means that the fn body can assume Self: 'a -- in a sense, it's an implicit where-clause. (*)
We actually pull a similar trick with associated types already. In particular, we say that if you have a projection like <T as Foo>::Bar, then in order to normalize this into a real type, you must first show that the type T is well-formed, along with any other trait parameters (the input types, in other words). This, in turn, means that the impl can assume that the self type is well-formed and so forth.
This is why you can write an impl like this:
impl<'a> Iterator for &'a [T] {
type Item = &'a T;
// ^^^^^ for this to be WF, we must know that T: 'a
}
The problem here is that, for &'a T to be well-formed, we must know that T: 'a. However, because we can assume that &'a [T] is well-formed, that implies that [T]: 'a which in turn implies that T: 'a, so we're all set.
So why can't we do a similar trick with the associated type constructor case? Consider this impl:
impl<T> Iterable for [T] {
type Iterator<'a> = slice::Iter<'a, T>
// ^^^^^^^^^^^^^^^^^^
// again, WF only if `T: 'a`
}
The problem is, the types on the impl in this case don't mention 'a! Knowing that [T] is well-formed doesn't really tell us anything interesting.
So, how then is the impl supposed to be able to prove that T: 'a? There are basically two choices:
We can declare the constraint in the trait (as I did). My intention in doing so was to say that it was an extra condition which must be proven in order to show that a projection is WF. In other words, if you have a type like <T0 as Iterable>::Iterator<'a>, you must of course show that T0 is well-formed (as ever). But, because of the where-clause, you must also show that T0: 'a, which would not ordinarily be required. However, I think this is not quite how we have been thinking of where-clauses placed on ATCs up till now. Let me come back to this in a sec.
Another option would be to impose such a constraint universally. For example, we might say that whenever you have <P[0] as Foo<P[1]..P[n]>::Bar<'a>, then P[i]: 'a must hold for all i, regardless of the particulars of Foo and Bar. This is what we do with the basic WF rules: we say that every input to the projection must be well-formed, even if it wouldn't appear in the output in the end; but this is no burden because WF types are something we always want. This would mean that nobody has to declare Self: 'a, because it is always required. Another way of saying this is that we assume that whenever you have an ATC like type Iter<'a>, we assume that you are somehow creating a reference to the entire self value (not just some parts of it). Or at least we impose requirements that are strict enough for you to do so, whether or not that is what you wanted.
Imposing this constraint universally might actually be the right way to go. I am worried it will be too strict, but I confess I am having trouble coming up with a convincing counter example. Here is an artificial one. Imagine I have a tree of things that can be hashed using the hasher H and which can also be iterated.
trait EncodableTree<H> {
type Children<'iter>: Iterator<Item=Self>;
fn children<'iter>(&'iter self) -> Self::Children<'iter>;
fn hash(&self, h: &mut H) -> usize;
}
The universal requirement now says that that, whenever we make a child iterator, the hasher H must outlive 'a, even though the hasher is not part of the data being iterated. Now I write some generic code that gets a tree and a hasher:
fn foo<'x, 'y, T, H>(tree: &'x T, hasher: H) -> T::Children<'x>
where T: EncodableTree<H>
{
tree.hash(hasher);
tree.children()
}
The problem here is that we now have a relationship created between 'x (the lifetime of the tree we plan to iterate over)
and H (the type of the hasher). This code would probably fail to compile without a H: 'x clause (though one could imagine adjusting the rules for implied bounds so that it is implied; currently we don't add implied bounds for projections, since the caller may legitimately normalize them). This bound shouldn't really be needed, in any case.
But I want to pop the stack to one other point. In my original example, I wrote in the trait where Self: 'a, but I wasn't thinking clearly about the meaning of a where-clause in a trait. Normally, where-clauses in traits are promises that impls make to people using the trait: so if I write trait Foo: Bar, that means "every impl of Foo must also be able to show that there is an impl of Bar". In this way, people who have a bound T: Foo can rely that T: Bar must also hold. Similarly, with an associated type, if I write trait Foo { type Output: Hash; }, I am saying "impls must only provide types that implement Hash". But that type Iter<'a> where Self: 'a was saying something different -- it was saying "the impl can assume that Self: 'a holds".
Currently, the way that impls make assumptions is by adding where-clauses to the impl. But those assumptions are verified at the point where we check that Foo: SomeTrait -- basically, this is provable if we can find an impl of SomeTrait for Foo whose where-clauses are satisfied. But the Self: 'a constraint is different, because we don't know 'a at that point. This would be a where-clause which the projector must satisfy, and that is something new.
So, yeah, an interesting question. =) I'm not sure what the best answer is yet. It seems clear that we can't expose this subtlety about who is promising what to whom in surface syntax. So maybe the implicit requirement that "'a must outlive all input types" is better (though we had similar rules for projections that wound up being too painful, iirc). Or maybe I am not thinking about all this straight and there is an easy solution I am overlooking.
That's because the where-clause is in an associated item - where-clauses on methods work exactly in this way (of course, ATM we require the trait method where-clauses to be duplicated in the impl, but we could just "automagically" assume them when checking the impl method).
For example, if we want to desugar an impl Trait on a trait to an ATC, we would need this kind of bound.
Of course, we need more kinds of examples of ATC uses to figure out what we want here.
In the list function for the type inference example, did you intend to write let mut iter = v.iter()?
Right. I'm realizing that there are two different worlds colliding here, in that respect. And what's most frustrating is that both uses are reasonable.
That is:
trait Iterable {
type Iter<'a>: Iterator<'a>
// ^^^^^^^^^^^^ impl should prove it
where Self: 'a;
// ^^^^^^^^ projector should prove it
}
I suppose the distinction is whether the where clause references the item itself (as in the first case, which of course expands to Self::Iter<'a>: Iterator<'a>) or not (as in the second case). It makes some sense because, if the item is not being referenced, then this is a condition that the projector can certainly verify. That may be a clue as to a rule we could use, though it has a "syntactic scan" aspect to which I don't love.
Yes.
Two thoughts: one about complexity, and the other about motivation.
There's a really important distinction here between the ATC and HKT proposals. ATC has a much clearer path to implementation and simpler mental model -- in particular, generic functions in traits are essentially already a form of ATC, since the resulting function types are parameterized by those generics. As @nikomatsakis put it to me, we're just a refactoring away. In particular, ATC doesn't require changes to unification, nor deep changes to the trait system (in particular, figuring out how higher-kinded Self should work). Note also that even in a world where we have HKT, we would certainly have ATC as well, and likely would want something like the proposed syntax.
You're right that we need to be piling up strong motivations, and fitting this story into the roadmap, before we go too far down this road. (Keep in mind the blog series is just a writeup of in-person chats.)
@withoutboats and others have offered one of the key motivations for ATC, namely, lifetime-parametric types in traits, which is needed for expressing associated iterators, just to pick a simple example. But another major motivation is impl Trait in traits, which essentially amounts to ATC.
A concrete place this kind of thing comes up: you have a trait with a method that takes a closure. You want to take that closure unboxed, and return some type that involves it (perhaps implementing a further trait along the way). But you can't -- that would be an associated type constructor, not just an associated type.
This kind of situation arises in libraries like futures-rs all the time. While there are workarounds, they usually force you into very unidiomatic places, and result in difficult to learn and use libraries. So in terms of roadmap, some (minimal!) work along these lines may be justified by e.g. a mixture of the server goal and learning curve/productivity. But any such consideration should also take into account the work involved, which, for ATC, seems to be relatively small.
I think the right path of action here is:
for bounds.I tried to engage really actively on the r/programming thread to find use cases for HKT in C++. Though a lot of users had been rather insistent that Rust needed this feature, it was hard to get down to really specific use cases for it. It doesn’t seem like it’s being used in C++ for abstracting over collections or even over smart pointers, as we’ve considered.
In modern C++ you don't really need HKTs for abstracting over collections. For example range-v3 just uses SFINAE to detect whether something is an lvalue container that provides a push_back operation and defines the push_back::Concept on top of this (if it quacks like a duck...).
When something that is not a container quacks like a container you can implement a trait for it saying that it is not a container using template specialization:
// By default everything is a container:
template <typename T>
struct is_container : true_type {};
// `my_type<T, Allocator>` looks like a container but isn't one:
template <typename T, typename Allocator>
struct is_container<my_type<T, Allocator>> : false_type {};
I don't think that this uses HKTs either since I am not using template my_type<class, class> anywhere.
EDIT: FWIW I went through the source code of Blaze and Eigen3 (two C++ linear algebra libraries) looking for HKT usage and found effectively zero use cases there (Blaze has an utility function for pointer casts and Eigen3 uses it in some performance measurement utilities, but nothing major).
Do I understand correctly that your example List<T>::prepend implementation contains typo: instead
self.cell.next = Some(Box::new(cell));
should be
self.cell = Some(Box::new(cell));
?