Higher Kinded Types Proposal

[CodaFi]

Proposal: Higher Kinded Types in Swift

• Proposal:
• Authors: TypeLift et al.
• Status: Review
• Review manager: TBD

Introduction

Higher-Kinded Types are an extension to the Swift type system that allows for more expressive generic quantification and protocols that are aware of more of the structure of their conforming types. Kinds, used to great effect in Haskell and Scala, have made generic programming with types easier, richer, and safer in these languages, and have recently attracted the attention of the Rust community because of this.

Motivation

The implementation of lawful structures and protocols in Swift occasionally necessitates being able to ask the Swift type system to check the shape of a type, not just its name. To that end, Higher Kinded Types enable not just a new class of programs to be written safely, but open the doors to better error checking and reporting, and the creation of higher-order structures and patterns.

For example, the standard library implements a number of declarative primitives and combinators, among them map. In order to create a model that abstracts over just those types capable of being mapped over, we wrote this Functor protocol:

/// Functors are mappings from the functions and objects in one set to the functions and objects
/// in another set.
public protocol Functor {
    /// Source
    typealias A
    /// Target
    typealias B
    /// A Target Functor
    typealias FB = K1<B>

    /// Map a function over the value encapsulated by the Functor.
    func fmap(f : A -> B) -> FB
}

From this signature, it is possible to implement Functor in a type-unsafe or unsuitably generic way by mixing up the associated types. In addition, because there was no way to indicate the kind of FB, we developed a stack of so-called "Kind Classes" to serve as markers, but the implementor may still overwrite FB with whatever type they so choose. In addition, any type can claim to be this Functor, meaning that quantification over Functor-like things is a fundamentally unsafe operation. This makes our abstraction leaky, fragile, and fundamentally non-composable.

With Higher-Kinded Types, that Functor protocol can be rewritten as such:

NB: Not final syntax, here for demonstration.

// Higher-kinded protocol with no other constraints.
protocol<A> Functor {
    // Inside this definition, `Self<B>` allows exchanging the type parameter.
    func fmap<B>(f: A -> B) -> Self<B> // Self is inferred to have kind * -> *
}

This definition uses Kind inference to enforce that any type that wishes to implement Functor<A> must have at least the Kind * -> * to instantiate the parameter A.

Proposed Solution

The compiler must be modified to produce and check kind information for classes, structs, and protocols. In addition, Protocols must now be capable of introducing kind parameters that are reflected in their conforming types. We demonstrate a proposed syntax for these in the next section.

Detailed Design

Syntax

Unlike GHC, our proposal involves implementing Kinds with just 1 possible constructor * or Kind for the type of data types. True to Haskell's kind system, * and k1 -> k2 (where k1, k2 : *) will be the only possible constructors for Kind. Kind inference for data types proceeds as a consequence of type checking. For example:

