Encoding of Higher-Order Contracts.

[marcoonroad]

We could generalize this current encoding of type refinements into higher-order contracts. Such contracts are used on lambda expressions, which are values with the sole responsibility of beta-reduction. On that setting, we have the following typing:

input -> output

Where the input type refines some type a, and the type output could be a refinement type for some type b and the input type itself as well (that is, the output type is a dependent type upon the input type). Notice that this relation introduces as well some concept of blaming, where the ill-refined input blames the client while the ill-refined output blames the service/provider.

[marcoonroad]

Bump/update:

The introduction of subtyping for such refinement relations will be a huge pain, 'cause it implies covariance & contravariance for such lambda expressions.