Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat!: Allow "Row Variables" declared as List<Type> #804

Merged
merged 70 commits into from
May 22, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
70 commits
Select commit Hold shift + click to select a range
7b242ac
Refactor: break out fn valid_row for validating a TypeRow
acl-cqc Jan 10, 2024
ba05010
Type::{validate,substitute}_in_row, {Substitution,SubstValues}::apply…
acl-cqc Jan 10, 2024
59c5854
[test] types.rs::construct - also validate
acl-cqc Jan 12, 2024
72b4fb2
[tests] poly_func.rs: test row variables
acl-cqc Jan 12, 2024
2cf1e7f
[test] validate Hugr passing around Function of unknown arity
acl-cqc Jan 12, 2024
8899806
[tests]Validation prevents row variables being used in node signatures
acl-cqc Jan 12, 2024
e1f1825
Simplify default apply_typevar_in_row
acl-cqc Jan 12, 2024
1074093
Separate TypeEnum::RowVariable
acl-cqc Jan 12, 2024
4291848
Merge remote-tracking branch 'origin/main' into feat/row_typevar
acl-cqc Apr 15, 2024
98c75a2
Doc updates - no DeBruijn, ref OpDef vs FuncDefn
acl-cqc Apr 15, 2024
b918bee
Remove unused test setup changes
acl-cqc Apr 15, 2024
a096f1a
Merge remote-tracking branch 'origin/main' into feat/row_typevar
acl-cqc May 9, 2024
4b0e23f
Combine Type::substitute(_in_row), doc, add TODOs
acl-cqc May 9, 2024
a0aba20
FunctionType/PolyFuncType validate_varargs (fixed-len not reqd)
acl-cqc May 9, 2024
bd0689f
Type::validate(=>_1type), fix TypeParam to call validate_in_row
acl-cqc May 10, 2024
72f4b98
{subst,valid}_row => TypeRow::{substitute,validate_var_len}
acl-cqc May 10, 2024
d9653aa
Normalize representation of row variable as TypeArg; extend check_typ…
acl-cqc May 10, 2024
15bf177
Test bad schema, test can't fit row variable into type hole
acl-cqc May 10, 2024
bc11c68
Extend validation tests using eval+parallel
acl-cqc May 10, 2024
f39373b
And extend no_outer_row_variables to include unconnected out'port's o…
acl-cqc May 10, 2024
bd39303
comments re. canonicalization, tests
acl-cqc May 10, 2024
ed64d12
clippy
acl-cqc May 11, 2024
d02c9c0
single_type_seq -> seq1ty
acl-cqc May 11, 2024
50b9c85
Merge remote-tracking branch 'origin/main' into feat/row_typevar
acl-cqc May 11, 2024
742ab55
Combine helpers giving extension_with_eval_parallel
acl-cqc May 12, 2024
ce72762
Add RowVar to serialization/tys.py
acl-cqc May 12, 2024
c556a8a
Regenerate schema
acl-cqc May 12, 2024
7214cbc
Really regenerate schema (after poetry install)
acl-cqc May 12, 2024
ce28154
Use Vec<TypeArg> .into() -> TypeArg
acl-cqc May 14, 2024
0e4b232
Add TypeParam::new_list
acl-cqc May 14, 2024
5b39b9c
rowparam() -> rowp.clone()
acl-cqc May 14, 2024
9ae2255
new_row_var => new_row_var_use, some cleanups using .into()
acl-cqc May 14, 2024
412ec08
squash! Add TypeParam::new_list
acl-cqc May 14, 2024
34ed4c9
Fix apply_row_var...TODO cover this
acl-cqc May 14, 2024
85d1969
check_type_arg_rv: improve comment
acl-cqc May 14, 2024
3cf333d
Remove rowvar_in_list using TypeParam::contains
acl-cqc May 14, 2024
2929135
Add Type::row_var_bound
acl-cqc May 14, 2024
0afdaf9
Remove check_type_arg_rv
acl-cqc May 14, 2024
5a8bf88
Use Type .into() -> TypeArg more
acl-cqc May 14, 2024
2e53529
Extend comment that TypeArg::Variable's are not row-vars
acl-cqc May 14, 2024
ed09ae6
type_row.rs: comment ...Variable]*s*
acl-cqc May 14, 2024
8c93c9d
Add check_type_arg tests as rstest cases
acl-cqc May 14, 2024
8811e1a
More tests! (giving up on rstest)
acl-cqc May 14, 2024
d728714
Add a couple of PolyFuncType-serialization tests
acl-cqc May 14, 2024
9af9d01
In validation, panic upon malformed TypeArgVariable
acl-cqc May 15, 2024
ef86cd7
Correct comment in TypeArg::new_var_use
acl-cqc May 15, 2024
0ff4a05
Add anti-row-var checks in TypeRow::get/get_mut
acl-cqc May 15, 2024
b9fc1cf
Make TypeRow::get(_mut) pub only to crate::types
acl-cqc May 15, 2024
bcffd57
Revert "Make TypeRow::get(_mut) pub only to crate::types"
acl-cqc May 15, 2024
98cf6af
row_var_bound -> is_row_var
acl-cqc May 15, 2024
4a41f96
Clarify bound in Type::new_(,row_)var_use
acl-cqc May 15, 2024
5359441
Thank you Doug!
acl-cqc May 15, 2024
fdb19ae
Comments (Function values, "must match" => "must be exactly")
acl-cqc May 15, 2024
d949cc9
Another TypeParam::new_list
acl-cqc May 15, 2024
571d025
Test: p -> seq_param
acl-cqc May 15, 2024
a353026
Test: rowvar = Type::new_row_var_use
acl-cqc May 15, 2024
93536b3
Capture TypeArg::Type substituting-to-multiple in a unit test, fix
acl-cqc May 15, 2024
d339e2c
Another test with a list-of-list-of-type
acl-cqc May 20, 2024
71b3ae2
Use vec![].into() somewhat selectively
acl-cqc May 20, 2024
b77e3c8
Merge 'origin/main' into feat/row_typevar. Proptest failing...
acl-cqc May 20, 2024
91317ae
Fix proptest by local reject
acl-cqc May 20, 2024
3cbccc7
Temp remove TypeRow checks
acl-cqc May 20, 2024
a43e0a1
Merge remote-tracking branch 'origin/main' into feat/row_typevar
acl-cqc May 20, 2024
e0c7162
Add non-debug asserts in FunctionType
acl-cqc May 20, 2024
7ebb596
Combine Type::validate_1type / validate_in_row to validate(bool,...)
acl-cqc May 20, 2024
bc2d358
validate_varargs => validate_var_len
acl-cqc May 20, 2024
5b63d0c
RowVarOutsideRow => RowVarWhereTypeExpected
acl-cqc May 21, 2024
2a28052
check_no_rowvars - ignore index, check whole row - breaks no_outer_ro…
acl-cqc May 21, 2024
c559abc
FunctionType::find_row_var, check in builder and validation (before p…
acl-cqc May 21, 2024
98c1fc9
Tests (rewrite w/out builder; add builder test, using now-pub-crate e…
acl-cqc May 21, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 18 additions & 1 deletion hugr-py/src/hugr/serialization/tys.py
Original file line number Diff line number Diff line change
Expand Up @@ -214,6 +214,15 @@ class Variable(ConfiguredBaseModel):
b: "TypeBound"


class RowVar(ConfiguredBaseModel):
"""A variable standing for a row of some (unknown) number of types.
May occur only within a row; not a node input/output."""

t: Literal["R"] = "R"
i: int
b: "TypeBound"


class USize(ConfiguredBaseModel):
"""Unsigned integer size type."""

Expand Down Expand Up @@ -321,7 +330,15 @@ class Type(RootModel):
"""A HUGR type."""

root: Annotated[
Qubit | Variable | USize | FunctionType | Array | SumType | Opaque | Alias,
Qubit
| Variable
| RowVar
| USize
| FunctionType
| Array
| SumType
| Opaque
| Alias,
WrapValidator(_json_custom_error_validator),
Field(discriminator="t"),
]
Expand Down
11 changes: 10 additions & 1 deletion hugr/src/builder/build_traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ use crate::{
types::EdgeKind,
};

use crate::extension::{ExtensionRegistry, ExtensionSet, PRELUDE_REGISTRY};
use crate::extension::{ExtensionRegistry, ExtensionSet, SignatureError, PRELUDE_REGISTRY};
use crate::types::{FunctionType, PolyFuncType, Type, TypeArg, TypeRow};

use itertools::Itertools;
Expand Down Expand Up @@ -645,6 +645,15 @@ fn add_node_with_wires<T: Dataflow + ?Sized>(
inputs: impl IntoIterator<Item = Wire>,
) -> Result<(Node, usize), BuildError> {
let nodetype: NodeType = nodetype.into();
// Check there are no row variables, as that would prevent us
// from indexing into the node's ports in order to wire up
nodetype
.op_signature()
.as_ref()
.and_then(FunctionType::find_rowvar)
.map_or(Ok(()), |(idx, _)| {
Err(SignatureError::RowVarWhereTypeExpected { idx })
})?;
let num_outputs = nodetype.op().value_output_count();
let op_node = data_builder.add_child_node(nodetype.clone());

Expand Down
38 changes: 35 additions & 3 deletions hugr/src/builder/dataflow.rs
Original file line number Diff line number Diff line change
Expand Up @@ -208,13 +208,14 @@ pub(crate) mod test {

use crate::builder::build_traits::DataflowHugr;
use crate::builder::{BuilderWiringError, DataflowSubContainer, ModuleBuilder};
use crate::extension::prelude::BOOL_T;
use crate::extension::{ExtensionId, EMPTY_REG};
use crate::extension::prelude::{BOOL_T, USIZE_T};
use crate::extension::{ExtensionId, SignatureError, EMPTY_REG, PRELUDE_REGISTRY};
use crate::hugr::validate::InterGraphEdgeError;
use crate::ops::{handle::NodeHandle, Lift, Noop, OpTag};

use crate::std_extensions::logic::test::and_op;
use crate::types::Type;
use crate::types::type_param::TypeParam;
use crate::types::{Type, TypeBound};
use crate::utils::test_quantum_extension::h_gate;
use crate::{
builder::test::{n_identity, BIT, NAT, QB},
Expand Down Expand Up @@ -550,4 +551,35 @@ pub(crate) mod test {
);
Ok(())
}

#[test]
fn no_outer_row_variables() -> Result<(), BuildError> {
let e = crate::hugr::validate::test::extension_with_eval_parallel();
let tv = Type::new_row_var_use(0, TypeBound::Copyable);
let mut fb = FunctionBuilder::new(
"bad_eval",
PolyFuncType::new(
[TypeParam::new_list(TypeBound::Copyable)],
FunctionType::new(
Type::new_function(FunctionType::new(USIZE_T, tv.clone())),
vec![],
),
),
)?;

let [func_arg] = fb.input_wires_arr();
let i = fb.add_load_value(crate::extension::prelude::ConstUsize::new(5));
let ev = e.instantiate_extension_op(
"eval",
[vec![USIZE_T.into()].into(), vec![tv.into()].into()],
&PRELUDE_REGISTRY,
)?;
let r = fb.add_dataflow_op(ev, [func_arg, i]);
// This error would be caught in validation, but the builder detects it much earlier
assert_eq!(
r.unwrap_err(),
BuildError::SignatureError(SignatureError::RowVarWhereTypeExpected { idx: 0 })
);
Ok(())
}
}
3 changes: 3 additions & 0 deletions hugr/src/extension.rs
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,9 @@ pub enum SignatureError {
/// A type variable that was used has not been declared
#[error("Type variable {idx} was not declared ({num_decls} in scope)")]
FreeTypeVar { idx: usize, num_decls: usize },
/// A row variable was found outside of a variable-length row
#[error("Expected a single type, but found row variable {idx}")]
RowVarWhereTypeExpected { idx: usize },
/// The result of the type application stored in a [Call]
/// is not what we get by applying the type-args to the polymorphic function
///
Expand Down
17 changes: 16 additions & 1 deletion hugr/src/extension/op_def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,10 @@ impl OpDef {
// TODO https://github.com/CQCL/hugr/issues/624 validate declared TypeParams
// for both type scheme and custom binary
if let SignatureFunc::TypeScheme(ts) = &self.signature_func {
ts.poly_func.validate(exts)?;
// The type scheme may contain row variables so be of variable length;
// these will have to be substituted to fixed-length concrete types when
// the OpDef is instantiated into an actual OpType.
ts.poly_func.validate_var_len(exts)?;
}
Ok(())
}
Expand Down Expand Up @@ -482,6 +485,7 @@ mod test {
use crate::extension::{SignatureError, EMPTY_REG, PRELUDE_REGISTRY};
use crate::ops::{CustomOp, OpName};
use crate::std_extensions::collections::{EXTENSION, LIST_TYPENAME};
use crate::types::type_param::TypeArgError;
use crate::types::Type;
use crate::types::{type_param::TypeParam, FunctionType, PolyFuncType, TypeArg, TypeBound};
use crate::{const_extension_ids, Extension};
Expand Down Expand Up @@ -639,6 +643,17 @@ mod test {
def.compute_signature(&args, &EMPTY_REG),
Ok(FunctionType::new_endo(vec![tv]))
);
// But not with an external row variable
let arg: TypeArg = Type::new_row_var_use(0, TypeBound::Eq).into();
assert_eq!(
def.compute_signature(&[arg.clone()], &EMPTY_REG),
Err(SignatureError::TypeArgMismatch(
TypeArgError::TypeMismatch {
param: TypeBound::Any.into(),
arg
}
))
);
Ok(())
}

Expand Down
21 changes: 20 additions & 1 deletion hugr/src/hugr/serialize/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -419,13 +419,32 @@ fn polyfunctype1() -> PolyFuncType {
PolyFuncType::new([TypeParam::max_nat(), TypeParam::Extensions], function_type)
}

fn polyfunctype2() -> PolyFuncType {
let tv0 = Type::new_row_var_use(0, TypeBound::Any);
let tv1 = Type::new_row_var_use(1, TypeBound::Eq);
let params = [TypeBound::Any, TypeBound::Eq].map(TypeParam::new_list);
let inputs = vec![
Type::new_function(FunctionType::new(tv0.clone(), tv1.clone())),
tv0,
];
let res = PolyFuncType::new(params, FunctionType::new(inputs, tv1));
// Just check we've got the arguments the right way round
// (not that it really matters for the serialization schema we have)
res.validate_var_len(&EMPTY_REG).unwrap();
res
}

#[rstest]
#[case(FunctionType::new_endo(type_row![]).into())]
#[case(polyfunctype1())]
#[case(PolyFuncType::new([TypeParam::Opaque { ty: int_custom_type(TypeArg::BoundedNat { n: 1 }) }], FunctionType::new_endo(type_row![Type::new_var_use(0, TypeBound::Copyable)])))]
#[case(PolyFuncType::new([TypeBound::Eq.into()], FunctionType::new_endo(type_row![Type::new_var_use(0, TypeBound::Eq)])))]
#[case(PolyFuncType::new([TypeParam::List { param: Box::new(TypeBound::Any.into()) }], FunctionType::new_endo(type_row![])))]
#[case(PolyFuncType::new([TypeParam::new_list(TypeBound::Any)], FunctionType::new_endo(type_row![])))]
#[case(PolyFuncType::new([TypeParam::Tuple { params: [TypeBound::Any.into(), TypeParam::bounded_nat(2.try_into().unwrap())].into() }], FunctionType::new_endo(type_row![])))]
#[case(PolyFuncType::new(
[TypeParam::new_list(TypeBound::Any)],
FunctionType::new_endo(Type::new_tuple(Type::new_row_var_use(0, TypeBound::Any)))))]
#[case(polyfunctype2())]
fn roundtrip_polyfunctype(#[case] poly_func_type: PolyFuncType) {
check_testing_roundtrip(poly_func_type)
}
Expand Down
30 changes: 23 additions & 7 deletions hugr/src/hugr/validate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use crate::ops::custom::{resolve_opaque_op, CustomOp};
use crate::ops::validate::{ChildrenEdgeData, ChildrenValidationError, EdgeValidationError};
use crate::ops::{FuncDefn, OpTag, OpTrait, OpType, ValidateOp};
use crate::types::type_param::TypeParam;
use crate::types::EdgeKind;
use crate::types::{EdgeKind, FunctionType};
use crate::{Direction, Hugr, Node, Port};

use super::views::{HierarchyView, HugrView, SiblingGraph};
Expand Down Expand Up @@ -211,7 +211,20 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
}
}