Int // Has kind *
[String] // Has kind *
struct Foo<A> {} // Has kind * -> *
enum Bar<A, B> {} // Has kind * -> * -> *
final class Baz<A : Functor, B, C : Functor, D, E> { //... } // Has kind (* -> *) -> * -> (* -> *) -> * -> * -> *

NB: NOT FINAL

The most visible user-facing change will be the introduction of parametrized protocols. The syntax for protocol declarations must be amended:

- protocol-declaration → attributes opt access-level-modifier opt **protocol** protocol-name type-inheritance-clause opt protocol-body
+ protocol-declaration → attributes opt access-level-modifier opt **protocol** protocol-name generic-parameter-clause opt type-inheritance-clause opt protocol-body
protocol-declaration → attributes opt access-level-modifier opt **protocol** protocol-name generic-
parameter-clause opt type-inheritance-clause opt protocol-body
‌ protocol-name → identifier
‌ protocol-body → { protocol-member-declarations opt }
‌ protocol-member-declaration → protocol-property-declaration
‌ protocol-member-declaration → protocol-method-declaration
‌ protocol-member-declaration → protocol-initializer-declaration
‌ protocol-member-declaration → protocol-subscript-declaration
‌ protocol-member-declaration → protocol-associated-type-declaration
‌ protocol-member-declarations → protocol-member-declarationprotocol-member-declarations opt

And, though it does not appear in the grammar, the Self keyword for parameter types must be extended to allow for ‌generic-argument-clauses in protocol type parameter lists.

Errors

New errors that can now be checked as a result:

protocol<A> Functor { func fmap<B>(f: A -> B) -> Self<B> } 

protocol<A> Pointed { func point(x : A) -> Self<A> }

// Kind constraint inherited from `Functor` and `Pointed` declarations
protocol Applicative : Pointed, Functor { func ap<B>(f : Self<A -> B>) -> Self<B> }
protocol Monad : Applicative { func bind<B>(f : A -> Self<B>) -> Self<B> }

extension Int : Functor { // Error: Type 'Int' (*) does not satisfy kind requirement (* -> *)
   // ...
}

extension Array<Element> : Functor { // Error: Array does not implement Functor
    public func fmap<Other>(f : Element -> Other) -> Array<Element> { //... }
}

// Has kind (* -> *) -> * -> *
struct MaybeT<M : Monad, A> = MaybeT { let runMaybeT : () -> M<Maybe<A>> { get; } }


let m : MaybeT<Int, Int> = //... // Error: Type 'Int' (*) does not satisfy kind requirement (* -> *)

func binary<A, B, G : Functor, F : Functor>(f : A -> B, d :  F<G<A>>) -> F<G<B>> { //... }

[CodaFi]

I realize HKT is going to be a very large undertaking and a significant change to the language. So, I'd like to kick off the higher-Kinded types proposal drafting process with this issue. The top comment is the proposal itself, and the comments will be reserved for discussion of current drafts. By the end, we will submit the complete proposal to swift-evolution for community review.

[CodaFi]

Protocols being the most obvious place to start with new stuff, here's a couple versions of our Functor with HKTs:

Version 1: Attack of the angle brackets.

protocol Functor<Self<_>> {
  typealias A

  func fmap<B>(f : A -> B) -> Self<B>
}

Version 2.1: Where clauses with angles

protocol Functor where Self<_> {
  typealias A

  func fmap<B>(f : A -> B) -> Self<B>
}

Version 2.2: Where clauses with no parameter binding

protocol Functor where Self : _ -> _ {
  typealias A

  func fmap<B>(f : A -> B) -> Self<B>
}

Version 2.3: Where clauses with parameter binding

protocol Functor where Self : A -> _ {  
  func fmap<B>(f : A -> B) -> Self<B>
}

[CodaFi]

I lean towards the last of these (because I hate associated types with a passion, but I recognize it requires the most change and a significant amount of syntax.

[pthariensflame]

Can't we regard v2.3 as sugar for v2.2?

[CodaFi]

I wanted to make a distinction between typealiases and type parameters. I don't want swift to start dumping implicit typealiases all over the place - tho it would be a very swift-y thing to do. I was thinking 2.3 would bring the parameter into scope without introducing a new type into the protocol.

[pthariensflame]

Actually, how about:

v1.2: Angles in the outfield

protocol<A> Functor {
  func fmap<B>(f : A -> B) -> Self<B>
}

[pthariensflame]

That would also allow us to write such things as:

// ignore Functor, etc. dependencies for this demo
protocol<A> Monad {
  static func unit() -> Self<A>
  func bind<B>(f : A -> Self<B>) -> Self<B>
}

protocol<M : Monad, A> MonadTrans {
  init(lifting: M<A>) -> Self<M, A>
}

[CodaFi]

What does conformance look like (say, in an extension)?

[jckarter]

Kind is a constraint on a type parameter, so it makes sense to me to have it be a form that appears after the :, which works both on protocols and generic type params:

protocol Functor: <*> {...}

func mapM<M: <*>>(...)

I would focus on figuring out the technical work involved before ratholing on syntax too much though.

[mpurland]

I personally prefer @pthariensflame v1.2 without associated types. I think it would be cleaner and easier to work with.

[mpurland]

I agree with @CodaFi in that v2.2/v2.3 would be a next logical step for the language that is addicted to type aliases.

[CodaFi]

@jckarter I agree, but wouldn't syntax (and tactictly, features to be added) influence those technical details?

[pthariensflame]

@CodaFi I imagine conformance working like:

extension<A> Array<A>: Functor {
  public func fmap<B>(f: A -> B) -> Array<B> { return map(f) }
}

EDIT: Or, for short, extension Array: Functor { … }, although you'd have to use the longer form for Either and the like.

[adamkuipers]

I always thought the way SML was able to encode HKT was the most Swift-like. This requires generic type-aliases, which seems to be a more manageable (and approved by Apple for an implementation) solution.

Taken from https://existentialtype.wordpress.com/2011/05/01/of-course-ml-has-monads/

signature MONAD = sig
  type 'a monad
  val ret : 'a -> 'a monad
  val bnd : 'a monad -> ('a -> 'b monad) -> 'b monad
end

And converted to Swift

protocol MonadOps {
  typealias Monad<A>
  static func unit<A>(a: A) -> Monad<A>
  static func bind<A, B>(monad: Monad<A>, transform: A -> Monad<B>) -> Monad<B>
}

[pthariensflame]

@adamkuipers That representation, and any others like it, requires explicit dictionary passing. I want to avoid that at nearly any cost, and I'm sure @CodaFi feels similarly.

EDIT: Never mind, I misread the proposal. Nonetheless, I don't like it because it's not very “clean” conceptually, and it makes higher kinds second class citizens in the type system.