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

Evolution Pitches
, , ,
1

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.

Links

Good YT video about dependent types in Haskell

23 Likes
2

This is really exciting and I'm looking forward to creating arrays of a certain length! Using numpy for ML projects, it was very unpleasant to get runtime errors for matrix operations that are evidently wrong at compile time.

However, your pitch is very theory-heavy and I have trouble understanding what exactly would be a good feature for Swift. Swift is very pragmatic so despite the theory behind dependent types, I think we need a specific motivating use case. For example, the auto-differentiation pitch did a really good job of providing motivation for a more theoretical/niche feature. Also, before implementing any functionality outlined in the pitch, we need to consider compile times. Swift already has a slow compilation compared to other languages (like Go or even Typescript?), so we need to ensure that formal validation checkers are fast.

You obviously have an advanced understanding of dependent types. So my question is what feature do you think is a good starting point with an enticing motivation and the ability to be efficiently implemented into the compiler?

10 Likes
3

Everything in a computer's RAM is a number. Dependent types let you write logic to handle numbers is a far safer manner. The use case is, people who write code :smile:

But also it sounds like you just gave a specific use-case: making matrix operations safer.

Matrix math is heavily used across a wide range of industries and applications from games to machine learning.

If you are working with matrices, you usually need a function that safely multiplies two matrices. Matrix multiplication requires the number of columns in the first matrix to match the number of rows in the second.

In a Swift with dependent types, we could enforce this constraint at the type level, making it impossible to compile code that multiplies incompatible matrices.

Here's a pseudo-Swift hypothetical implementation using dependent types:

struct Matrix<T, Rows: Nat, Columns: Nat> {
    let elements: [[T]]
}

func multiply<T: Numeric, A: Nat, B: Nat, C: Nat>(
    _ mat1: Matrix<T, A, B>,
    _ mat2: Matrix<T, B, C>
) -> Matrix<T, A, C> {
    // Perform matrix multiplication and return the result
}

In this example, Nat is a universe of natural number types that can represent dimensions. Key here is that any dependent type that has bounds on the values of the numbers can be used.

The Matrix struct is parameterized by the element type T, which represents the elements of the fields in the matrix. The number of Rows, and the number of Columns are dependent types in Nat.

The multiply function takes two matrices and enforces that the number of columns in the first matrix (B) matches the number of rows in the second matrix by using the same parameter (B) for both.

With this implementation, if you try to multiply two incompatible matrices, the code will not compile:

let mat1 = Matrix<Int, 3, 4>(...)
let mat2 = Matrix<Int, 5, 6>(...)
let result = multiply(mat1, mat2) // Compile-time error: incompatible matrices

Before dependent types, I'd have to:

  • throw an error
  • catch the error at all call sites
  • log and gracefully handle the caught error
  • write tests to ensure the errors get thrown when invalid operations are attempted
  • write tests to ensure thrown errors are handled gracefull
  • hope I did not miss an edge case in any test

All those things make my code less scalable and less maintainable.

And if there was an edge case not covered in the tests, we still might ship malfunctioning code to the customer.

Then maybe my employer gets sued because it was their software and the bug caused 450,000 people to lose money. Maybe my employer gets hit with a class-action lawsuit for $25,000,000.

That may sound like an exagerration, or a hypothetical worst case, but I can assure you it isn't. Very few things in life are more practical than things that help you not get sued. Getting sued sucks.

3 Likes
4

I've previously explored dependent types in a language with Swift-like syntax in Kara, and that looked promising, but I do agree that the time it takes to compile your code becomes much less predictable with dependent types. I personally think that explicitly marking functions and constant bindings as evaluable at compile time is a better approach than the one I initially took with that language. I no longer work on that project though.

I do agree that making a theory-heavy pitch puts a quite high barrier for potential adoption. Maybe approaching it from the side of compile-time evaluation, and then finding a way for compile-time functions to participate in the type system could be an interesting direction.

8 Likes
5

Anything that lets us limit the range of possibilities our code has to handle ought to make it more predictable, not less. But I have never worked with Kara, so I'm curious why you found their implementation of dependent types to be unpredictable.

I feel dependent types are just a next improved evolution over the existing ways we have to limit and define possibility spaces, like optional unwrapping, enums with pattern matching, and literal constants.

Thanks. I updated the text of the General Motivation and added a section for practical use-cases. Hopefully that helps to convey the less theoretical side better.

Most of the best trends to hit the shores of our mainstream languages have originated within these kinds of theory-driven, research-type languages. Heck, computing itself was once thought of as just a weird thing math people like Alan Turing theorized about, and in the Swift Concurrency Manifesto, @Chris_Lattner3 cites Pony, Erlang, and a Ph.D thesis as the sources of the actor-driven concurrency model.

Since implementations of dependent types have now been around long enough to be mature and have the hardest lessons out of the way, with multiple languages and industrial use-cases out there, it seems worth considering as something with broader potential benefits.

3 Likes
6