// Secondly that the node has correct children
// Secondly, check that the node signature does not contain any row variables.
// (We do this here so it's before we try indexing into the ports of any nodes).
op_type
.dataflow_signature()
.as_ref()
.and_then(FunctionType::find_rowvar)
.map_or(Ok(()), |(idx, _)| {
Err(ValidationError::SignatureError {
node,
cause: SignatureError::RowVarWhereTypeExpected { idx },
})
})?;

// Thirdly that the node has correct children
self.validate_children(node, node_type)?;

Ok(())
Expand Down Expand Up @@ -301,11 +314,14 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
var_decls: &[TypeParam],
) -> Result<(), SignatureError> {
match &port_kind {
EdgeKind::Value(ty) => ty.validate(self.extension_registry, var_decls),
EdgeKind::Value(ty) => ty.validate(false, self.extension_registry, var_decls),
// Static edges must *not* refer to type variables declared by enclosing FuncDefns
// as these are only types at runtime.
EdgeKind::Const(ty) => ty.validate(self.extension_registry, &[]),
EdgeKind::Function(pf) => pf.validate(self.extension_registry),
// as these are only types at runtime. (Note the choice of `allow_row_vars` as `false` is arbitrary here.)
EdgeKind::Const(ty) => ty.validate(false, self.extension_registry, &[]),
// Allow function "value" to have unknown arity. A Call node will have to provide
// TypeArgs that produce a known arity, but a LoadFunction might pass the function
// value ("function pointer") around without knowing how to call it.
EdgeKind::Function(pf) => pf.validate_var_len(self.extension_registry),
_ => Ok(()),
}
}
Expand Down Expand Up @@ -794,4 +810,4 @@ pub enum InterGraphEdgeError {
}

#[cfg(test)]
mod test;
pub(crate) mod test;
Loading
Loading