Context
Generalized abstract data types (GADTs) are a useful and natural extension of enums (ADTs) in Swift today.
Wikipedia explains GADTs quite well. Haskell's wiki also provides a motivating use case for why you'd want to graduate from ADTs to GADTs.
Motivation
In a phrase, I'd summarize GADTs as "more-typed enum cases". Have you ever wished you could give a type to a specific enum case?
// A simple expression: a boolean or a number.
enum Expression<T> {
case bool(Bool)
case number(Int)
}
// Evaluates an expression to a value.
func evaluate<T>(_ expression: Expression<T>) -> T {
switch expression {
case .bool(let bool):
// Uh oh, we can't write this without a forced-cast (as!).
return bool as! T
case .number(let int):
// Ouch again. Dear type-checker, can't you do better?
return int as! T
}
}
Enter GADTs to the rescue. Pseudocode:
// 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 "the type ascription for each enum case".
indirect enum Exp<T> {
case bool(Bool): Exp<Bool> // (1)
case number(Int): Exp<Int> // (2)
case boolFunction(BoolFunction, lhs: Exp<Bool>, rhs: Exp<Bool>): Exp<Bool> // (3)
case numberFunction(NumberFunction, lhs: Exp<Int>, rhs: Exp<Int>): Exp<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)
}
}
Question
What would be needed to implement GADTs in Swift?
Just curious and wanted to start a discussion. I'd like this thread to focus more on low-level implementation details and feasibility, rather than high-level language feature design (this is not a Swift Evolution pitch) - but certainly the latter informs the former.
Among possible type system extensions for Swift (like higher-kinded types and rank-2 types), GADTs seem to be relatively useful and easier to implement.
Kudos to @rxwei for his Gist teaching me about GADTs in Swift!
It is a neat embedding. Perhaps Swift compiler-supported GADTs can desugar to something like it that is already expressible in Swift today. Or perhaps the compiler can have more infrastructure (type-checking, SIL, runtime) to support GADTs.
]. The method potentially could make the value null again, but Kotlin's flow-dependent type system told me it was non-null. Now, in my case, this was actually correct, but I doubt that the compiler is that smart - it would have to look into the actual implementation of the other method and check all code paths (the latter part actually being equivalent to the halting problem). I'm glad that Swift went another way and requires us to bind unwrapped optionals to a new variable/constant.