[SR-14045] Generalized enums (algebraic data types, GADTs)

[dan-zheng]

Previous ID	SR-14045
Radar	rdar://17539086
Original Reporter	@dan-zheng
Type	New Feature

Additional Detail from JIRA

| | | |------------------|-----------------| |Votes | 1 | |Component/s | Compiler | |Labels | New Feature | |Assignee | None | |Priority | Medium | md5: d2fd52e3d3d765d906a4ad16c648e2f9

Issue Description:

Motivation

Generalized enums in Swift would be an implementation of generalized algebraic data types (GADTs). They enable enums with cases whose types are more refined, leading to more safety, user-exposed information, and usability - as opposed to using unsafe casts.

See this discussion thread on implementing GADTs: https://forums.swift.org/t/generalized-abstract-data-types-gadts/42298

See this reply for rationale for adding GADTs to Swift: https://forums.swift.org/t/generalized-abstract-data-types-gadts/42298/24

One part of this work will be to write a Swift Evolution pitch. The latest syntax for generalized enums:

// Binary boolean functions.
enum BoolFunction {
  case and, or
  // Evaluates the function for the given operands.
  func callAsFunction(_ lhs: Bool, _ rhs: Bool) { ... }
}

// Binary number functions.
enum NumberFunction {
  case add, subtract, multiply, divide
  // Evaluates the function for the given operands.
  func callAsFunction(_ lhs: Int, _ rhs: Int) { ... }
}

// A simple language of booleans, numbers, and operations.
// GADT syntax is "enum cases with where clauses binding all generic parameters.
indirect enum Exp<T> {
  case bool(Bool) where T == Bool // (1)
  case number(Int) where T == Int // (2)
  case boolFunction(BoolFunction, lhs: Exp<Bool>, rhs: Exp<Bool>) where T == Bool // (3)
  case numberFunction(NumberFunction, lhs: Exp<Int>, rhs: Exp<Int>) where T == Int // (4)
}

// Evaluates an expression to a value.
func evaluate<T>(_ expression: Exp<T>) -> T {
  switch expression {
  case .bool(let bool):
    // (1) Since `Exp` is a GADT, the type-checker gains extra knowledge
    // when pattern-matching on cases.
    // Here, it knows that `T == Bool` when matching the `.bool` case.
    return bool

  case .number(let int):
    // (2) Here, the type-checker knows that `T == Int`.
    return int

  case boolFunction(let function, lhs: let lhs, rhs: let rhs):
    // (3) Here, the type-checker knows that `T == Bool`.
    return function(lhs, rhs)

  case numberFunction(let function, lhs: let lhs, rhs: let rhs):
    // (4) Here, the type-checker knows that `T == Int`.
    return function(lhs, rhs)
  }
}

Motivating use cases

Example from apple/swift-driver: https://forums.swift.org/t/generalized-abstract-data-types-gadts/42298/47

[typesanitizer]

[Again a compiler-y example but] One example of a library using GADTs to ensure invariants is the Haskell
Hoopl library (paper, package docs), where GADTs can be used to ensure the right connectivity. To get a quick overview, check out section 3 in the paper, particularly subsections 3.1 and 3.2.

I've used this library in the past, and having type-level guarantees for well-formedness was helpful in avoiding accidentally optimizing code into other code with illegal control flow.

That said, I think the usefulness of GADTs in the style of Hoopl would be a bit less in Swift because Swift doesn't have higher-rank types, and you sometimes want the ability to write rank-2 functions to handle different cases in a GADT uniformly.