As a user, I want to be able to omit quantifier bounds and have them be inferred wherever possible. This should be possible except when quantifying over infinite types, and it should be possible to quantify over function, map, and list types without explicitly specifying a quantifier bound.
To accomplish this, we can change the type system so that for each type there exists a bound on the cardinality of elements of that type. We put a maximum cardinality on functions, lists, and maps, specified as part of the type. Then when a quantifier bound is omitted, we can infer the maximum bound for that type. In the cases of function and map types, a cardinality bound can be inferred when not specified, based on the cardinality of the domain or key type.
This should result in quantifier bounds being inferrable except when using types containing infinite scalar types (i.e., natural numbers or integers).
morganthomas
commented
2 years ago
As a user, I want to be able to omit quantifier bounds and have them be inferred wherever possible. This should be possible except when quantifying over infinite types, and it should be possible to quantify over function, map, and list types without explicitly specifying a quantifier bound.
To accomplish this, we can change the type system so that for each type there exists a bound on the cardinality of elements of that type. We put a maximum cardinality on functions, lists, and maps, specified as part of the type. Then when a quantifier bound is omitted, we can infer the maximum bound for that type. In the cases of function and map types, a cardinality bound can be inferred when not specified, based on the cardinality of the domain or key type.
This should result in quantifier bounds being inferrable except when using types containing infinite scalar types (i.e., natural numbers or integers).