A possible approach, on which I was experimenting some time ago, would be to use ephemerons to attach predicates to data, which could be later checked (a mere presence check) on the caller side.
Something like this:
let typecheck code =
ensures ["well-typed"] @@
perform_typecheck code
let normalize code =
requires ["well-typed"];
provides ["well-typed"; "normal-form"] @@
perform_normalization code
let optimize code =
requires ["normal-form"; "well-typed"];
provides ["normal-form"; "well-typed"; "optimized"] @@
do_optimizations code
where requires tags obj
is a function of type string list -> 'a -> unit
that takes a list of tags, denoting features, and checks that they are attached to the given object, and provides tags obj
is a function of type string list -> object -> object
takes a list of features and attaches it to the object (an alternative syntax is having type object -> unit
, since an ephemeron is a mutable hashtable).
The implementation is using ephemerons, which are hashtables indexed with arbitrary boxed objects with a special treatment of liveness (i.e., values from those hashtables disappear when the index disappear, so no memory leakage should happen).
The main benefit of this approach is its simplicity, it is vanilla OCaml, it is easy to implement, and easy to disable. The main drawback is that it works only with heap values (aka boxed values) and that it is not reflected in the function signature. And of course, since it is that simple, the contract can’t actually be a formula, especially that references the host language.