Is it an explicit design goal to not allow type-level functions/computation in Swift?

Evolution Discussion
12

NAND won't help as a lot of other things are still missing. To work on numbers on the type level you'd still need support for recursion with termination checks and/or induction. The other languages that allow this don't use NAND or gates or binary logic at all for their foundations of type-level functions. I really do recommend checking out how they do this and then, as I mentioned in the other thread, translating manually their simplest code to Swift will expose the next steps in getting things off the ground.

It is answered in the Generics Manifesto: with dependent types you'll get type-level functions, and with regards to dependent types there's no explicit design goal to (dis)allow them.

The idea with extensions is interesting overall, but even if typealiases were clearly disambiguated between extensions by the type checker, it still wouldn't help without the recursion as I mentioned above. For example, you could start with the classic natural numbers example from 90% of all available introductions to dependent types:

protocol Nat {}
struct Zero: Nat {}
struct Next<N: Nat>: Nat {}

protocol NonZero {
  associatedtype MinusOne: Nat
}
extension Next: NonZero {
  typealias MinusOne = N
}

typealias One = Next<Zero>
typealias Two = Next<One>
typealias Three = Next<Two>
typealias Four = Next<Three>

struct Sum<N1: Nat, N2: Nat> {}
extension Sum where N2 == Zero {
  typealias Result = N1
}

extension Sum where N2: NonZero {
  typealias Result = Sum<Next<N1>, N2.MinusOne>.Result
}

With this you'd expect Sum<Two, Two>.Result.self to print Next<Next<Next<Next<Zero>>>>, but the problem is with the last extension on Sum, in which the Result typealias does not resolve recursively (and doesn't type check). Maybe there's a way to avoid recursion here, but it would rely on some other primitive type checker behavior allowing to define Sum's Result by induction for all cases.

Don't get me wrong, I'm not saying it shouldn't be possible. If something like Sum above worked, it wouldn't be relegated to a niche of SIMD libraries. It's highly valuable to operate on "type-level numbers" in everyday applications. Imagine something like this:

struct Vector<Element, Length: Nat> {}

extension Vector {
  // guarantees at compile time that the returned vector is not empty
  func append(_ e: Element) -> Vector<Element, Next<Length>>
}

extension Vector where Length: NonZero {
  // no optionals here!
  var first: Element

  // this always works as the type checker won't allow it on empty vectors 
  func dropFirst() -> Vector<Element, Length.MinusOne>
}

extension Vector {
  // guarantees that appended non-empty vectors are not empty
  func append<L>(
    contentsOf: Vector<Element, L>
  ) -> Vector<Element, Sum<Length, L>>
}
2 Likes