It's not the implementation that is unpredictable, but the amount of work the compiler has to do for an arbitrary piece of code. The fact that Swift allows operator overloads for arbitrary combination of types already makes things not so great with "Expression too complex" errors. I don't expect things to improve if we allow operators to be not only type checked, but also evaluated at compile-time for the purposes of type checking itself.

This is something that Idris 2 tried to address, but I don't think that goes far enough. In a practical implementation I wouldn't want a value 42 Nat to be a tree of 42 cons values, using a plain Int is probably ok.

Without explicitly specifying in your code what's evaluated at compile time and what isn't you raise all sorts of developer tools-related questions. What if an expression was eagerly evaluated at compile-time, but you still want to step through it with a debugger? Do you evaluate everything eagerly or lazily? How do you control that? What if a function you have to evaluate at compile time is recursive? You could say that a compiler should be smart enough to figure that out on its own, but I haven't found a good way to make that work in practice and haven't seen a language with dependent types that does that.

5 Likes
7

Well, the question is how do the more mature dependently-typed languages deal with that issue?

A primary way to prevent non-deterministic compile times is by using universes to limit which set of types can be used for a dependent parameter. For example one universe might be "NaturalNumbers". Another common one are "propositions" (static assertions).

I would expect if Swift implements dependent types to some extent, that it would err on the conservative side and base the implementation on the learnings from Coq, Lean, Agda, etc.

3 Likes
8

In dependently-typed languages that support compile-time evaluation, like Agda, Coq, or Idris, recursive functions can be evaluated at compile-time, but they must be well-founded.

Well-founded recursion enables the compiler to guarantee the function will halt for any input, using termination checking mechanisms. The compiler ensures that recursive dependent functions are well-founded, allowing them to be safely evaluated at compile-time.

Universes are one tool used to guarantee well-foundedness. This works kind of like how the Swift compiler recognizes if an enum is self-referential and requires it to be labelled "indirect" if so. Except with universe hierarchies, the compiler prohibits a type's dependent parameter from being used with types in the same universe level as the type whose declaration it's a part of. That prevents you from defining compile-time computational that is undecidable.

In Coq, the compiler handles these details behind the scenes, but for debugging you can enable it to print which universe each type is in.

See: https://coq.inria.fr/library/Coq.Init.Wf.html

3 Likes
9

Excellent questions. Hopefully we can discuss some possible answers in this thread to what a Swift version of dependent types would entail from an lldb standpoint.

Lets also consider what the tradeoffs might be. If a new language feature "defines away entire classes of programming errors" then we get fewer bugs. What is that worth?

Evaluation Strategies in Existent Dependently-Typed Languages

In some existing dependently typed languages, evaluation of expressions can be a combination of eager and lazy, depending on the language and constructs.

Agda and Idris use a kind of lazy evaluation. Expressions are only evaluated when their values are needed. This allows for better modularity, reasoning, and code reuse. Lazy evaluation also makes it easier for the compiler to reason about infinite data structures, which can be useful in some dependently typed programs.

Meanwhile, Coq uses eager evaluation by default. It also supports user-defined evaluation strategies for controlling the evaluation order and optimizing sections of code. Since proof terms can be complex, eager evaluation can help optimize the size of terms to improve performance.

Debugging In Dependently-Typed Languages

Dependently typed languages usually have specialized tools and techniques available to help understand the evaluation of expressions and code behavior. Examples:

  • interactive assistants: Agda, Idris, and Coq provide interactive environments where you can step through evaluation to see how values are computed, and offer features to fine-tune the tactics that the compiler will employ for constructing proofs and refining programs
  • debugger commands: like lldb, dependently typed languages tend to offer debugging commands that let you inspect the evaluation of expressions, view intermediate results, trace execution, etc.
  • formal reasoning and verification: a big advantage if dependently typed languages can be the ability to formally reason about the behavior of your code and prove its correctness with proof statements, which can serve as a powerful debugging tool, allowing you to identify issues with your code & ensure it behaves expectedly

I am curious to hear more perspectives on this from those who maintain the debugging-related aspects of the Swift toolchain. The fact Swift supports interactivity and REPL seems like it would make Swift better-suited for some dependent type features than languages like C++.

1 Like
10

This could be the best written pitch in the history of Swift forums, and it's a very intriguing concept. I wonder how far it could be taken, can we imagine compile time guaranteed non-singular matrices? Unitary ones?

In your examples we can put conditions on the number of elements, and you show some pseudo syntax for that, but what are the limitations for what kinds of conditions we can place? What I mean is, do we need new compiler support for us to be able to add new kinds of restrictions?

I can't even quite wrap my head around what dependent types actually are, I mean in a sense we already have them, I can make a type Unitary4x4Matrix with a throwing initialiser. I could even let the size be a generic parameter, UnitaryMatrix<Four>. How is that really different from this, apart from some syntactic sugar? Does it make anything possible that is completely impossible know, or is it a matter of making it more ergonomic?

Also, it would be wonderful, and maybe help the argument, with more pseudo-swift examples, particularly for universes, that part was a bit abstract. Also things like pi and sigma types sounded very interesting, but abstract.

3 Likes
11

