Bounds and Constraints

[zrho]

Bounds and Constraints

hugr-core allows to attach a bound to runtime types, which is either
Copyable or Any. As the name suggests, values of types that are marked
Copyable can be copied by connecting multiple input ports to the same output
port that produces a value of that type. The Copyable bound also includes the
ability to delete the value by not connecting the output port. Types that are
marked Any must be treated linearly. Throughout hugr-core a bound is
attached to every type, presumably as a cache.

hugr-core also adds a subtyping relation to this system: The type of copyable
types is a subtype of the type of any types. Moreover, custom runtime types[^1]
declare the way in which they compute their bound from the bounds of their
parameters:

• Either the bound is explicitly fixed, or
• the bound is computed as the least upper bound of the bounds of a specified subset of the parameters.

I propose replacing the bounds system with constraints.

Extensibility and Composability

Custom operations may have non-trivial rules that determine their typing. This
includes variadic ports, constructions similar to those of tail-loops and
conditionals, or more sophisticated (local) validation rules. A constraint
system allows to express these rules in an extensible and composable way.

Extensibility is achieved by allowing declaration of custom constraints. These
custom constraints can be supplemented with code that the validator executes in
order to check the constraint and to propagate type information when performing
type inference. This is similar to the current system, where custom operations
can come with validation code.

The difference between a constraint system with pluggable solvers and the
current implementation is composability. Constraints and their solvers can
be defined once and then reused in many different contexts and combinations.
A small suite of standard constraints will likely cover many use cases already,
reducing the need for custom constraints and therefore custom validation code,
while increasing the expressiveness of a declarative extension system.

Example: Variadics

An example of this is variadic operations. At some point previously, the binary
logic operations were variadic, which required the operations not to have a
declarative type but instead come with a custom function that computes the type
given the ports. This code would be required for every operation that needed to
be variadic. Moreover, the type of the operations would be entirely opaque until
the custom code was run. This would be very dissatisfying for declarative
extensions. The logic operations have been made binary.

The logic behind variadic types can be expressed naturally as a constraint:
For a runtime type x and a list of runtime types xs, the constraint
(variadic x xs) holds whenever all elements of xs are x. For instance,
the following constraints all hold:

• (variadic int [])
• (variadic int [int])
• (variadic int [int int])
• (variadic int [int int int])

Then a variadic logic operation can use the variadic constraint on the list of
its input types to ensure that all inputs are booleans. A variadic int operation
can use the variadic constraint to ensure all inputs are ints. The logic
behind the variadic constraint is written once and can be reused in many
different contexts, establishing a standard vocabulary. When defined via
declarative extensions, the fact that an operation is variadic is immediately
visible in the type signature:

(declare-op logic.and
  (forall ?xs (list type))
  (where (variadic bool ?xs)
  (op xs [bool])))

(declare-op int.add
  (forall ?xs (list type))
  (where (variadic int ?xs)
  (op xs [int])))

Example: List Concatenation

Another example of a constraint that goes a long way is list concatenation.
Through supporting multiple variables in one row, hugr-core rows have a
builtin capability for concatenation; however that makes unification and pattern
matching over hugr-core rows be ambiguous. When lists are restricted to a
single variable which has to be at the end of the list, this ambiguity is
solved, but the ability to concatenate is lost at first. A concatenation
constraint restores the ability to concatenate lists, while keeping
ambiguity-free unification and pattern matching. All ambiguity is pushed
into the constraint system, which is meant to handle it [^2].

With the concatenation constraint, we can express the the type of a tail-loop
operation fully declaratively:

(declare-op core.tail-loop
  (forall ?just-inputs (list type))
  (forall ?just-outputs (list type))
  (forall ?rest (list type))
  (forall ?inputs (list type))
  (forall ?outputs (list type))
  (forall ?targets (list type))
  (where (concat ?just-inputs ?rest ?inputs))
  (where (concat ?just-outputs ?rest ?outputs))
  (op
    ?inputs
    ?outputs
    [(dfg ?inputs [(adt [?just-inputs ?just-outputs]) . ?rest])]))

