Refinement Without Specification

Summary

Imagine we have a SQL database with a user table, and users have a non-nullable is_activated boolean column. Having read That Boolean Should Probably Be Something else, you decide to migrate it to a nullable activated_at column. You can change any of the SQL queries that read/update the user table but not any of the code that uses the results of these queries. Can we make this change in a way that preserves all external properties? Yes. If an update would set is_activated to true, instead set it to the current date. Now define the refinement mapping that takes a new_user and returns an old_user. All columns will be unchanged except is_activated, which will be f(new_user).is_activated = if new_user.activated_at == NULL then FALSE else TRUE Now new code can use new_user directly while legacy code can use f(new_user) instead, which will behave indistinguishably from the old_user. A little more time passes and you decide to switch to an event sourcing-like model. So instead of an activated_at column, you have a user_events table, where every record is (user_id, timestamp, event). So adding an activate event will activate the user, adding a deactivate event will deactivate the user. Once again, we can update the queries but not any of the code that uses the results of these queries. Can we make a change that preserves all external properties? Yes. If an update would change is_activated, instead have it add an appropriate record to the event table. Now, define the refinement mapping that takes newer_user and returns new_user. The activated_at field will be computed like this: g(newer_user).activated_at = # last_activated_event let lae = newer_user.events .filter(event = "activate" | "deactivate") .last, in if lae.event == "activate" then lae.timestamp else NULL Now new code can use newer_user directly while old code can use g(newer_user) and the really old code can use f(g(newer_user)). Mutability constraints I said "these preserve all external properties" and that was a ...