9
$\begingroup$

I implemented a basic generics-free, parameterless trait (type class) system. And I want to parameterize my trait system. The alternative paths I know of are Generic Associated Types (GAT) and Higher-Kinded Types (HKT). In my opinion HKT seems to be more expressive.

For the following GAT usage,

trait MonadGAT {
    type Unplug;
    type Plug<B>: MonadGAT;
    fn pure(a: Self::Unplug) -> Self::Plug<Self::Unplug>;
    fn bind<B, F>(self, f: F) -> Self::Plug<B>
    where
        F: Fn(Self::Unplug) -> Self::Plug<B>;
}

impl<A> MonadGAT for Option<A> {
    type Unplug = A;
    type Plug<B> = Option<B>;
    fn pure(a: Self::Unplug) -> Self::Plug<Self::Unplug> {
        Some(a)
    }

    fn bind<B, F>(self, f: F) -> Option<B>
    where
        F: Fn(A) -> Option<B>,
    {
        self.and_then(f)
    }
}

The equivalent HKT usage would be something like:

trait MonadHKT<M<~>> {
    fn pure<A>(a: A)-> M<A>;
    fn bind<A, B>(self: M<A>, f: A => M<B>) -> M<B>;
}

impl MonadHKT<M<~>> for Option {
    fn pure<A>(a: A) -> Option<A> {
        Some(a)
    }
    fn bind<A, B>(self, f: A => Option<B>) -> Option<B> {
        self.and_then(f)
    }
}

I think HKT is more readable and concise, so I tend to implement HKT.


But I still have some questions:

  1. Are the upper limit of expression ability of the two at the same level?

    • Is there a situation where GAT can express something but HKT cannot, or vice versa?
    • Is there any reason why Rust has to use GAT, since GAT is more complicated?
  2. Are there other ways to parameterize type classes?

$\endgroup$

1 Answer 1

6
$\begingroup$

The two type system features are related, but still quite distinct. For the specific example you’ve chosen, it is possible to encode the same rough idea using either feature, but this is a very narrow view of what the respective features are. To make it clearer why that is, let’s start by considering each of them independently.

Higher-kinded types

Higher-kinded types allow type constructors to accept other type constructors as arguments, rather than only accepting types. For example, in a type system that supports higher-kinded types, it is possible to write a type that represents the sum of two functors. In Haskell, this definition is provided in Data.Functor.Sum:

data Sum f g a = InL (f a) | InR (g a)

In Rust syntax, the above definition would look like this:

enum Sum<F,G,A> {
  InL(F<A>),
  InR(G<A>)
}

This definition is not currently legal Rust, as Rust does not permit higher-kinded types, but it should hopefully get the idea across. The key detail is that F and G are not types, but type constructors, which allows them to each be applied to the type parameter A in the fields of InL and InR.

Using these definitions, it is possible to write the type Sum Maybe Vector Int (in Haskell syntax) or Sum<Option, Vec, i32> (in Rust syntax) to mean “either an optional integer or a vector of integers”. As you can see, this is quite unrelated to GATs, as there are not any traits involved in this example at all.

Another way of thinking about higher-kinded types is that HKTs allow type constructors to be used without being fully-applied. In a language that does not support HKTs, a bare type like Option is essentially a syntax error; all type constructors must appear applied to the appropriate number of arguments. This is not entirely dissimilar from languages that do not (directly) support higher-order functions: in Java, it is illegal to refer to a bare method name without applying it to arguments. Higher-kinded types allow type constructors to be passed around as if they were types in much the same way that higher-order functions allow functions to be passed around as if they were values.

Higher-kinded typeclasses/traits

In a language that supports HKTs, it is natural to also support higher-kinded typeclasses (traits in Rust nomenclature). For example, in Haskell, a commonly used typeclass has the following definition:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

Again, in hypothetical Rust syntax, this might look like this:

trait Functor {
  fn fmap<F,A,B>(self: Self<A>, f: F) -> Self<B>
  where
    F: Fn(A) -> B;
}

This translation is a little bit more confusing than the one above due to the fact that the first type parameter to all Rust traits is the implicit Self parameter, whereas all type parameters to Haskell typeclasses are written explicitly. Regardless, it should once again hopefully get the idea across: implementations of the Functor trait are not types but type constructors, which is what allows Self to be applied to the type parameters A and B in the type signature for fmap.

Here is an example implementation of Functor in both Haskell and (hypothetical) Rust syntax:

instance Functor Maybe where
  fmap :: (a -> b) -> Maybe a -> Maybe b
  fmap f x = case x of
    Just v  -> Just (f v)
    Nothing -> Nothing
impl Functor for Option {
  fn fmap<F,A,B>(self: Option<A>, f: F) -> Option<B>
  where
    F: Fn(A) -> B
  {
    match self {
      Some(v) => Some(f(v)),
      None    => None,
    }
  }
}

Note that this uses the syntax impl Functor for Option, not impl Functor for Option<T>, as the whole idea is that Self is the unapplied type constructor.

Associated types

Associated types are an extension of typeclasses that allows type declarations to appear in the body of a class declaration. For example, we might define a class that provides conversions between signed and unsigned versions of an integer type (once again in both Haskell and Rust syntax):

class Signed a where
  type U a
  toUnsigned :: a -> U a
  fromUnsigned :: U a -> a
trait Signed {
  type U;
  fn to_unsigned(self) -> Self::U;
  fn from_unsigned(Self::U) -> Self;
}