Example: Bounded Naturals

hugr-core's type for static naturals can come with an upper bound. Given a
constraint (nat-lte? ?n ?m) which holds when a natural ?n is less than or
equal to a natural ?m, we can define a bounded natural type with its values
declaratively:

(declare-term core.bounded-nat-type
  (param ?bound nat)
  static)

(declare-term core.bounded-nat
  (forall ?bound nat)
  (param ?value nat)
  (where (nat-lte? ?value ?bound))
  (core.bounded-nat-type ?bound))

Migration

Migration between hugr-core and a constraint based system is admittedly tricky, which is why it wasn't
included in #1542. The current state of the discrepancy is as follows:

• Bounded types: we import every type as copyable and lose the bound when exporting.
• Bounded naturals: we import every bounded natural as unbounded and lose the bound when exporting.
• Row variables: we only support one variable per list, at the end of the list.
• Extension sets: we only support one variable per extension set.

For bounded types and bounded naturals, a possible migration path is to remove the bounds from hugr-core
at first. This would admit more programs than before, but it would not reject any programs that were
previously accepted. We can then add the bounds back in as constraints.

For rows and extension sets, I am not quite sure how much we rely on having multiple variables.
If it turns out that that feature is pretty much unused, we could remove it from hugr-core
and make extension sets and rows take a single variable. We could then later add in the concatenation
constraint, so in the long run we do not lose any expressiveness.

Existentials

There is a trick which would allow us to perform a gradual migration without changing hugr-core initially.
I don't think I like it that much since it would make the typesystem quite a bit more complex,
but it's worth mentioning. We could use the alias system to define existential types:

(define-alias compat.copyable-type
  (forall ?t type)
  (where (core.copy ?t))
  (where (core.delete ?t))
  ?t)

[^1] hugr-core does not currently allow custom static types.
[^2] If we keep concatenation as part of the term language, unification has to become a constraint itself.

[zrho]

This is about the tension between type bounds and constraints. Type bounds as
they are in hugr-core use subtyping. Subtyping is a deceptively subtle
feature. I've looked at automatic translations between subtyping and constraints
and found that it is quite hard.

Say we have a function with type (x : CopyableType) -> T for some type T.
This can be translated into a version without subtyping but with constraints
easily as (x : Type) -> T where Copy(x). However, things become more complicated
when the copyable type is nested within another type. Consider for example a function
with type (x : List(CopyableType)) -> T. Here the parameter x can be any list
of types that all need to be copyable but otherwise may be entirely different types.

Incomplete Translations

Note that for full generality, it is not sufficient to simply introduce a
CopyList constraint. While that would solve this particular case, it would not
be able to handle, say,
(x : List(Tuple(CopyableType, Nat))) -> T.
We could argue that in practice only a few such cases occur, which might be good
enough for migration until we find a better solution.

Keep the Subtyping

One option is to keep the type bounds system from hugr-core and make it a
thing in hugr-model. This is certainly the most expedient solution but comes
with the cost of then having to deal with subtyping.

In case we do go this route, we should make sure that the rest of the design is
coherent with subtyping in mind. Do we want to allow subtyping in other places?
Should we have variance annotations? Should we be able to extend the subtyping
relation for custom types, and if so, to what extent? Do we have principal types
or do we allow a term to have multiple incompatible types? How does subtyping
interact with references and effects (a potential source of unsoundness).
We could elect to ignore all of that for now, but that would come at the risk of
engineering ourselves into a corner even further.

Existential Types

