Dealing with recursive constraints

[dabrahams]

Recursive protocol constraints cause an enormous amount of complexity in Swift. This thread is about how to deal with that. Obviously we could implement Swift's Requirement Machine, which is complex. Maybe there are lighter-weight approaches, that start by banning recursive constraints.

Is this the minimal example that demonstrates a problematic recursive constraint?

trait Collection {
  type SubSequence: Collection
}

or do we need some other constraints on SubSequence in order to have a problem, e.g.

trait Collection {
  type SubSequence: Collection where
    SubSequence.SubSequence == SubSequence, // <=== THIS
    SubSequence.Element == Self.Element,
    SubSequence.Position == Self.Position
}

…which is more like Swift's SubSequence constraints. In Swift, the SubSequence type is the result of the slicing operation on a collection.

If we want to ban recursive constraints, and the first example is a minimal problematic example, practically speaking, it means that SubSequence could not be an associated type. Well, we could make it an associated type with weaker constraints, but I lived in that world for a long time in Swift and the consequences were really ugly.

So that means slicing a C: Collection must yield some non-associated type; let's call it Slice<C>:

type Slice<Base: Collection>: Collection {
   remote var base: Base
   var startPosition: Base.Position
   var endPosition: Base.Position
   ...
}

If we just have the above declaration, here's what Swift allows that Hylo would not:

1. I can create a more-efficient custom SubSequence type for a given Collection type. For example, slicing a Range<Int> yields a Range<Int> instead of something that stores four Ints. String has a custom SubSequence with a smaller start/end index representation when the sliced String is stored inline.
2. I can ensure that we never end up creating Slice<Slice<Array<Int>>>, because slicing a Slice<T> yields Slice<T>.
3. I can nail down the requirement that any custom SubSequence type X also has the property that X.SubSequence == X.

I consider the last of these completely dispensable. My next question would be, how much of the other capabilities can we claw back for Hylo?

[dabrahams]

In the interest of completeness, I'll mention that we could get some of the capability back by creating an overloaded slicing subscript on Slice<Base> that returns Self, and teaching overload resolution that it is to be preferred over the more general slicing subscript of Collection. I personally find that highly unsatisfying from a usability point of view. Overloading in general is bad for users, increasing the number of distinct APIs that must be understood in order to grasp what is conceptually one operation. This is overloading on return type, which is even worse in many ways. I consider that solution to be worse than the problems it solves.

[dabrahams]

The “make SubSequence an associated type with weaker constraints” approach taken by pre-recursive-constraint-capable Swift was ugly primarily because then your slice was not a Collection in generic contexts, so it didn't interoperate with the rest of the library the way it should; for example, none of the Collection-requiring algorithms could work on it.

