Blog post series: Alternative type constructors and HKT

[withoutboats]

The same ellision rules could be applied as normal, so realisticially Iterable would look like this:

trait Iterable {
    type Item<'a>;
    type Iter<'a>: Iterator<Item = Self::Item<'a>>;
    fn iter(&self) -> Self::Iter;
}

For the purpose of explaining this, making the lifetime in iter explicit can be helpful, which is why I think Niko did that here.

[withoutboats]

You usually do not want any sort of “backlink” relation with associated items, “family traits” are the only exception. In general, a single type could be the associated type of many different trait impls. In the example I just posted, for example, &'a T would be the <_ as Iterable>::Item<'a> for Vec<T>, VecDeque<T>, HashSet<T>, BTreeSet<T>, Option<T>, and many others.

[steven099]

I’m confused as to why you can’t infer List<32> when the caller annotated it with ListFamily. I’ll keep reading but I want to take notes as I go: it seems like you know you need a Family, you were told it’s a ListFamily, and the only way to get a collection from ListFamily is with List.

I was also confused by the issue steven99 pointed out with the linked list prepend impl.

Interestingly, these two issues are related.

The problem in the blog post is that the caller has to annotate the function with the ListFamily parameter. Ideally, the fact that the argument is a List<i32> should let us infer that the output type is List<f32> without any annotation. But we can’t, because there’s no way to work backwards from List<i32> to ListFamily. In order to solve this, an associated type is added to Collection<T> to tell us what the type family is for a given implementer.

My earlier comment demonstrates a similar type inference issue. Basically, with HKTs, the type family of List<i32> should just be List, so we don’t have to introduce a dummy type (ListFamily) and link it all together with associated types. With a type like Pair<T, U>, however, there’s more than one possible type family it can belong to. I chose to denote those families as <T> Pair<T, U> and <U> Pair<T, U>. The existence of more than one possible type family means we can’t infer the type family for a given type. For Pair<T, U>, this means we can’t determine if the sibling for f32 should be Pair<f32, U> or Pair<T, f32>. This is basically the same inference problem as in the blog post. The associated type added to Collection<T> solves it in the blog by forcing each type to belong to exactly one type family. The question is what the equivalent solution would be in the situation I presented.

[leonardo]

One nice part about avoiding “true HKT” is that we get to sidestep some of the thorny questions that it raises. In particular, the challenges that full HKT poses for inference.

Giving up some type inference is acceptable if this makes writing and reading code simpler than the code you write with family traits.

[kristoffer]

I second this comment. Having to design an extra trait, an extra empty struct, and link (and backlink) things together in an extra boilerplate impl is a lot of work for the ability to talk about “partially filled types”.

Also, I am not certain at all whether this is equivalent to HKT in the case of having more than one type parameter. Is it as flexible? What if I wanted to fill only one parameter in a two-parameter type? Using a two parameter type as a one parameter type is simple with the associated type constructors but you still need to make a trait for every arity, I think.

More importantly, this also completely breaks when you want to use a Result as a one parameter type two different ways. I mean, that’s a bad example, maybe, but I can imagine that somewhere in the future it’s going to be handy to want to link a two parameter type to some kind of family trait through both parameters, and people are going to find out they aren’t able because they already tied the knot with the associated types.

The fact that you explored this path (using associated constructors) shows that HKTs really suck to implement in Rust! Thanks for all the hard work you’ve been doing, Niko, and I am certain that whatever you and the rest of the lang team will settle on is going to be great as usual!

[withoutboats]

More importantly, this also completely breaks when you want to use a Result as a one parameter type two different ways.

Haskell does not allow this either though.

[arielb1]

Giving up some type inference is acceptable if this makes writing and reading code simpler than the code you write with family traits.

The problem is that injectivity is sort of a swamp that I’m not sure we want to go into - it comes with a “magical” set of rules for whether types match or not. We already have this with higher-ranked unification and it’s bad quite enough.

[tupshin]