The most direct way to translate the type from using subtyping to constraints is to use
existential types, in which case the signature would become
(x : List(∃(a : Type) where Copy(a). a) -> T.
However, existential types are a very heavy feature, just like subtyping itself.

Higher-Order Constraints

The term language and therefore also the language of constraints in hugr-model
is first-order. We could extend the language to terms with binders. We could
then rewrite the type
(x : List(CopyableType)) -> T as
(x : List(Type)) where EveryItem (λ(a: Type). Copy(a)) -> T.

Higher-order constraints would allow us to address the migration problem for bounded types,
but would also make it possible to express other common patterns declaratively with constraints.
For example, a constraint
ZipWith: (List(a), List(b), (a, b) -> Constraint) -> Constraint
can come in very handy for numerous operations.

Local Recursive Constraints

Say we have a list of types xs : List(Type) and we want to ensure that all types in
the list are copyable. Since lists are a recursive algebraic data type, we can express
this via recursion: if xs is empty, then all of its items are copyable. If xs
is not empty, then the first item must be copyable and the rest of the list must
consist of copyable types. This can be expressed as a recursive constraint as follows:

CopyList: List(Type) -> Constraint
CopyList(EmptyList).
CopyList(ConsList(x, xs)) :- Copy(x), CopyList(xs).

To allow for translation of copy bounds that are arbitrarily nested within types,
we could introduce such constraints locally in the type scheme. The type
(x : List(Tuple(CopyableType, Nat))) -> T from above would then come with
a set of constraints

C0: List(Tuple(Type, Nat)) -> Constraint
C0(EmptyList).
C0(ConsList(x, xs)) :- C1(x), C0(xs).

C1: Tuple(Type, Nat) -> Constraint.
C1(Tuple(x, _)) :- Copy(x).

Like higher-order constraints, this feature allows us to express a wide range
of common patterns.

Remove type bounds (and bounded nats) for now

A different option would be to remove type bounds from the core for now until we have figured out an ergonomic and coherent way to add something like them back in.

Different ideas?

I'd love to hear if there is any different ideas on how to address this since none seem like the obviously correct one.

[acl-cqc]

Ok, some thoughts

• Do we have any use-cases for constraints besides the linear/copyable type bounds? The latter seems sufficiently fundamental to Hugr (and distinct from any ideas in A system of "Interfaces" #842 "does this type support these operations) that I don't see we necessarily need to generalize. A special system for dealing with copyable/linear and nothing else seems quite justifiable and reasonable.
  • There was an idea for having custom constraints instead of binary compute_signature, allowing to know some parts of what a (missing) binary function might do. This might be a nice to have - but it's not clear that it's urgent - and I'm not at all sure how the API for this would work if I consider, say, two custom constraints acting on the same variable (where neither constraint knows about the other)....
  • So I am not yet convinced about the need for constraints.
• In general, subtyping is nasty, yes - your complex constraint-defining systems and/or existential types are no worse than subtyping. (I tend to think of existentials as the closest translation, and you are quite right that although existentials seem "very heavy", subtyping is equally heavy.) But that could well be an argument to limit subtyping as much as possible, i.e. we do not need a general notion thereof.
  • Whether we even need BoundedNat, I'm open to debate, but I think we need Copyable/AnyType unless we have a thorough rebuttal of all use-cases.
• Is this about principal types? I appreciate that as Hugr stands, [Int] could be a List[AnyType] or a List[CopyableType]. Whereas with constraints, it is only a List[Type] - that happens to satisfy the local/recursive CopyList constraint. Does that get us any notion of principality? (Local/recursive, or higher-order, definitions of constraint, seem unlikely to have the property of there being a principal constraint definition (?). Indeed, these start to look like they are verging on dependent types in terms of what you'd need to compare equivalence of different definitions of "the same" constraint - more and more, I'm thinking, we need specific techniques for dealing with CopyableType/AnyType not general mechanisms here)

If you are arguing that we need to be flexible and able to incorporate future advances in type theory into our IR, I would note that we have way more type-safety in our IR than most and adding type-system features to programming languages seems to proceed more rapidly than adding them to IRs (but still slowly!) - I would say that for IRs one tends to use a wide variety of conservative static analyses that often do not look/feel like type systems.

• "Way more type safety" might get restrictive, as we require equality in types at both ends of a wire - hence to provide subtyping on extended types, you need to "drop" custom/extensible type information. (A strictly bigger constraint set implies a smaller one.) I think we do that via explicit type-system-extension-provided coercions.
• An interesting (counter)example might be, say we wanted to add polyhedral-analysis info to our types (big tensors of qubits), how would we do that - would that be something we could do via constraints, would we use metadata, etc.? I think one might well add metadata with a separate tool rather than try to build the Hugr typesystem to be flexible enough that it could be extended in that way.

[zrho]

A special system for dealing with copyable/linear and nothing else seems quite justifiable and reasonable.

We definitely need a way to deal with copyability and I wouldn't have an issue at all with it being afforded special status. My issue is with the subtyping: as soon as we introduce any subtyping at all, even if just for copyability, the snakes are released and we have to make sure that it is coherent with the rest of the system. That is a very steep price to pay for this feature.

If you are arguing that we need to be flexible and able to incorporate future advances in type theory into our IR, I would note that we have way more type-safety in our IR than most and adding type-system features to programming languages seems to proceed more rapidly than adding them to IRs

In some sense I'm trying to argue for the opposite: I hope that we can make the type system extremely simple. In particular, I'd like us to avoid subtyping, rank-n types, existential types, implicit generalisation, pi types etc. In my mind, ideally types should be simple trees which can be compared for equality and unified in the obvious way as trees. And ideally these trees should have a principal type.

Then there are type schemes: when we define a function, operation, constructor etc. we specify parameters, which can depend on each other, and can be subjected to constraints. That appears very complicated at first, but turns out to be surprisingly simple: whenever you use one of these things, the type scheme becomes instantiated and so simply acts as a template for types in the simple type language.

Constraints then serve two purposes: one purpose is to act as a tag, e.g. tagging a runtime type as copyable. The other purpose is to act as an escape hatch for the type system where we need a bit more than just equality on trees. This escape hatch has a well-defined API boundary with the rest of the type system: a constraint solver can look at types, postulate new equalities between types and check if there are other constraints that mention types (e.g. requiring some types to be copyable).

I don't see this as a system for future extensibility of the type system with arbitrarily exotic features, but rather as an API to organise validation code for custom operations in a way that composes nicely. With metadata expressed as terms (and therefore just labelled trees), metadata can be incorporated into this process easily as well.

When we have all of the types available, the constraint solvers can simply check for type equalities, which can be trivially parallelised. When we do not have all of the types available and want to do inference, the solvers can interact through unification of the types and therefore collaborate without even being aware of each other (I know that if we want to do inference is controversial, my point is simply that there is a very nice story for how to do it in this system). The type system would have a very simple declarative formulation in terms of constraint handling rules.

If this is all so simple, then why all of the complicated stuff in my comment above? That stuff is to address the issue of translating the subtyping of types and copyable types, arbitrarily nested. I strongly suspect that in practice there are only a handful of patterns in which this subtyping is actually used. If there is any, I would like to see an example that isn't covered by just Copyable and CopyableList.

[zrho]

Looking at guppy, there are only three places where a hugr PolyFuncType is created:

• The signature of the partial operation, which does not involve any types that must be copyable.
• The signature of the unsupported operation, which does not involve any types that must be copyable.
• guppylang.tys.ty.FunctionType.to_hugr_poly.

guppylang.tys.ty.FunctionType.to_hugr_poly takes a list of guppylang.tys.param.Parameters and makes them into parameters of the PolyFuncType. This can either be a guppylang.tys.param.TypeParam or a gupplylang.tys.param.ConstParam. The first is translated to hugr either as a type with the All bound or the Copyable bound, depending on whether the type can be linear. The latter is either a natural (without bound) or an extension type which is translated to a string.

Therefore all hugr PolyFuncTypes that can be generated by guppy are expressible with a simple Copyable constraint on a type parameter. In particular none of the complicated features listed above are required to express the subset of hugr that can be generated by any arbitrary guppy program.

Are there any planned guppy features that would require more complicated (esp. nested) usages of bounds?

[acl-cqc]

(Note: this relates to #1606)

[acl-cqc]

In some sense I'm trying to argue for the opposite: I hope that we can make the type system extremely simple. In particular, I'd like us to avoid subtyping, rank-n types, existential types, implicit generalisation, pi types etc. In my mind, ideally types should be simple trees which can be compared for equality and unified in the obvious way as trees. And ideally these trees should have a principal type.

Sounds good, but my question is whether we are just moving that complexity elsewhere, i.e. into the constraint system. There may be an argument that that is worth doing (even if that is all we achieve), specifically the argument of modularity.

That stuff is to address the issue of translating the subtyping of types and copyable types, arbitrarily nested. I strongly suspect that in practice there are only a handful of patterns in which this subtyping is actually used. If there is any, I would like to see an example that isn't covered by just Copyable and CopyableList.

Looking for such examples is totally worth doing. I am not wedded to the idea that we need to support Copyable outside single types and lists. Or....hmmm....actually maybe I am: one of our canonical/design examples was the headers of a statically-sized tensor, which would be List(Tuple(Type, Nat)), but you'd almost certainly want the headers to be copyable (even if the contents are not), so Type, List(Tuple(CopyableType, Nat)).

Maybe there is some other way of dealing with those, though...?

It's the putting a CopyableType in where a Type is expected that causes the problem, right? Can we use an explicit widening so you'd have to have [CopyableToAny(Int)] to get a List(Type) whereas [Int] would be a List(CopyableType) only? I guess that when you want to pass a List(CopyableType) in where a List(Type) is expected you then need ListOfCopyableToListOfAny (aka map CopyableToAny) but can we just stop there (draw a line saying we are invariant beyond the two simplest cases)? Arbitrary I know but would that help and is it good enough?

[zrho]

For this example, there is an elegant solution using custom types: instead of List(Tuple(Type, Nat)) you would take a List(Header) where Header has a constructor header : (t : Type, dim: Nat) where Copyable(t) -> Header.

But even without that, the point isn't that Copyable and CopyableList would be sufficient for everything. There will likely be corner cases where they are not, but that is fine, since the constraint system is extensible. The question is rather whether we can do without a mechanical translation from arbitrarily nested subtyping to constraints. And looking at guppy and hugr-core it appears that we can. This would then be a significant reduction of complexity if it allows us to get rid of all subtyping.

What would the type be of the operation that creates a statically sized tensor given some runtime values? That would likely involve some custom logic; I do not see it being expressible in plain types currently, regardless of subtyping or not. At the moment, this custom logic would be attached to the operation implementation, so we already need and already have mechanisms for near arbitrary extensibility of the type system. Now the idea would be to move all of that into constraints.

Moving the custom logic from custom operations to custom constraints at first is only moving complexity. It starts to make sense once it allows us to subsume multiple features into the constraint system at the same time: type copyability bounds, custom operation signatures, bounded naturals, etc. We could then start to notice that quite a few custom operation signatures appear to use the same kind of logic again and again, so we can factor out that logic into just one constraint to be shared among them. This does not need to cover all the cases; an operation can still come with some custom constraint just for that operation. But I suspect that there will be some common patterns.

[acl-cqc]

So if the long-term answer is to move to a constraint system, that might be fair - note long-term. Personally I'd want to see both

• a lot of examples/use-cases/translations of the current way of doing things into the constraint system (demonstrating the improvement, preferably on real-world/existing examples, which I admit means there'll be more of a migration when it happens);
• a lot of details, in particular, trying to make any constraint system as simple as it could possibly be, because at the moment it feels like a lot of complexity (e.g. you are including ideas of custom types, functions, higher-order/recursive constraints, possibly existentials)...

Now, when you say, we already have a lot of complexity because we have subtyping, I think that's less of an argument for a constraint system, and more of an argument for reducing complexity / having less subtyping. (See #1606 about reducing complexity, too.) My proposal would be something like - we have explicit coercions TreatLinearly :: CopyableType -> AnyType and TreatAllElementsLinearly :: List[CopyableType] -> List[AnyType]. Then we declare AnyType and CopyableType disjoint (maybe rename AnyType to LinearType I guess). And lo, there is no subtyping anymore, everything has a principal type, right? (Ok, we also need to establish something similar for bounded nats.) Anything beyond List[Type] we say has no coercion/conversion right now, we monitor demand, probably do nothing, maybe add one or two, if demand really becomes significant (which I think very unlikely) then that's another argument to (either add a more general mechanism or) move to constraints. How's that?

[acl-cqc]

That said, I'm not entirely sure how much complexity there is in having subtyping. Theoretical complexity maybe, but does that impact non-(type-)theorists i.e. users? Indeed it means we cannot have a function from term to (principal) type, and must instead have a function from term/thing and candidate type to bool, but I haven't really followed the other practical ramifications i.e. how much harder it seems to be making the task of compiling current Hugr types to hugr-model.

[zrho]

a lot of details, in particular, trying to make any constraint system as simple as it could possibly be, because at the moment it feels like a lot of complexity (e.g. you are including ideas of custom types, functions, higher-order/recursive constraints, possibly existentials)...

I only mentioned the higher-order/recursive constraints and existentials because that'd be necessary to automatically convert a subtyping based version to a constraint based version. I don't really want any of that stuff. Without the requirement of automatic conversion and the realisation that we currently do not actually use any of the cases where it becomes complicated, the constraint system would be very simple. We could then, as you say, monitor demand and probably do nothing.

Now, when you say, we already have a lot of complexity because we have subtyping, I think that's less of an argument for a constraint system, and more of an argument for reducing complexity / having less subtyping.

Ideally no subtyping, yes. I thought about having a separate LinearType and Type initially (LinearType perhaps named Resource?); it would be a more substantial breaking change than using a Copy constraint and since I wanted to maintain a light touch, I didn't pursue it further. This would also have some repercussions for the type system which I don't know how to resolve.
For instance: What are the arguments of a function type? Currently they have types List(Type), List(Type) and ExtensionSet. If we separate linear and non-linear runtime types, this would be much more complicated to accomodate for functions that have any mixture of both linear and non-linear inputs and outputs. Similar questions would arise for the type of ports, etc. So overall I believe that the constraint solution is still much simpler.

That said, I'm not entirely sure how much complexity there is in having subtyping. Theoretical complexity maybe, but does that impact non-(type-)theorists i.e. users?

It impacts users because it impacts us developers since we have to either deal with the complexity, which takes time and thought, or ignore the complexity, which leads to bugs, corner cases and inconsistencies. One of the reasons I care about this is that when we want hugr-model to become a reasonably stable format, we should be relatively sure that it covers all the bases. A simple and theoretically coherent system increases the likelihood that we don't get into a corner that is hard to get out of later.

[acl-cqc]

I only mentioned the higher-order/recursive constraints and existentials because that'd be necessary to automatically convert a subtyping based version to a constraint based version. I don't really want any of that stuff.

Ok :-)

I wrote:

My proposal would be something like - we have explicit coercions TreatLinearly :: CopyableType -> AnyType and TreatAllElementsLinearly :: List[CopyableType] -> List[AnyType]. Then we declare AnyType and CopyableType disjoint (maybe rename AnyType to LinearType I guess). And lo, there is no subtyping anymore, everything has a principal type, right? (Ok, we also need to establish something similar for bounded nats.) Anything beyond List[Type] we say has no coercion/conversion right now, we monitor demand, probably do nothing, maybe add one or two, if demand really becomes significant (which I think very unlikely) then that's another argument to (either add a more general mechanism or) move to constraints. How's that?

If we replace subtyping with explicit coercions, does that "fix" things enough that we can move forward, and consider switching to a more constraint-based system (less complex because we have monitored demand and discovered we really only need a tiny minority of the possible coercions) in the future?