[Pitch] Dependent Types & Universes (Stage 1 of Proof-Driven Development?)

Evolution Pitches
, , ,
28

In Swift enum cases already return things. For many intents and purposes they do look like static functions. You just don't need to provide a body for such function. This is perfectly valid Swift 5.7:

enum Expression {
  case bool(Bool)
  case number(Int)
}

let caseFunction: (Int) -> Expression = Expression.number

print(caseFunction(42))
// prints `number(42)`

The main limitation is that cases of generic enums always return Self with an unapplied generic argument:

enum Expression<T> {
  case bool(Bool)
  case number(Int)
  case sum(Expression<Int>, Expression<Int>)
  case and(Expression<Bool>, Expression<Bool>)
}

// this makes sense
let b = Expression<Bool>.bool(true)

// fine too
let n = Expression<Int>.number(42)

// wat
let nonsense = Expression<Int>.bool(false)

// these should be caught as errors by the type checker, but nope
let absurd = Expression<Bool>.number(24)
let moreNonsense = Expression<Int>.and(.number(42), .number(24))
let ohWell = Expression<Bool>.sum(.bool(true), .bool(false))

For the type checker to catch invalid expressions we need to be able to specify return types for cases, which is impossible with Swift as it is right now:

enum Expression<T> {
  case bool(Bool) -> Expression<Bool>
  case number(Int) -> Expression<Int>
  case sum(Expression<Int>, Expression<Int>) -> Expression<Int>
  case and(Expression<Bool>, Expression<Bool>) -> Expression<Bool>
}

This feature in other languages is called Generalized Abstract Data Types (GADT) and is most probably a prerequisite for ergonomic dependent types. This is what allows both Action and ActionSequence in the state machine example above to be enums with a fixed number of cases that you can match against in switch statements, like for any other enum.

2 Likes