[Pre-Pitch] Runtime Type Guarantees

Evolution Pitches
41

I think just find it a bit absurd when I try to generalize it:

var x: Positive Int8 = 127
x += 1 // runtime error on overflow
x -= 200 // compiler error: -= is unavailable for Positive integers

And then the first thing people will write after seeing a compiler error like this is:

x = x - 200 // compiler error?

The normal - operator by itself is obviously allowed because it does not have to return a Positive Int8, but whether this is useful or not depend on the broader context. I think your proposal should explore in a bit more details how those guaranties are going to propagate around and explain in which situations the garanties are lost.

42

I think the ideal situation is where both work and are functionally equivalent. For non-trivial constraints, being able to just say “does this thing conform to <bundle of constraints>” is much more convenient (and less copy-paste redundant) than having to express all the constraints explicitly. Similar to how it’s often faster and more semantically precise to ask if an object conforms to a protocol, than to check that it implements every method of that protocol (I’m being a bit lazy and pulling from Objective-C in this case).

But, there’s a lot of practical value & convenience in being able to step sideways into that. More importantly, in a strict subset of cases it’s more semantically accurate - e.g. where the prior code & context happen to assure that myVar is positive, but that it’s not intentionally a requirement / expectation that it is - you want the compiler to be free to use an optional override that’s optimised for known-positive Ints, but it’s not an error if it can’t - it’ll just fall back to a version that takes regular Ints.

It’s analogous to being able to make use of extensions with selective availability via where clauses on generic / associated types - it’d really suck if you had to always explicitly write, at the call site, that same conformance check every time you want to use the extension in question. You expect the compiler to figure it out, and only stop you if the end result is no matching method. But nobody’s stopping you from writing those possibly-redundant checks if you want; if that makes your code’s intent clearer.

43

Interesting thread! For reference, we have an implementation of refinement types that we use “in production” here: Refinement types by peter-tomaselli · Pull Request #11 · wayfair-archive/prelude · GitHub

It’s super simple and does not require compiler magic or new features if you are willing to make some concessions!

Fun to see the same questions coming up in this discussion that we grappled with when writing this. The most interesting one, which is briefly touched upon above, is the issue of composition of refinements.

On one hand, it is basically just “type level” composition of predicates, which can be modeled at the “value level” like a set. (eg. in our library we implement Both by using a Predicate type and calling through to the intersection o two of them).

On the other hand, there are numerous problems with this — for example: from Swift’s point of view, Both<CheckA, CheckB> is a “different” refinement than Both<CheckB, CheckA>, despite the fact that they represent the same checks. A more mathy person could probably explain how that is because there are algebraic properties of predicates that do not extend to Swift types… commutativity, I suppose?

Anyway, I’d strongly recommend engaging with some of the prior art on this topic — other languages and libraries (not necessarily ours, it was just a quick, modest thing) have thought this through already to incredible depth.

3 Likes
44

Maybe we should try to propose a minimal version of this feature that would be (minimally) useful and viable to implement, then hopefully it will be easier to see if there's an obvious path to take this further. The essence of this idea is to replace ad-hoc runtime checks and be able to skip those checks when the compilers knows they're redundant. Manual checks are only performed at specific points in a program (eg: usually on function entry as a precondition, before a specific operation etc.). All of the complexity I see is when we try to guarantee that a condition holds for the whole lifetime of an object/struct as long as it lives, but do we really need this? Eg:

func a(x: Positive Int) {
  print("This is a positive \(x)")
}

func b(x: Positive Int) {
  x -= 2     // <-- ??? It's negative but we don't really care. The programmer knows it won't be negative when we call a.
  x += 3
  a(x)
}

b(1)    // Do we really care that x will become negative at an intermediate point in b? As long as it's positive when it enters b and when we call a we probably don't care what happens in the middle

My proposal is to stop thinking of Positive as a type constraint and instead think of it as a type check. Inside a and b, x is just a regular Int, but before entering b we check if it's positive, then before entering a we check again. This could serve as a starting point as the minimal feature that still has the essence of this feature.

As a bonus, the compiler can detect when a struct hasn't mutated and skip the checks if they were performed upstream.

Feel free to improve on this or poke holes if I missed anything.

1 Like
45

I think there is something to this idea. The big question is: What do we do if the check doesn't hold?

46

The good thing about this is that the compiler knows at all times if x has been checked for Positive, so it's easy for the IDE to give a warning if it hasn't been checked. If the user decides not to check then it would throw a fatal error if it doesn't hold.

func foo(x: Positive Int) { // The Positive at the signature acts kind of like a throws in Java
  bar(x)  // We don't warn if bar takes a Positive because we assume we checked for it upstream before foo was called
}

let x = makeInt()
foo(x)  // Gives a warning, x is unchecked
foo(3)  // No warning
foo(-2)  // Error
if let posX = x as? Positive x {
  foo(posX)  // No warning
}

To add a further idea to this, we could introduce co-dependent checks that enable run-time dispatch which would emulate a kind of pattern matching. Eg: A signed number is either positive or negative (lets assume zero is positive for simplicity in this example), so we can create a co-dependent check (syntax off the top of my head, so feel free to just examine the idea).

