Comment by gue5t

These types don't seem to escape the scope of what can be described with algebraic types, but the relationships between them seem like you're looking for a notion of type-level functions: subset ≡ X => 2^X, partial ≡ A×B => (A+1)×partial(B)