FWIW, I’m playing with iterator-like behavior and modeling something that needs to be both a regular container, and a self-consuming iterator-like thing as well, with a signature of: pub trait Dynamo { // Yes, I’m secretly an iterator fn next(self) -> Option<(Self, T)> where Self: Sized; }

Would be nice if any HKT-oriented traits could encompass consuming signatures as well.

[nrc]

I’d love to see some more ‘formal’ discussion of the motivation for HKT. I love the intellectual challenge around the language design, etc., but from a practical point of view it is really hard for me to weigh various proposals against each other without having a more concrete idea of why we are doing this. Getting into the details as in these blog posts is fun, but seems premature without having clear goals and use cases etc. Given that it is such a big feature (in terms of complexity), it seems like a good opportunity to use a motivation RFC or something similar as we’ve discussed in the past (in particular, I don’t really see how HKT of any form fit into the 2017 roadmap).

[withoutboats]

I completely agree! Where I really feel we need some degree of higher kindedness right now is ATCs of lifetime arguments. This is necessary to express several abstractions we know would be useful (Iterable and StreamingIterator are prominent examples).

Beyond that the utility is a little less clear. I often want HRTB of type arguments, but I less often want ATCs of type arguments. Its even rarer that I want “higher order type constructors” (which I think is what most people think of as “full HKT”; type constructors with the kind (type -> type) -> type like Foo<T>(T<u32>) for example).

I think the reason that the thought process has gone this far is this: we knew we wanted ATCs, especially of lifetime arguments. We knew that we had to restrict them to be compatible with higher order type constructors in the future (as has been alluded to in this thread several times). The questions that have arisen are:

• What specifically are the restrictions we’d need to place on ATCs to be compatible with “full HKT”?
• Is “full HKT” worth placing those restrictions on ATCs?

[Ericson2314]

Right now, I see far more crates defining functions than data structures. I think the lack of a standard collections trait hierarchy is squarely to blame, and as this blog post nicely accidentally indicates, any collections hierarchy done entirely without HKT is going to be annoying to the point where nobody uses it.

[As others have I think regular users would actually turned off more by this fancy associate type hackery boilerplate than HKT: slight unfamiliarity + boilerplate where the exact design of the boilerplate is extremely subtle is way scarier looking and judicious use of feature made for the task! In generally I find the assumption here that HKTs are scary and hard to teach irksame. In my mind, HKT is a classic example of a language feature that’s hard to design and but easy to use. You need to deeply understand HKT to design the ATC hack, but regular HKT collections hierarchy probably will look pretty tame at first glance.]

[Ericson2314]

Another common thing is the need to be parameterized over &'a T vs &'a mut T. Interestingly, I don’t think that associated type constructors (or HKT) really gives us that! The problem is that borrow expressions operate on paths, and we have no way to reify that distinction right now.

A bit off topic, but for anybody intrigued by this, we can solve this problem with a type for borrowed fields, and more interesting function types. Then an ATC on a HKT-Self trait would be the most elegant library code to exploit this.

[leonardo]

I’ve just read the third blog post. When I see code like this:

fn floatify_hkt<I<_>>(ints: &I<i32>) -> I<f32>
    where for<T> I<T>: Collection<T>

This suggests to also take a look at the C++ “Concepts Lite” proposals, because they face problems similar to Rust HKTs. They also propose shorter concept syntaxes that could be handy in Rust too.

[Manishearth]

I just read part 3, and I’m a bit wary of the I<_> stuff. This is mostly a complexity budget issue.

In the first two blog posts, I was very happy with the ATC syntax. This didn’t really introduce new syntax from the complexity budget POV. It filled in syntax that most people would expect to work. Indeed, I’ve seen many people complain that type Foo<T> = ... doesn’t work in associated types and they don’t know why. So to me that was a very elegant solution that gave us most of HKT without increasing the complexity budget. With I<_> in mind, the complexity budget is being spent again, and since uses of HKT itself can get pretty complicated, I suggest we tread very carefully in choosing the syntax and trying to make it look natural. To me I<_> seems like a good syntax, but I’m not sure.

[petrochenkov]

For comparison, a curious history of allocator::rebind pattern in C++: http://stackoverflow.com/questions/12362363/why-is-allocatorrebind-necessary-when-we-have-template-template-parameters rebind is an equivalent of Family/Sibling from the blog post.

It’s fun that after all these years member typedefs/structs (ATCs) are still universally preferred to template template parameters (HKTs) in C++ metaprogramming.

[agrif]

I’ve been looking forward to each new post in this series eagerly, and I have a couple notes about part 3.

So we just saw that we need HRTB to declare that any type I is a collection (otherwise, we just know it is some type). But (as far as I know) Haskell doesn’t have anything like HRTB […]

It may not be possible directly, but with ConstraintKinds it is possible with some type-level hackery and with an ok interface. I would render for<T> I<T>: Collection<T> in rust as ForallF Collection i in haskell, using this library.

(Interestingly, GHCI will happily parse forall a. Collection (f a) and even identify it as a constraint, but won’t let you actually use it anywhere.)

The same problem also confronts collections like HashSet or BTreeSet that require bounds – that is, even though these are generic types, you can’t actually make a HashSet of just any old type T.

This problem usually shows up in haskell-land as “why doesn’t the Set type implement Functor?”

With constraint kinds, that specific problem can be solved by adding an associated constraint type to the Functor class (for an example see this reddit comment), though it’s not clear at all to me if this is a good solution or a scalable one.

However both of these solutions use constraint kinds, which are definitely further down this rabbit hole than HKT alone.

[arielb1]

, and I’m a bit wary of the I<_> stuff. This is mostly a complexity budget issue.

In the first two blog posts, I was very happy with the ATC syntax. This didn’t really introduce new syntax from the complexity budget POV. It filled in syntax that most people would expect to work. Indeed, I’ve seen many people complain that type Foo<T> = … doesn’t work in associated types and they don’t know why. So to me that was a very elegant solution that gave us most of HKT without increasing the complexity budget. With I<> in mind, the complexity budget is being spent again, and since uses of HKT itself can get pretty complicated, I suggest we tread very carefully in choosing the syntax and trying to make it look natural. To me I<> seems like a good syntax, but I’m not sure.

Sure enough. We basically already have HKTs up to syntax and implementation issues (aka the longstanding “non-supertrait-predicates are not elaborated” problem):

pub trait Collection where
    for<'a> &'a Self: IntoIterator
{
}

pub trait RefIter<'a, C> = <&'a C as IntoIterator>::IntoIter;

If we get ATCs to work, I am quite sure RefIter would be isomorphic to an Collection::Iter<'a> associated type up to syntactic sugar (after all, associated types are type-level functions, and currying is a Thing).

[withoutboats]

Syntax is a big issue with “full HKT.” allowing the Self parameter of a trait to be higher kinded also presents a lot issues with method resolution. This is some of the downside of going “that far” on this language feature.

[bluss]

for<'a> &'a Self has that annoying side effect of requiring Self: 'static, which makes it much less useful.

[arielb1]

for<'a> &'a Self has that annoying side effect of requiring Self: 'static, which makes it much less useful.

How is this any different from an ATC? The “magic” of implied bounds should keep this “working” if we can get it to apply, but it should be the same either way. In fact, an ATC would have it worse because there is no place for implied bounds to work their magic.