typeconstraint Signed: Int {  // Acts like an exhaustive switch
  case x < 0:
    return .negative
  default:
    return .positive
}

// Lets also assume for now that the return value of Signed.positive is not checked, we take the programmer's word for it. There is probably a better way but we can leave that concern for later
func abs(x: Signed.positive Int) -> Signed.Positive Int { return x }
func abs(x: Signed.negative Int) -> Signed.Positive Int { return -x }
// Also abs function needs to be exhaustive for all cases of Signed.

abs(makeInt()) // Compile time error, int isn't checked for sign
abs(Signed(makeInt()))    // Valid
Signed(makeInt()) { x in
  abs(x)    // Also valid. Alternative syntax?
}
if let posX = x as? Signed.positive x {
  abs(posX)  // No error, also valid
}
47

Riffing on the ideas put forth by others above, how about the following?

  1. The refinement is fragile, and can be lost from the type whenever the guarantee might possibly fail (as opposed to blocking calls to things which might destroy the guarantee).

  2. Explicit refinement checks are completely optimized away when the compiler can prove that they aren't needed.

  3. To help discovery, the compiler would issue an Error when trying to pass a might-be-lost refined type referencing the line which lost the refinement. For example: "Array myVar can't guarantee NonEmpty after call to remove(at:)." and would have a fix-it adding an as? or as! check.

  4. You could annotate functions to specify that they preserve the guarantee (e.g. appending(_:))

  5. You could still specify overloads for the refined type which offer optimizations or additional signatures (e.g. non-optional first).

  6. Classes would have a special compiler-supported refinement "unique" when they are provably uniquely referenced at compile time.

  7. Reference types which are provably unique could use that knowledge to keep the guarantee in cases of possible mutation. Otherwise, they would rely on optimizing away runtime checks where possible.

Thoughts? Does this strike a good balance of simplicity and flexibility? Does it solve the issues with reference types?

1 Like
48

I just finished reading the article linked in this Figure.ink post. It's about Haskell, but the principles apply to Swift as well.

The article's called "Parse, don't validate" and in summary, the author makes a distinction between "parsing" which preserves the "knowledge gained by a function about its input data" versus "validation" which performs the same checks, e.g. !array.isEmpty, but doesn't "preserve the knowledge" in any way.

Your pitch is exactly in line with the "parse, don't validate" idea, and I'm a big fan of making this kind of thing easier in Swift.

I'd like to suggest that adding syntactic sugar in the form of an annotation as you suggest may not be the right approach here. Consider that we can already get kinda close to the desired behavior today by using @dynamicMemberLookup. Let me explain with a code sample.

let nea = NonEmptyArray(validating: [1, 2, 3])!
nea.first // uses efficient NonEmpty implenentation
nea.last // uses Array implementation via dynamicMember subscript
nea.append(4) // unsupported today, we to implement this manually

// Implementation:

@dynamicMemberLookup
struct NonEmptyArray<Element> {
    private(set) var array: [Element]

    init?(validating array: [Element]) {
        if array.isEmpty {
            return nil
        }
        self.array = array
    }

    // Allows us to forward any undefined properties to the underlying Array.
    // Only supports properties, not functions :(
    subscript<T>(dynamicMember keyPath: KeyPath<[Element], T>) -> T {
        get {
            array[keyPath: keyPath]
        }
    }

    var first: Element {
        array[0]
    }
}

You could implement this generically over Collection, but I stuck with Array for simplicity.
The really cool thing is that we can use keyPaths with dynamicMemberLookup. This makes our NonEmptyArray act just like an Array from that perspective.

Now consider if we could do the same thing with functions, e.g. implement @dynamicCallable by using keyPaths somehow! We could allow most function calls like append to pass-through to the Array implementation while shadowing functions like remove with safer, semantics-preserving implementations. Then our NonEmptyArray would behave just like an Array, but with stronger requirements, practically for free.

Side note: it's possible that "dynamicCallable with KeyPaths" isn't really the right way to implement this. Maybe giving dynamicMemberLookup the ability to refer to methods would be better. Or maybe a new annotation will be easier to implement in the compiler, e.g. @forwardCalls(to: self.array). I use dynamicCallable here just to provide a point of reference.

If this were possible, we should even be able to declare NonEmptyArray: Collection, Sequence, etc. and gain all the nice language sugar that comes with that without having to implement every single requirement — we'd get them for free with @dynamicCallable!

The only thing missing here compared to your pitch is that there wouldn't be any special syntactic sugar like NonEmpty [Int] — It would just be NonEmpty<[Int]>. Still, if sugar like this were appropriate, @propertyWrapper might be a good fit to give us that.

Also, considering where Compile-Time Constant Expressions might take us in the future, we may even be able to promote some of those run-time guarantees into compile-time guarantees.

TL;DR — If we can make @dynamicCallable support static function passthrough the way @dynamicMemberLookup does, when combined with existing compiler sugar, I think we'd be able to implement 90% to what's being pitched here without adding another new compiler sugar :smile_cat:. Either way, I would love to see these kind of wrapper types become way easier to write and hopefully way more common.

1 Like