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

How do you pattern match against chain in switch statements with your code if chain is a function and not a case of an enum? Also, how do you define ActionSequence? It's mentioned as a generic type in your code, but how do you express it with the existing generics system? Is it a struct? Is it an enum? How do you pattern match against all possible states in a switch statement if DoorState is a protocol and not an enum?

I don't quite understand your example, it confuses me that the cases return things. Are they actually functions?

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

// 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.


I am aware of how enums work. But then you meant something like this:

protocol DoorState { }

enum DoorStateOpen: DoorState { }
enum DoorStateClosed: DoorState { }

struct Action<Initial: DoorState, Final: DoorState> { }

extension Action<DoorStateClosed, DoorStateOpen> {
    static func makeOpen() -> Action { fatalError() }

extension Action<DoorStateOpen, DoorStateClosed> {
    static func makeClosed() -> Action { fatalError() }

struct ActionSequence<First: DoorState, Second: DoorState> {
    static func chain<Initial, Intermediate, Final>(
        first: Action<Initial, Intermediate>,
        second: Action<Intermediate, Final>
    ) -> ActionSequence<Initial, Final> { fatalError() }

    static func end<Final>() -> ActionSequence<Final, Final> { fatalError() }

func test() {
    let open: Action = .makeOpen()
    let close: Action = .makeClosed()

    // fail
    let seq0: ActionSequence = .chain(first: open, second: open)
    // ok
    let seq1: ActionSequence = .chain(first: open, second: close)

That code snippet doesn't answer these previously posed questions that arise without GADTs and dependent types:

  1. How do you exhaustively enumerate all states when matching against them in a switch statement? I.e. how do you get a compiler error if you forgot to specify one of the states as a switch branch?
  2. How do you iterate over ActionSequence if it's a struct and chain/end are functions declared on it?

I don't know, I'm not sure what your goal is with the example, so it's hard to say. But in general I'm not arguing against dependent types, I think it sounds awesome, just trying to understand what it actually means.

Are you saying that iteration is one part of it, the difference between what we have already and what dependent types are?

Being able to express these concepts as enums and getting type safety with exhaustiveness checking at compile time is the main difference. You may be able to work around the lack of GADTs and dependent types with protocols and similar hacks, but it will require significantly more code and won't be as type-safe and readable.

OTOH, finding a good way to integrate it with the existing Swift type system and not breaking anything, while not making developer experience worse at the same time is a challenge. I think GADTs on their own are much more lightweight than dependent types, and still move the language in the right direction IMO. Maybe a better approach is to get a consensus on GADTs first, and if that's successful it could get more people interested in more advanced topics like dependent types.

Now that we have a generalized existential representation inside the compiler, as well as implicit opening, it should be possible to implement GADTs using those mechanisms together to represent enum cases that capture type information. @griotspeak had proposed what I think is a nice syntax for them a while back:

indirect enum Expr<T> {
  case literalInteger(Int) where T == Int
  case literalString(String) where T == String
  case add(Expr<Int>, Expr<Int>) where T == Int
  case concat(Expr<String>, Expr<String>) where T == String
  case embed<U>(swiftValue: U, eval: (U) -> Expr<T>) where U: Sendable

No pun intended, but it depends. The simplest way would be to construct a data type whose inhabitants are all even integers by construction.

In Agda you could spell such a type over the naturals as

data isEven : ℕ → Type where
  zero : isEven 0
  plusTwo: (n : ℕ) → isEven n → isEven (succ (succ (n)))

In pseudo-Swift this would be

@dependent enum IsEven<var n: Int> {
  case zero : IsEven<0>
  case plusTwo(n: Int, IsEven<n>) : IsEven<n + 2>

Note the embedding of values into type bounds and the GADTs holding this whole thing together. You don't need GADTs to spell this, it just becomes significantly more annoying as you now have to write a function that constructs this proof.

But I also want to comment on the original pitch here. Yes, dependent types are very cool. I even spent some time trying to hack together a dependently-typed programming language that used Agda's syntax and Swift's runtime type metadata scheme. But in the process, I came to see the enormous complexities involved in even that system. Here are some notable open questions I would like to see answered by anybody looking to add dependent types to Swift:

How Powerful is the System You're Proposing?

There's lots of different grades of dependent types systems. How much generalization do you want to imbue the system with? Can you get away with first-order dependent types, or do you need higher-order systems? Do you actually want GADTs or do you want to truly collapse the barrier between types and values? Can you get away with something like type-level predicates instead?

What is the underlying notion of Equality?

This is the fundamental question driving type theorists and their research. You may want to read The Meaning of Meaning by Hilary Putnam if you haven't already for a crash course in the philosophical implications of intensionality and extensionality. Similarly, I highly recommend reading Thomas Streicher's seminal thesis for a thorough grounding in intensional type theory - it's really quite good and he actually takes the time to write down a lot of the proofs you see elided in the literature. I'm also personally a fan of McBride and Altenkirch's Observational Equality paper even if it has been superseded for the most part by folks shooting for proper extensional equalities.

The notion of equality you pick determines the vast majority of the features you're able to propose from the proof assistant angle. Moreover, it directly determines the implementation of the system in the compiler. From a user perspective, in systems with intensional equalities one spends an awful, awful amount of their programming time justifying the structure of well-typed ASTs to the compiler. I mean, this what it takes to prove to Agda that (x * (1 + y) = x + x * y) which is a fact I would expect any student with a basic grounding in algebra to be able to demonstrate, but which I now have to spoon-feed to the compiler. To my mind, the thing that makes that kind of exercise bearable is that the authors of these languages tend to make their tooling highly interactive, and can often automatically search for well-typed programs that inhabit user-defined types and goals. In earlier extensional systems, one would have to trade such a flexible and powerful equality with either losing sight of the computational content of their proofs or losing other desirable program properties like equality being generally decidable (in the presence of other safeguards like well-foundedness or termination checking or whatever syntactic "shrinking" notion).

Ultimately, I don't think Swift is the right medium to prove out this featureset. What I would love to see instead is if we were to reach out to the communities behind this work and pinch some of the features of their proof assistants, not necessarily their languages. Like, consider the idea of runtime type holes in Haskell. In most modern proof assistants - which have type systems significantly more powerful than vanilla Haskell - you can similarly open "holes" in the middle of your developments and you can work hand-in-hand with the compiler to interactively solve those holes. We have an strikingly similar idea in Xcode today with placeholder tokens, what we're missing is the interactivity and the compilers not stressing so hard about always having tokens filled in. Imagine if you could enter a mode where you could compile those missing program pieces in and run your code. When your program encounters the hole, it could trap to the editor and you could work with Xcode to insert the missing piece, back up, and retry the program's execution. This is the kind of workflow that researchers have been using for decades in these kinds of proof assistants, and that most programmers in industry could only dream of!

If anybody would like a brutalist introduction to Agda, I have formalized an old course taught by McBride in Agda and have answers to most of the exercises available.


Isn't this the same workflow one gets in Swift with fatalError if it's used as an implementation "hole"? Or is there an implied requirement for hot reloading just one function when its implementation hole is replaced with valid code?

It's an extension of that workflow. For one, a hole doesn't necessarily have to be a hard trap. For another, holes in proof assistants are places you can place your cursor and start a conversation with your tools. In Agda, one can ask 'what type of value ought to go here?', or 'what do I have in scope so I can build a value of this type?', or 'I know what type constructor I want to use here, can you refine this hole for me?'. I can't ask Xcode to do any of those things for me with a fatalError.


For people who might be confused by some of the concepts in this thread, I think the Software Foundations series from UPenn should serve as a good introduction.


I’m not sure if we’re discussing specific implementations yet, but if we were to implement value constraints, we’d need to consider overload resolution. Here’s an example with constraints (which aren’t practical but highlight the problem of overload resolution).

struct Array<Element, let count: Int>
  // ...
  subscript(position: Int) where position >= 0 { get }

  subscript(position: Int) where position < count { get }

let a: Array<Int, 1> = [1]
a[0] // Which overload do we choose?

Would be a general compile error for unknown values.

But overload resolution in Swift isn't perfect anyways.

Just as a reference: I mentioned this topic in the topic Dreaming of a “harmless” language mode just created by me.

Frankly I've been waiting a long time for someone to post exactly this pitch. I think that AI (and possibly CAD) is the biggest motivation for me wanting dependent types. As AI operates more broadly in software ecosystems and programming I want tools that can prove certain restrictions in an AI's model or its output in a far more rigorous way that what's currently offered by compilers. Combining that with differential swift my hope is these can also open doors to more bespoke learning architectures to solve specific problems, or entirely different architectures that aren't based just on feed-forward neural networks. For those concerned with adding complexity to the language, I would refer to this, "Our goals for Swift are ambitious: we want to make programming simple things easy, and difficult things possible." https://www.swift.org/ -- not trying to be dismissive of concern, just pointing out the goal should be to make that complexity progressively disclose for those who want it or need it.

Yet from what I'm reading, there's already some clear stepping stones that will get us closer to this vision without yet requiring universes and dependent types in the language, as pointed out. GADTs, const functions, everything codafi pointed out, and actually mainlining auto-diff itself. Not to mention generalizing keypaths to optics and including broadcasting (there was some mention of this in this thread Ongoing work on differentiable Swift - #16 by Troy_Harvey) and whatevers' left in the generics manifesto swift/GenericsManifesto.md at main · apple/swift · GitHub.

Is there good reason "Dependent Types & Universes" is the thing that should be tackled first? Makes me wonder if there's an evolution to the GenericsManifesto or a new manifesto that can accurately capture the 30k ft view of how these pieces should connect and lay out some relative prioritization. Maybe there's a way to split up some of these ideas to be spec'd out a bit and recombined into a larger viewpoint?

P.S. I really liked the straw man syntax discussed in the thread you posted by anachron and also was very excited about that conversation before it seemed to fade away.

1 Like

To elaborate a bit here, my personal wish is that those concerned with too much complexity collaborate with those like myself who really want to see this vision reach fruition, so that we meet everyone's needs.

Just checking: is the leading dot in the case declarations there to mark it as a GADT, or is it just an oversight? Feels strange to deviate from current case declaration syntax like that.

I haven't read very far yet, but I do want to make sure I understand these types correctly.

Would that be like the getValue function in this TS snippet?

interface ValueTypes {
  foo: number;
  bar: string;

function getValue<T extends keyof ValueTypes>(key: T): ValueTypes[T] {
  switch (key) {
    case 'foo': return 1;
    case 'bar': return '1';

This sounds a lot like enums with associated values.

I'm struggling to think of a use case for these, but perhaps it's because I haven't yet seen them in practice.

I've seen this abused in languages that allow this, like TS and C++, resulting in things like type-level mergesort (though it's still not as bad as what constexpr allows). If there's even a slight concern about compile times now, this could cause them to explode.

1 Like

Sorry, that was just a typo on my part.

1 Like