Blog post series: Alternative type constructors and HKT

[gasche]

Talking to too many knowledgeable people at once can be exhausting sometimes.

[Eh2406]

@gasche

Talking to too many knowledgeable people at once can be exhausting sometimes.

Quote of the week! So many knowledgeable people in the rust community! I am always so excited to hear what thay all say that I end up to exhausted to work on my projects. My first world problems.

[nrc]

I came across this old comment (well, essay in the form of a comment) from Niko: https://github.com/rust-lang/rfcs/pull/213#issuecomment-65756753. It concerns some potential interactions between default type parameters and the curried form of HKT. To me, it serves as another point in favour of ATC and away from curried HKTs.

[withoutboats]

Default arguments are the primary reason that Niko proposes the restriction be “currying in reverse” - the unbound parameter has to be the first parameter, not the last. So HashMap should be read as a constructor of kind type A -> type V-> type K -> HashMap<K, V, A>.

[glaebhoerl]

I think it’s worth pointing out, just to properly anchor expectations, that probably nothing we design will let us ergonomically abstract over the existing HashMap with HKT-based abstractions. As far as I can tell, for inference to work acceptably, it needs to have either a left- or a right-bias, and HashMap's V type parameter is in the middle. Does anyone know of anything to contradict this?

Likewise, it won’t be possible to ergonomically abstract over both Result and e.g. BTreeMap, because Result's Ok type is on the left, and BTreeMap's V type is on the right. If we had wanted our std types to interoperate well with HKTs we would have had to pay attention to it from the start. At least we’re lucky that e.g. Vec doesn’t have an allocator parameter yet, so if/when we figure out the plan for HKT inference, we could potentially add it in a way which doesn’t interfere.

[withoutboats]

If the abstraction you want is over the value type but not the key type, this is definitely true.

[steven099]

The reason ATC works is because coherence requires any type-trait pair to have exactly one definition of the ATC. If parameterized Self were permitted under the same rules as ATCs, would that not ensure that there’s exactly one type constructor for a given type-trait pair?

trait Collection<T> for Self<T> { ... }

impl<K, V, A> Collection<V> for HashMap<K, V, A> /* as Self<V> */ { ... }

// illegal due to incoherence
impl<K, V, A> Collection<K> for HashMap<K, V, A> /* as Self<K> */ { ... }

Any prefix rule that allows for eliding arguments under certain circumstances would be purely syntactic, and not impact inference. Another thing is that, if you added another (default) argument to HashMap, you could disambiguate:

// no longer violates coherence
impl<K, V, A> Collection<K> for HashMap<K, V, A, ByKey> /* as Self<K> */ { ... }

I haven’t brushed up on what is and isn’t legal for default arguments.

[withoutboats]

@steven099

If parameterized Self were permitted under the same rules as ATCs, would that not ensure that there's exactly one type constructor for a given type-trait pair?

No, the type constructors V -> HashMap<K, V, A> and K -> HashMap<K, V, A> are distinct type constructors, they are not incoherent. This is sort of similar to the fact that impls for HashMap<String, String> and HashMap<u32, File> would not be incoherent.

[steven099]

I understand that the type constructors are distinct, so implementing a higher-kinded trait for two different type constructors able to construct overlapping types wouldn’t be incoherent. What I was suggesting (and what I was hoping to show in my example) was to only allow implementing concrete traits for concrete types, and then allowing Self to act as an ATC. This could be lifted to allow HKT syntax while still ensuring there’s only one type constructor for each type-trait pair. Note that this means that higher-kinded parameters would always have to be constrained by a higher-kinded trait, since otherwise the Self ATC would be ambiguous.

By “lifted to allow HKT syntax”, I mean that, given my above example HashMap<K, *>: Collection<*>. If you allow eliding arbitrary prefixes, this would be HashMap<*>: Collection<*>, and thus HashMap: Collection. If you had two parameters S<*, *>: Trait<*, *>, the mapping between the *s in the type and those in the trait would be fully determinable based on the impl, since a second impl with the mapping inverted would be incoherent.

