Rather than a monad stack, are there any PLs where functions can just have a set of statically verified properties attached?