But a variation on that theme might work. “Temporary limitations” of the current Hylo compiler prevent me from type checking this except in my head, but it plays out something like the following (I could probably prove it out using Swift, if that's helpful). Contract documentation intentionally omitted so you can more easily see the type system mechanics.

/// Everything but the slicing-related requirements of Collection
trait CollectionCore {

  type Element
  type Index

  fun start_index() -> Index
  fun end_index() -> Index
  fun index(after i: Index) -> Index

  subscript(_ i: Index): Element { let }

  // A type that is wrapped to get the result of slicing
  type SliceCore
    = DefaultSliceCore<Self> // Default makes new Collections easier to define.

  // Not for user consumption; provides the implementation of slicing
  subscript slice_core(_ start: Index, _ end: Index): SliceCore { let }
}

// Adds slicing support requirements to CollectionCore.
trait Collection: CollectionCore {

  type SliceCore: CollectionCore where
    SliceCore.SliceCore == SliceCore

  // `Unsliced`: `Self == `Slice<U> ? U : Self`
  type Unsliced: CollectionCore
    where Unsliced.SliceCore == SliceCore,
          Unsliced.Element == SliceCore.Element,
          Unsliced.Index == SliceCore.Index

}

// Provide the user-consumed slicing operation.
extension Collection {

  typealias Unsliced = Self

  subscript(_ start: Index, _ end: Index): Slice<Unsliced> {
    yield Slice(core: self.sliceCore[start, end])
  }

}

// Wraps Unsliced_'s SliceCore as a full Collection.
type Slice<
  Unsliced_: CollectionCore
  where Unsliced_.SliceCore: CollectionCore,
        Unsliced_.SliceCore.SliceCore == Unsliced_.SliceCore,
        Unsliced_.SliceCore.Index == Unsliced_.Index,
        Unsliced_.SliceCore.Element == Unsliced_.Element
>: Collection
{

  memberwise init

  var core: SliceCore

  typealias Unsliced = Unsliced_

  // Prevents buildup of Slice<...> nesting.
  typealias SliceCore = Unsliced.SliceCore

  // Forward CollectionCore requirements to core
  typealias Element = SliceCore.Element
  typealias Index = SliceCore.Index
  fun start_index() -> Index { core.start_index() }
  fun end_index() -> Index { core.end_index() }
  fun index(after i: Index) -> Index {  core.index(after: i) }
  subscript(_ i: Index): Element { _read { yield core[i] } }

  subscript slice_core(_ start: Index, _ end: Index): SliceCore {
    yield core.slice_core[start, end]
  }

}

conformance Slice: Equatable where Unsliced.SliceCore: Equatable {}

//
// Conveniences so new Collections don't need to define their own slicing support.
//

extension Collection where SliceCore == DefaultSliceCore<Self> {

  subscript slice_core(_ start: Index, _ end: Index): SliceCore {
    yield DefaultSliceCore(base: self, start: start, end: end)
  }

}

type DefaultSliceCore<Base: CollectionCore>: CollectionCore  {

  let base: remote let Base
  var start: Index
  var end: Index

  typealias Element = Base.Element
  typealias Index = Base.Index

  fun start_index() -> Index { start }
  fun end_index() -> Index { end }
  fun index(after i: Index) -> Index { base.index(after: i) }

  subscript(_ i: Index): Element { yield base[i] }

  subscript slice_core(_ start: Index, _ end: Index): Self {
    yield Self(base: self.base, start: start, end: end)
  }

}

conformance DefaultSliceCore: Equatable where Base: Equatable, Index: Equatable {}

// ========= Demonstrations ============

// A simple collection using default slicing
type Basic: Collection, Equatable {

  typealias Element = String
  typealias Index = Int

  fun start_index() -> Index { 0 }
  fun end_index() -> Index { 10 }
  fun index(after i: Index) -> Index { i + 1 }

  subscript(_ i: Index): Element { yield String(i) }

}

 fun test_basic() {
  let basic = Basic()

  precondition(
    basic[3, 5] ==
      Slice<Basic>(
        core: DefaultSliceCore(base: basic, start: 3, end: 5)))

  precondition(basic[3, 5][3, 5] == basic[3, 5])
}

// A collection with a custom slice representation.
type CustomSliced: Collection, Equatable {

  typealias Element = UInt8
  typealias Index = Int

  fun start_index() -> Index { 0 }
  fun end_index() -> Index { 10 }
  fun index(after i: Index) -> Index { i + 1 }

  subscript(_ i: Index): Element { yield UInt8(i) }
  subscript slice_core(_ start: Index, _ end: Index): SliceCore {
    yield SliceCore(start: start, end: end)
  }

  type SliceCore: Collection, Equatable {

    typealias SliceCore = Self
    typealias Element = UInt8
    typealias Index = Int

    var start: Int
    var end: Int

    fun start_index() -> Index { start }
    fun end_index() -> Index { end }
    fun index(after i: Index) -> Index { i + 1 }

    subscript(_ i: Index): Element { yield UInt8(i) }

    subscript slice_core(_ start: Index, _ end: Index): SliceCore {
      yield Self(start: start, end: end)
    }
  }

}

fun test_custom() {
  let custom = CustomSliced()

  precondition(
    custom[3, 5] ==
      Slice<CustomSliced>(core: CustomSliced.SliceCore(start: 3, end: 5)))

  precondition(custom[3, 5][3, 5] == custom[3, 5])
}

fun main() {
  test_basic()
  test_custom()
}

[dabrahams]

OK, translating to Swift and running it through the compiler found lots of silly errors, but didn't change the basic shape of things. The result is here in two files, the second being a refined version of the first. I've translated the second refinement into Hylo above.

[dabrahams]

If the above technique works, we'll want to think about how to hide from the user the kludgey parts that are only there for the sake of the technique, such as CollectionCore. I have some ideas.

[dabrahams]

@slavapestov points out this Swift example, which illustrates another source of undecidability that doesn't involve recursive constraints. That strongly suggests to me that undecidability is inevitable, and the best we can do is to put computational limits on typechecking. He also points out that the requirements machine can be implemented in a few hundred lines of code so maybe we should just bite the bullet.

protocol MyIterator {
  associatedtype Element
}

protocol MySequence {
  associatedtype Iterator: MyIterator
}

struct ConcreteIterator<Elements: MySequence>: MyIterator {
  typealias Element = Elements.Iterator.Element
}

The definition of ConcreteIterator creates an implicit inequality constraint, “where Elements.Iterator != Self” because clearly Elements.Iterator == Self makes ConcreteIterator.Element a circular definition. However, detecting all such inequality constraints is equivalent to solving the halting problem.

[kyouko-taiga]

How is that different from this:

func f<T: Equatable, U>(x: T, y: U) -> Bool { x == y }

Clearly it doesn't type check because there is nothing in the signature that says T.infix== is defined for an argument of type U. The important property that separate checking upholds is precisely that it can reject this function. Template specialization can't.

It may be worth making sure we agree on some ground principles, so let me try to define them.

Inside of f, T and U are bound existentially and therefore only described by their constraints. So we take these constraints for granted and operate under a closed-world assumption. When we call f, we see universally quantified variables so we're free to pick anything as long as we can prove that our choices satisfy f's signature.

There is no way to skip this proof, even without equality constraints. If we write this:

func g<T: Equatable>(x: T, y: T) -> Bool { x == y }

We sill have to prove that whatever we substitute for T is indeed equatable when we call g. So at call site we must first substitute generic parameters and then check that all constraints on them are satisfied. That is fine because the existentially quantified version was rich enough to be checked separately.

Now let's discuss about the constraints.

For separate checking of generics to be complete, a generic component must describe, in the <...> and the where clause, all constraints that its parameters must satisfy in order for a concretization of that component to pass typechecking.

This definition is too strong to support anything other than conformance constraints, and only in a language where T: P can never rule out T: Q. As I mentioned, <T: Collection where T.Element == Int> is underspecified under this definition because it doesn't tell about all the types that T cannot be. There is an unbounded number of such types so we can't even write a complete signature.

And if we're ready to say that T == Int implies that T != Bool, then I don't say why we can't also say that the generic signature of ConcreteIterator implies Elements.Iterator != Self. I don't think making such an inference is undecidable and I'm pretty sure Slava didn't say it was.

Now even if I'm wrong and making these inferences is indeed undecidable, then the cure is just to run type checking under a time budget. I never understood why type checking had to be decidable and I thought we agreed to give up on this idea a long time ago.

Here's an example using HKTs [...]

IteratorSupplier is not really higher-kinded but that is not the point of your example. Basically you're trying to hide the implicit constraints on MakeIterator that are caused by the definition of ConcreteSequence. There's a simpler way to do that:

func h<T>(_ x: T) {
  struct S<U: Collection> where U.Element: Equatable, U.Element == T {}
}

Here, <T> is underspecified because it doesn't say that T must be equatable.

Note: This function is rejected in Swift because we can't declare a generic type in a generic function but we can replace S by a generic function with the same signature, in which case it may be a source of unsoundness worth invistigating.

This problem is slightly orthogonal IMO. At the very least there are many more considerations to take into account when it comes to declarations nested in generics so I think that would deserve a separate design discussion cycle.

[dabrahams]

You never answered this question, which may in fact play a 🔑 role in understanding:

Which parts do you consider declaration and which do you consider implementation?

How is that different from…?

Clearly it doesn't type check because there is nothing in the signature that says T.infix== is defined for an argument of type U.

In the same way there's nothing in the signature of ConcreteIterator that says Elements.Iterator != ConcreteIterator<Elements>, and yet that condition produces a type error in the body 🔑 of ConcreteIterator. You haven't said anything that explains why these cases should be viewed as different.

The important property that separate checking upholds is precisely that it can reject this function. Template specialization can't.

I don't know why you're bringing up template specialization; that's not how I've been thinking of this. Furthermore, to the extent that what I'm talking about is anything like what happens with templates, it's like specializing the template with maximally-uncooperative archetypes, and that technique certainly does reject f in my example. But please, let's not bring templates into this. The ground principles you outline are all part of my background assumption, except possibly for this, which I don't understand:

we must first substitute generic parameters and then check that all constraints on them are satisfied

What specifically do you mean by "substitute generic prarameters" (e.g. substitute them for what?) and why would it be important to do that before checking that the generic arguments satisfy constraints on the corresponding generic parameters? (speculating: maybe this “substitution” is just the way you're talking about identifying what the generic arguments are?). And why are you putting so much emphasis on this ordering?

For separate checking of generics to be complete, a generic component must describe, in the <...> and the where clause, all constraints that its parameters must satisfy in order for a concretization of that component to pass typechecking.

This definition is too strong to support anything other than conformance constraints, and only in a language where T: P can never rule out T: Q.

I don't understand what it could mean for my definition of “complete checking” to “support” a language feature; the only way I can figure out to read the first part of your sentence (which may be a misinterpretation) is "that kind of completeness can't be provided by any language with non-conformance (e.g. type equality) constraints.” But that's clearly false. And I can't even guess at an interpretation for the second part of your sentence, I'm afraid.

As I mentioned, <T: Collection where T.Element == Int> is underspecified…

I didn't address this before so let me go back to the original statement:

If we had to ensure that the equality constraints of generic signature can never be contradicted by a given set of arguments, then we'd have to say that <T: Collection where T.Element == Int> is underspecified because we must also add T != Array<Bool>, T != Deque<Bool>, T != LinkedList<Bool>, ....

I don't understand what the premise “if we had to ensure that the equality constraints of generic signature can never be contradicted by a given set of arguments” even means, but it doesn't sound like anything I'm talking about. <T: Collection where T.Element == Int> already rules out T being a collection whose Element is Bool. This example is also very unlike ConcreteIterator because I'm saying the body 🔑 of ConcreteIterator implies constraints on its parameters that are unstated. There is no body in what you're describing.

if we're ready to say that T == Int implies that T != Bool, then I don't say why we can't also say that the generic signature of ConcreteIterator implies Elements.Iterator != Self.

Why we can't also say that is very simple: I can change the body of ConcreteIterator (which is not part of its generic signature) in such a way that you would never suggest such an implication exists

struct ConcreteIterator<Elements: MySequence>: MyIterator {
  typealias Element = Int // <==
}

Poof! Same generic signature 🔑, no constraint on the relationship between Elements.Iterator and Self.

I don't think making such an inference is undecidable and I'm pretty sure Slava didn't say it was.

Nor did I say that. My understanding of all the undecidability we've seen is that it is something that can occur given a certain level of expressivity. The simplest known example that actually demonstrates it for the problem @slavapestov originally pointed out (years ago now) is much more convoluted than what we've been looking at. What I believe Slava said is that there exists a Swift program where the existence-or-not of what I'm calling an implied inequality constraint is undecidable. Nobody has produced an example, but I believe Slava arrived at his conclusion by mapping the problem of determining the existence of such a constraint onto the problem of detecting infinite recursion (i.e. non-termination) in a functional program that you could derive mechanically from the declarations in the problematic Swift program.

you're trying to hide the implicit constraints on MakeIterator that are caused by the definition of ConcreteSequence

Are you sure? 🤷 That doesn't sound like anything I was trying to do. I was trying to demonstrate that those implicit inequality constraints exist and need to be expressed (e.g. on shouldNotTypeCheck), and can't be inferred by the compiler from declarations even if it is willing to look into the bodies of generic types to find them. Even if you think the body of a generic type is part of its generic signature 🔑 , I'm pretty sure you don't think the body of a generic function is part of its signature; I think we agree that the compiler should not look into the body of a (generic) function in order to determine that a call to that function type-checks.

Your "simpler way" doesn't demonstrate the same thing I was trying to show because there's no implied inequality constraint.

[kyouko-taiga]

You never answered this question, which may in fact play a 🔑 role in understanding:

Which parts do you consider declaration and which do you consider implementation?

A type isn't like a function in that it has public parts in its body. In particular, the parts that make it conform to a trait must be visible to every consumer of that conformance. A function exports nothing more than it's signature.

I think it is the point where asynchronous messages on the Internet have reached the maximum they can do for us. I carefully read everything you wrote and would prefer to continue online.

[dabrahams]

I'm ready to have an interactive discussion whenever you are. But FWIW, I put a lot of labor into the post above. I asked very specific questions where I could in order to try to understand what you're saying (and you still haven't even answered the first one, although you seem to be sort of hinting at an answer). Where I couldn't come up with specific questions I tried hard to explain why I couldn't understand you and to point out mistaken assumptions you seemed to be making about what I've said. It's going to be pretty unsatisfying for me if we don't address all of those points in whatever discussion comes next. And I think it's important that we ultimately tie up all the loose ends here so that the written record can act as a guide for others, and for our future selves.

[kyouko-taiga]

I'm hoping we can get to the very bottom of everything and it'll be very valuable to come back here with our conclusions. I just feel like continuing the discussion in this form at this point is a time sink for both of us with endless opportunities to get misunderstood.

[dabrahams]

FWIW, this is what I get when I do as you suggested and replace S by a generic function with the same signature

func h<T>(_ x: T) {
  func s<U: Collection>(_: U.Type) where U.Element: Equatable, U.Element == T {}
}

The compiler accepts it, which seems perfectly fine to me. If you add the call s([x]) you get an error, as you should because T is not Equatable; in fact there are no types you can call s with. This program (or your original version) should only be rejected if you believe declaring a generic whose constraints can't be satisfied must be diagnosed by the compiler. To me such a diagnosis seems like a nice-to-have, but non-critical, feature. I certainly can't see any hint of unsoundness in its absence.