Pitch: Dependent Types & Universes
Intro
I'd like to re-open a discussion of adding support to Swift for dependent types, universes, and related features. Dependent types have been pitched twice before (here in Oct. 2017 by @felix91gr and here in Dec. 2022 by @anachron), but there wasn't much discussion or explanation of the ideas, so it seemed best to start a new thread.
General Motivation
Next year will be the 10-year anniversary of Swift. Moore's Law means we get to have nicer things in the future, like Apple Silicon and the Internet of Things. Yet the more powerful and ubiquitous computing devices become, the more damage can result if our software malfunctions.
What will be the paradigm shifts of the next 10 years in software development?
How can I prove that the constraints I've given to someone (or to an AI) are satisfiable?
How can I prove that the code someone wrote satisfies the constraints that I set?
Test-driven-development became a popular answer, but tests aren't proof unless you can prove that the tests cover all the edge cases. Humans are bad at imagining edge cases.
It's not going to be good enough to just write tests and then be happy when an AI writes the code that passes the tests.
Thankfully in the last 15 years, a new set of ideas has matured from mathematics and computer science that can allow us to do proof-driven development.
Imagine you could write static assertions that the compiler can check against all possibilities, combined with the ability to statically constrain the range of possible values that types can represent, founded on a groundwork of paradox-free logic and guard rails that ensures compiles times aren't adversely affected.
The first pieces of proof-driven development that we might need for this are dependent types and universes.
Motivating Use-Cases
The content of this pitch may seem theory-heavy, but there are a wide range of specific use-cases that can benefit from improving the security, reliability, scalability, and maintainability of code that processes data.
The most obvious use-cases where dependent types could be beneficial for Swift code are math-heavy domains like machine-learning, augmented and virtual reality, image processing, gaming, audio plug-ins and music apps, and any app that manipulates streaming data from sensors or external devices. Swift has had a tougher time breaking into these domains vs. entrenched languages like C++ and Metal Shader Language, which might change if Swift offers enough advantages.
You can also find discussions of adding dependent types to C++, in which case interoperability might become an issue.
Those domains aside, my primary motivation is that I feel dependent types would be broadly impactful for most Swift projects, in particular when business-critical information and data validation are performed. For example, large enterprise B2B apps involve data entry where numbers are expected to be within certain ranges. Even basic SwiftUI code could benefit.
While Swift does have features already to help with this at runtime, such as error throwing, logging, and assertions, a preferable and Swiftier option would be to "define away" this whole class of programming error, wherever possible.
General Background
Like every other major paradigm evolution that's been proposed here, the Swift forums are not where these ideas began.
Dependent types and universes are core concepts on the cutting edge of computer science. They have been proven out (literally, no pun intended) over the last 10-15 years in academic and corporate research settings, including the World Championship for Automated Theorem Proving. In 2017, some computer scientists at UT Austin used the ACL2 therem prover to verify a two-petabyte-long mathematical proof.
Several new languages have emerged from academia and corporate labs based on these ideas over the past 15 years. Some of them undergone more releases over more years than Swift has.
These languages and proving systems have now begun to see adoption in the corporate world as tools for formal verification of critical software and hardware systems. For example, ACL2 is used by companies like Motorola and Intel to validate the correctness of hardware chip designs before they get printed to silicon. Microsoft Research currently supports the Leaf Prover system based on these concepts.
So, what can we bring over from these systems to put in the hands of "the rest of us," who may not have a PhD in mathematics or theoretical computer science, that will help us write code that works properly for our millions of users?
Disclaimer: The below "pseudo Swift" examples are just for illustrative purposes, to help explain these concepts to the Swift community. They're not meant as the proposed form of anything.
What are dependent types?
Dependent types are types with value constraints. You can also find a formal definition here.
We already have some ways that types constrain values in Swift. Current examples:
- UInt contrains the value to a 64-bit, non-negative, whole number
- Float and Double specify different constraints on the precision of a floating-point number
- An enum constrains the value to a predefined set of possibilities
Dependent types take this many steps further.
One thing they let you do, is to parameterize the allowed upper and lower bounds statically at the type level. For example, in a language with dependent types, the following declaration might fail to compile:
let x: Int[1...8] = 9 // compiler error: "out of bounds"
Dependent type languages also enable functions where the return type depends on the specifics of the dependent type of one or more function parameters. We could imagine something like:
func f<V: Int>(_ x: V) -> V where V[1...3] {
switch x {
case 1: return 2
case 2: return 3
case 3: return 1
}
}
Or we could imagine a way to guarantee a returned set will have a certain number of elements:
func f<V: Int, S: Set>(_ x: V) -> S where V[1...3], S[3], S.Element == V {
// results from function with switch, above
Set<V>([f(x),f(f(x)), f(f(f(x)))])
}
Swift's existing treatment of optionals with the Optional type can be thought of as a very simple form of a dependent type. While optionals in Swift do not offer the full expressiveness of dependent types, they do capture a dependency between the presence of a value and its type.
In languages with full support for dependent types, such as Coq, Agda, or Idris, you can express more complex relationships between values and types. These languages often provide:
- advanced type-level constructs
- pattern matching on dependent types
- and support for formal reasoning and verification using their type systems
- compile-time assertions about certain relationships between types
- code-generation based on various constraints supplied by the user
- pi types, which are function types whose return type depends on the value of the input argument, are a fundamental building block in dependent type languages, allowing for more expressive function signatures that capture value-level dependencies
- sigma types, which are tuples where the type of one element depends on the value of another element, can be used to express relationships between values and types, and are useful for encoding complex data structures and enforcing invariants
- inductive types, which can define recursive data structures, such as lists, trees, and natural numbers
- coinductive types, which allow for infinite and lazy data structures, such as streams or infinite trees
- productivity checkers that ensure that coinductive definitions produce infinite data structures in a well-behaved manner
- higher inductive types that allow for constructors that introduce equalities between elements of the type, useful for expressing complex topological structures and reasoning about equality
Another benefit of dependent types is that it can increase the accuracy of code analysis by enabling automated code proving, i.e. the process of using automated theorem provers, proof assistants, or other formal verification tools to automatically prove the correctness of code or verify that code satisfies certain properties or invariants. This can help to eliminate bugs, ensure security, and provide stronger guarantees about the behavior of a program. Examples include Coq, Agda, and Idris.
If Swift were to gain support for dependent types and universes, it could potentially open the door to more advanced automated code proving capabilities within the language itself. However, as of now, Swift developers rely mostly on external tools and testing techniques to ensure code correctness and verify properties of their programs.
What are universes?
Universes can be thought of as static, hierarchical sets of types, including dependent types. Universes are known at compile-time and can be used to enforce certain kinds of restrictions and rules about what kinds of types are allowed to be used in generic parameters that dependent types can be specialized over.
The goal of universes is to prevent certain kinds of self-referentiality paradoxes that can compromise the formal guarantees of correctness that dependent types are meant to provide, leading to scenarios where (for example) all code is deemed "correct."
The kind of paradox at question is Girard’s paradox. A very formal explanation of it can be found here, but the short version is to say it's a cousin of Russel's paradox:
Let R be the set of all sets that are not members of themselves. If R is not a member of itself, then its definition entails that it is a member of itself; yet, if it is a member of itself, then it is not a member of itself, since it is the set of all sets that are not members of themselves.
Swift's existing design has ensured that no such paradoxes exist in our current structure of types. We also have features in place to prevent some bad forms of self-reference within the type system and to classify a hierarchy of types without the need for a concept of universes:
- use of Metatype as the type of all Types
- indirect enums
- Covariant 'Self' type cannot be referenced from a stored property initializer
However, dependent types with value constraints incur additional kinds of problems. Universes in languages like Coq enable features such as:
- Type-level computation: Universes enable you to perform type-level computation, which allows you to express complex relationships between types and values within the type system. This can lead to stronger compile-time guarantees, more expressive abstractions, and better error-checking during compilation.
- Well-founded hierarchy: Universes provide a way to organize types into a well-founded (non-self-referential) hierarchy. This can help manage the complexity of a type system, especially when dealing with higher-order or more advanced type constructions.
- Consistency and soundness: Universes can help ensure the consistency and soundness of a type system by preventing certain kinds of paradoxes or inconsistencies that can arise when dealing with dependent types. By separating types into different universes, the type system can enforce a well-founded hierarchy that avoids circularity and other issues.
- Expressive type-level constraints: Universes can be used to define expressive type-level constraints and relationships, allowing you to express precise requirements on the types used in your code. In Swift, this could potentially involve extending the existing support for generic constraints, associated types, and protocol requirements with more powerful mechanisms for expressing type-level relationships.
- Some languages have features to allow a type declaration to be specified as "universe-polymorphic"—that it should be allowed to work across different universe levels.
- In some languages like Coq, the use of universes is an internal detail to the compiler, and is usually hidden from view of the user (although you can ask it to print the universe information). Swift might aim to keep this as a compiler implementation detail.
Universes do this by helping to organize types into a hierarchy, or encosed groups by kind. Universes are more focused on the organization and relationships between types, rather than the specific behaviors or properties that the types share, as with protocols.
Some of the benefits provided by universes can already be achieved in Swift through existing features such as generics, protocols, and associated types. However, full support for universes and dependent types might require more advanced and expressive type-level capabilities, which could in turn open up new possibilities for the evolution of Swift.
What are some examples from other languages?
Example 1: Agda (Indexed Types and Dependent Pairs)
Agda is a dependently-typed programming language and proof assistant that supports universes. Here is a good breakdown of how this stuff works in Agda. Official docs are here.
Example 2: Coq (Vector length enforcement)
Coq is another dependently-typed programming language and proof assistant. In Coq, you can define a "vector" type with a length that is enforced at the type level:
Inductive vector A : nat -> Type :=
|nil : vector A 0
|cons : forall (h:A) (n:nat), vector A n -> vector A (S n).
Here, vector
is a type indexed by a natural number n
, which represents its length. The constructors nil
and cons
create empty and non-empty vectors, respectively. The type system ensures that the length of a vector is enforced at compile-time, making it impossible to accidentally mix vectors of different lengths.
In Swift, you can't express the length of an array as part of its type. While you can use generics to create fixed-size arrays, there is no way to enforce the length relationship between two arrays at the type level, let alone construct compile-time assertions to check whether constraints you have defined are satisfiable.
Example 3: Coq (Universes and Universe Polymorphism)
In Coq, universes help maintain consistency and soundness in the type system. Coq's type hierarchy is built on universes, with Prop and Type as the main universe levels. Universes are used to classify types, avoid paradoxes, and enable universe polymorphism.
Here's an example of a simple polymorphic identity function in Coq:
Polymorphic Definition id {A : Type} (a : A) := a.
In this example, A
is a polymorphic type argument with an implicit universe level. By using Polymorphic, we indicate that the function id
is universe-polymorphic, meaning it can work with types from different universe levels. The actual universe level of A
will be inferred by the Coq type-checker based on how the function is used.
Universes in Coq allow for more precise control over the type hierarchy and can help prevent inconsistencies or paradoxes that might arise from allowing arbitrary self-referential or circular dependencies between types. See the Coq docs here.
Example 4: Lean (Inductive Function Definitions With Successor)
Lean lets you define functions recursively if you have a well-founded relation on the dependent type. For example consider this recursive definition of the common "greatest common denominator" function on the natural numbers:
def gcd : nat → nat → nat
| 0 y := y
| (succ x) y := have y % succ x < succ x, from mod_lt _ $ succ_pos _,
gcd (y % succ x) (succ x)
Because <
is known to the compiler to be a well-founded relation on the natural numbers, and because y % succ x < succ x
, therefore this recursive function is considered well_founded
by the compiler and can thus avoid the kind of paradoxes I mentioned above.
More information on languages that support dependent types can be found on Wikipedia here.
Conclusion
The first compilers were tools that allowed humans not to have to write machine-code directly. As time has progressed, computer languages have become higher and higher level. However, the codebases we're all having to maintain have become increasingly complex as well.
As computers get more powerful, eventually they'll be writing most of our code for us. We're going to need better language features to ensure the correctness of code and ideally, prove that it can't misbehave. This is especially a concern when security is a concern.
If you got this far, thanks for reading this pitch. I hope that it could be a good starting-off point for a discussion about whether any of these kinds of capabilities would be worthwhile to consider for Swift. I'm not under any delusions that Swift ought to be winning Automated Theorem Prover Championships, however I think that there are some very intriguing capabilities from this realm that ought to be worth at least discussing.