RustSydney / talks

Talk requests and proposals for Rust Sydney
http://www.meetup.com/Rust-Sydney/
22 stars 2 forks source link

Higher kinded types, maybe #1

Closed caspark closed 8 years ago

caspark commented 9 years ago

Supposedly higher kinded types are possible now with some contortions: https://github.com/rust-lang/rfcs/blob/master/text/0195-associated-items.md#encoding-higher-kinded-types

I've been meaning to put some time into understanding how this works; I could package it up into a talk if people are interested.

caspark commented 9 years ago

After playing with this for a bit, I don't believe it's possible to get the sample code there to compile at the moment.

I was focusing on the sample for encoding arbitrary higher kinded types: specifically the line type HKT where Apply<HKT, E> = Self; is invalid in today's Rust, because the where clause on associated types was dropped from the associated items rfc (though the text wasn't updated! :( ). It should be possible to replace it with an equivalent where clause on the trait definition, but equality bounds on where clauses for traits are not implemented yet.

Anyway, here's where I got to (had to make a few other changes to deal with the scoping changes that happened):

trait TypeToType<Input> {
    type Output;
}
type Apply<Name, Elt> where Name: TypeToType<Elt> = Name::Output;

struct Vec_;

impl<T> TypeToType<T> for Vec_ {
    type Output = Vec<T>;
}

trait Mappable
    where Apply<Self::HKT, Self::E> = Self // syntax which requires rust-lang #20041 to be closed
{
    type E;
    // `where` is invalid syntax on associated types, so we moved this to the trait bound instead
    //type HKT where Apply<Self::HKT, Self::E> = Self;
    type HKT;

    fn map<F>(self, f: FnMut(Self::E) -> F) -> Apply<Self::HKT, F>;
}

So as far as I'm concerned, this talk will have to wait until we actually get proper HKT support, or at least until rust-lang/#20041 is closed.

srijs commented 8 years ago

Tom McGilchrist gave a talk at a recent fpsyd about higher kinded polymorphism in OCaml, which is achieved roughly the same way.

The paper that introduced the ideas he was talking about is "Lightweight higher-kinded polymorphism" by Yallop and White (2014): https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

The OCaml lib that implements those ideas is here: https://github.com/ocamllabs/higher

His slides are here: http://lambdafoo.com/fp-syd-higher-2015

Maybe that could be further inspiration for this :)

caspark commented 8 years ago

I'm going to close this for now - might get back to it later.