Again, the specialness of the implicit Self parameter (and the use of method dot notation) makes the correspondence a little less direct, but the concept is the same. Here is an example instance for 8-bit integers:

instance Signed Int8 where
  type U Int8 = Word8
  asUnsigned = fromIntegral
  fromUnsigned = fromIntegral
impl Signed for i8 {
  type U = u8;
  fn to_unsigned(self) -> u8 { self as u8 }
  fn from_unsigned(x: u8) -> i8 { x as i8 }
}

One way to view associated types is as type-level functions. The Haskell syntax makes this particularly clear: U is a function that accepts a type and returns some other type. For example, U Int8 applies U to Int8 to get Word8, while U Int16 applies U to Int16 to get Word16. The Rust syntax makes this interpretation a little less clear, but Rust’s associated types still work the same way.

What distinguishes these “type-level functions” from type constructors is the same thing that distinguishes term-level functions from datatype constructors. That is, just as the expression f x can be reduced to another term by applying the function, the type U Int8 can be reduced to another type. This is unlike the expression Just 5 or the type Maybe Int, each of which is already fully reduced and can’t be reduced any further.

Generic associated types

Generic associated types are an extension of associated types, and they are conceptually quite simple: they are associated types that happen to be generic, i.e. they accept type parameters.

In a language that has both associated types and higher-kinded types, there is essentially nothing special about this idea: it simply allows the type-level functions defined by associated types to return type constructors in addition to types. For this reason, the term “generic associated type” is not in use in Haskell; the concept is included in the phrase “associated type”.

On the other hand, Rust does not support higher-kinded types, and as I noted in the previous section, this effectively means that its type system lacks the ability to talk about type constructors that are not immediately applied to arguments. This restriction means that generic associated types must be a special type system feature rather than merely being a special case of the associated type concept.

Since GATs are essentially type-level functions that return type constructors, one way to view them is as a limited and highly restricted form of HKTs. It is therefore unsurprising that some idioms that are usually encoded using HKTs can also be encoded using GATs, but these encodings are usually not exactly the same. For example, let’s consider a GAT encoding of the Functor class from above (which is quite similar to the definition of MonadGAT from your question):

class Functor (Unplug a) => Functor a where
  type Plug a :: Type
  type Unplug a :: Type -> Type
  fmap :: (Plug a -> b) -> a -> Unplug a b
trait Functor {
  type Plug;
  type Unplug<B>: Functor;
  fn fmap<F,B>(self, f: F) -> Self::Unplug<B>
  where
    F: Fn(Self::Plug) -> B;
}

If you consider that Unplug is essentially a function from a type to a type constructor, you may be able to figure out why this definition of Functor is not precisely the same as the one from earlier. Here is an instance of the GAT version of Functor that illustrates the difference:

instance Functor (Maybe a) where
  type Plug (Maybe a) = a
  type Unplug (Maybe a) = List

  fmap :: (a -> b) -> Maybe a -> List b
  fmap f x = case x of
    Just v  -> [f v]
    Nothing -> []
impl<A> Functor for Option<A> {
  type Plug = A;
  type Unplug<B> = Vec<B>;

  fn fmap<F,B>(self, f: F) -> Vec<B>
  where
    F: Fn(A) -> B
  {
    match self {
      Some(v) => vec![f(v)],
      None    => vec![],
    }
  }
}

This instance is completely legal and is accepted by rustc today (given an implementation of Functor for Vec<A>), though it is probably not the instance that is desired: it results in Some(false).fmap(|x| !x) evaluating to [true]! This should not be completely shocking—the Unplug associated type is an arbitrary function, and the only restriction placed on it is that it must have an implementation of Functor. This is quite different from the more obvious encoding using HKTs, where type functions are not involved at all and the constructor is referred to directly.

Returning to your questions

With the above out of the way, allow me to finally answer your questions.

Is there a situation where GAT can express something but HKT cannot, or vice versa?

Yes.

As illustrated above, even attempting to encode the same thing using these features yields different results. Comparing the two directly is sort of a category error, as GATs are a special case of associated types, while HKTs are a pervasive type system feature. The Sum functor from the section on HKTs cannot be encoded using GATs (no traits are even involved, so GATs are simply not relevant). Likewise, HKTs alone certainly do not provide the ability to define type-level functions.

Is there any reason why Rust has to use GAT, since GAT is more complicated?

Again, this is sort of asking the wrong question, because it makes it sound as though these are two alternatives, and that Rust has chosen GATs over HKTs. This is almost backwards: Rust needs GATs precisely because it does not support HKTs! As mentioned above, if the type system natively supports both HKTs and associated types, support for GATs comes more or less for free.

This shifts the question to why Rust does not support HKTs more generally. The answer to that is nuanced and would likely be better suited to a separate question, but one reason is that HKTs pair particularly nicely with partial application, something that Haskell pervasively supports but Rust does not. In Haskell, a multi-argument type constructor like Either has kind Type -> Type -> Type, and that constructor can be partially applied as Either e to yield a type constructor of kind Type -> Type (which is the right kind to support a Functor instance).

Haskell programmers generally accept this design choice, along with all the tradeoffs it entails, such as the inability to partially apply the second argument but not the first. This has substantial ramifications on library design, so that approach is unlikely to work in Rust, but alternatives are substantially more complicated.

Are there other ways to parameterize type classes?

I’m not sure what you mean (and this question seems potentially very broad). Regardless, it’s usually best to only ask one thing per question, so I will decline to answer it here, but feel free to open a separate question (with more details) about this.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .