You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
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:
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:
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:
[^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.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
Bounds and Constraints
hugr-core
allows to attach a bound to runtime types, which is eitherCopyable
orAny
. As the name suggests, values of types that are markedCopyable
can be copied by connecting multiple input ports to the same outputport that produces a value of that type. The
Copyable
bound also includes theability to delete the value by not connecting the output port. Types that are
marked
Any
must be treated linearly. Throughouthugr-core
a bound isattached to every type, presumably as a cache.
hugr-core
also adds a subtyping relation to this system: The type of copyabletypes 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:
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 typesxs
, the constraint(variadic x xs)
holds whenever all elements ofxs
arex
. 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 ofits 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 logicbehind 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:
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 abuiltin capability for concatenation; however that makes unification and pattern
matching over
hugr-core
rows be ambiguous. When lists are restricted to asingle 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:
Example: Bounded Naturals
hugr-core
's type for static naturals can come with an upper bound. Given aconstraint
(nat-lte? ?n ?m)
which holds when a natural?n
is less than orequal to a natural
?m
, we can define a bounded natural type with its valuesdeclaratively:
Migration
Migration between
hugr-core
and a constraint based system is admittedly tricky, which is why it wasn'tincluded in #1542. The current state of the discrepancy is as follows:
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:
[^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.
Beta Was this translation helpful? Give feedback.
All reactions