[withoutboats]

I don’t follow you. We seem to be working from different understandings of how traits / type classes behave, which doesn’t mean that your understanding isn’t a workable solution.

In the model I understand, there’s not really such a thing as a “higher kinded trait” - a trait is parameterized by 1…n terms, at least 1 of which (today) must be a type - the Self type. In “full HKT,” those terms could include type constructors (or indeed, arbitrarily kinded type operators), and the Self term could be any type or type constructor.

My reading if your post is that you seem to have a notion in which the trait itself could be a constructor of a kind like type -> trait, which is interesting but I don’t understand how it works.

[steven099]

Double check the added paragraph in my previous comment if you missed it.

What I’m suggesting “isn’t HKT”. It is to allow Self to be an ATC (i.e. a parameterized associated type). Effectively:

trait Collection<T> {
    type Self<U>: Collection<U> where Self<T> == ImplementingType;
    ...
}

which I’m writing as:

trait Collection<T> for Self<T> { ... }

with the necessary bounds being implied. Note that there is no HKT (yet), just an ATC. One could imagine using this as:

fn map<T, C_T, U, F>(c: &C_T, f: F) -> <C_T as Collection<T>>::Self<U>
where C_T: Collection<T>, F: Fn(T) -> U { ... }

My observation is that, under this system, for any C_T, there’s exactly one type constructor (let’s call it C) such that C<T>: Collection<T> and C<T> == C_T, because of coherence. If you allowed type constructor parameters, you could therefore rewrite this as:

fn map<T, C, U, F>(c: &C<T>, f: F) -> C<U>
where for<V> C<V>: Collection<V>, F: Fn(T) -> U { ... }

Elision rules could then let you write for<V> C<V>: Collection<V> as C: Collection. Note that Collection itself is not a trait in this model, it’s syntax sugar. However, if you squint, you’ll notice that Collection looks a lot like CollectionFamily, and C looks a lot like CFamily, with all the necessary linking handled automatically. If the elision rules don’t work cleanly, an alternative syntax could be provided, like C<*>: Collection<*>.

[withoutboats]

@steven099

What I'm suggesting "isn't HKT". It is to allow Self to be an ATC (i.e. a parameterized associated type). Effectively:

Self cannot be an associated type, because Self has to be an input parameter. I think you know this, but to be very explicit, Rust's syntax around Self is really sugar for trait Collection<Self, T>.

What you seem to be saying is some sugar which expands to

trait Foo<T> where Self = Self::_Self<T> {
    type _Self<X>;
}

And then also some sugar on bounds as well.

Essentially, using sugar to make the family pattern look like you're using "HKT", but never actually having (type -> type) in the kind language.

Something like this seems workable. I want to have the undergirding functionality of ATC to implement the family pattern explicitly, to have a clear understanding of how this sugar would expand and what cases it would solve.

[steven099]

Exactly. I’d renamed the implicit parameter to ImplementingType as a way to get around that exact issue. The way you expressed it is clearer, though.

Note that while I’ve framed it as syntax sugar simulating HKT, I think it would also be valid to frame it as actual HKT, just with restrictions on what implementations you can write. One could say type constructors (type -> type) are first class, and that a type -> trait is a typeclass that applies to these type constructors which is implied by the corresponding impl trait for type but can’t be implemented directly.

Edit: Thinking about it more, it seems like it might avoid some confusion to do:

trait Collection<T> for C<T> { ... }

i.e. allow the user to specify the name of the type constructor and leave Self as Self, in order to avoid precisely the difficulty encountered here. Being able to refer to “this one” in a trait is too useful of a concept to muddy up with higher-kinded nuances. The key point is having an ATC which the compiler implicitly understands as generating Self, and leveraging that to enable HKT(-like) syntax without introducing inference problems or ordering constraints. This is somewhat reminiscent of Haskell, except with the parameters fully specified.