Blog post series: Alternative type constructors and HKT

[withoutboats]

It also encompasses more cases - you can have a Collection<T> which isn’t constructed by a Container, but you can’t have a Collection<T> which doesn’t have an associated CollectionFamily because of the way the backlink works.

[glaebhoerl]

The infamous Scala SI-2712 might also be very relevant here. My hazy impression is that the situation in Scala is something along the lines of: they allow arbitrary type-level lambdas (similar to associated type constructors without any ordering/number-of-uses restriction on variables?), but will only infer the cases where you in fact have a type constructor partially applied in-order to some number of type arguments. But I’m not really familiar with it.

I deeply share @gasche’s sentiment that we should get in touch with the people who actually designed and implemented this stuff for Haskell and Scala (and perhaps other languages, if applicable). Increased cooperation across language communities can only be to the benefit of everyone involved. What have we got to gain by going it alone?

[Torsten]

I’ve just started reading the first post of the blog series and struggled already to fully understand the background info on traits. So I ran the example and found some typos. Here are my changes to make it compile in case anyone else wants to play with it:

11c11
<     cell: Option<Box<ListCell<T>>
---
>     cell: Option<Box<ListCell<T>>>
32,33c32,33
<         let cell = ListCell { value: value, next: old_head };
<         self.cell.next = Some(Box::new(cell));
---
>         let cell = ListCell { value: value, next: List { cell: old_head } };
>         self.cell = Some(Box::new(cell));
42c42
< pub struct ListIter<'iter, T> {
---
> pub struct ListIter<'iter, T: 'iter> {

[gsingh93]

@nikomatsakis Can you make these corrections? Your posts were well written, but things like this make it hard to follow posts about complicated concepts; I waste time wondering if I’m wrong and missing something, or whether there’s an actual mistake.

[withoutboats]

@glaebhoerl @gasche I’d be happy to talk to folks who have worked on these issues in other languages, but I don’t know the best way to reach them. Recommendations?

[gasche]

@withoutboats I would just send them an email. You need to decide who is “them” (one good option is to just write to SPJ, which acts as somewhat of a steward on these questions, and trust him to include whoever is relevant to the conversation), but it would also help to have a reasonably compact description of the question and design space you considered – @nikomatsakis’ blog post are thorough and excellent in terms of explaining the design process to the Rust community, but maybe they could be condensed in something that fits in a couple pages to not scare new readers away. On the other hand, you need to keep code examples in, because they are important and useful to follow what you are talking about – especially across communities with different vocabularies and backgrounds.

If you decided to submit a ML workshop talk on higher-kinded types in Rust (the next edition of the ML workshop is in September 2017 in Oxford, UK), you would have to write a two-page extended abstract in the typical dreaded two-column ACM format. That might be a reasonable format to constrain oneself to concisely explain the problem – although you should feel free to sprawl more pages in one-column format, two-column is the worst for code examples.

@glaebhoerl rightly pointed out that the Scala community struggled with these questions as well. To my knowledge the most up-to-date public document on this discussion is the summary by Martin Odersky, Guillaume Martres and Dmitry Petrashko of the several approaches that have been taken to represent higher-kinded types in Dotty, the clean-slate Scala compiler effort: Implementing Higher-Kinded Types in Dotty. You should feel free to contact both groups.

My (fairly uninformed) gut feeling, however, is that the Scala discussion was more concerned with representation within the new Dependent Object Types (DOT) core language/formalization of Scala’s type system, and therefore more likely to draw conclusion specific to Scala’s design and implementation approaches, while the Haskell community tends to have a fairly general approach to these design questions that will transfer more easily to other languages.

[glaebhoerl]

Another option might be to send an email to the haskell-cafe@haskell.org mailing list (and/or maybe glasgow-haskell-users) to see who is interested. There are quite a lot of knowledgeable people lurking in the Haskell community (type theorists, compiler implementors, original inventors of things) so casting a wide net might have benefits.

I’m much less familiar with the Scala community, though it seems like a greater proportion of them are active on Twitter.

I was grepping the PDF linked by @gasche to see if it references SI-2712 and found the link to the actual pull request implementing it which further links to an in-depth explanation which are both probably more useful than the link to SI-2712 itself which I had posted earlier.

[gasche]

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

[Eh2406]

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]

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]

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.