The right way to think about dependent types is not that the compiler is actually able to derive a proof "from scratch", but rather that the only mechanism to construct values of such a type is equivalent to the programmer writing down a proof which the compiler then checks, which is a simpler problem for the compiler (and a harder problem for the programmer).

So yeah, you could probably encode something like a theory of linear groups in terms of dependent types and then define a type of unitary matrices. However code that does "matrix math" with these data types will end up looking quite different than what you're used to with general matrix math libraries in ordinary programming languages.

8 Likes
12

I think these concepts are worth exploring and would help with important things like maintaining invariants. However, it would probably be very difficult to implement something like this in Swift, and there's a lot of higher-priority work going on, so I doubt these features will make it into Swift any time soon.

Additionally, adding dependent types, pi types, sigma types, inductive types, coinductive types, productivity checkers, and universes into Swift would add a lot of new things to the language and may be too complex for a language like Swift.

6 Likes
13

Thanks for the reply. This part seems very relevant, but it's really too abstract for me. Can I ask you to exemplify this, ideally with pseudo-swift? For example if we want a type NonSingular2x2 or just EvenInteger, what would the "proof" be, and how would it be different from just a throwing init or something?

14

Yes please! Constraining numerical and collection types would be a huge win. Can't wait!

4 Likes
15

Simulating this in current swift:

protocol Nat { static var size: Int { get } }

enum N1: Nat { static var size: Int { 1 } }
enum N2: Nat { static var size: Int { 2 } }
enum N3: Nat { static var size: Int { 3 } }
enum N4: Nat { static var size: Int { 4 } }

struct Matrix<Rows: Nat, Columns: Nat> {
    var elements = Array(repeating: 0.0, count: Rows.size * Columns.size)
}

func * <RA, CA, RB, CB> (lhs: Matrix<RA, CA>, rhs: Matrix<RB, CB>) -> Matrix<RA, CB>
    where CA == RB // corrected, thanks to Gustaf Kugelberg
{
    // TODO
    fatalError("TODO")
}

let a12 = Matrix<N1, N2>()
let b21 = Matrix<N2, N1>()
let c12 = Matrix<N1, N2>()
_ = a12 * b21 // âś…
_ = a12 * c12 // 🛑 Cannot convert value of type 'Matrix<N1, N2>' to expected argument type 'Matrix<N2, N1>'
16

Exactly, this kind of thing is why I don't quite understand what the essence of "dependent types" really is. Is it notation? More general generic like parameters? More general constraints?

Btw RA == CB is not needed.

17

I think Swift would benefit from at least these two (range type and fixed array type).

Beware that range checks can't always be done at compile time:

let x: Int[1...8] = 9 // compiler error: "out of bounds"
var x: Int = foo()    // happens to be 9
let x: Int[1...8] = x // compiles ok, runtime check is required

Edit: Example of range from Modula-2:

MODULE HelloWorld;
TYPE Range = [1..8];
VAR x: Range;

BEGIN
    x := 1; (* OK *)
    x := 9; (* warning: attempting to assign a value '9' to a designator 'x' which will exceed the range of *)
END HelloWorld.
1 Like
18

Beware that range checks can't always be done at compile time:

Not if it's an Int, but if your restricted Int is its own type, then it's just like an enum, so it wouldn't even be possible to construct invalid numbers.

1 Like
19

In my mind it's an ability to write functions that operate on types, evaluate at compile time, and participate in type checking as a result. AFAIU these functions are necessarily pure (no side-effects, i.e. no use of reference types, no I/O) and have restrictions on recursion. That way the compiler can guarantee that just type checking something won't mess up the file system or it won't hang due to a networking error or infinite recursion.

That way you can produce new types that "depend" on values. If your fixed-length array (let's call it a Vector) concatenation function has this type:

func ++ <Element, Length1, Length2>(
  Vector<Element, Length1>, 
  Vector<Element, Length2>
) -> Vector<Element, Length1 + Length2>

you can guarantee at compile-time that ++ always returns an array of correct length by using expressions in generic arguments of other types, like in Vector<Element, Length1 + Length2> above. Here type of a vector depends on a value of its length and + is a function evaluated at compile time during type checking:

let a1: Vector<Int, 3> = [1,2,3]
a1[3] // type error, out of bounds
let a2: Vector<Int, 3> = [4,5,6]
(a1 ++ a2)[6] // type error, OOB

This allows us to check not only OOB errors at compile time for simple one-dimensional collections, but also matrix/tensor operations, pointers etc.

3 Likes
20

I really appreciate that you try to explain this to me, but I must be honest, this still feels like it's the same as what we already have in generics. The difference to me does not seem to be qualitative, it's more a matter of making numbers a generic parameter?

I mean, if ++ wasn't concerned about length but something else, then we could already do the same thing now.

It doesn't seem fundamentally different from say a composition operator:

struct Mapping<In, Out> {
     let f: (In) -> Out
}

func •<R, S, T>(
    lhs: Mapping<S, T>,
    rhs: Mapping<R, S>
) -> Mapping<R, T> {
    Mapping { r in
        lhs.f(rhs.f(r))
    }
}

Isn't it the type that it depends on, length is part of the static type information, no?