I think I have an idea about how to have "types with invariants". Consider the following use case: I know that a function [f] returns elements of type [t] that satisfy the property [p]. We can probably have a function "suchthat : 'a ty -> ('a -> bool) -> 'a ty" that generates a new type descriptor.
I think I have an idea about how to have "types with invariants". Consider the following use case: I know that a function [f] returns elements of type [t] that satisfy the property [p]. We can probably have a function "suchthat : 'a ty -> ('a -> bool) -> 'a ty" that generates a new type descriptor.