function processUserInput(input: String, requirement: InputReqs[input]): Unit = ...
type InputReqs[input] = {
// We'll say that a Proposition takes Boolean expressions and turn them into types
notTooLong: Proposition[length(input) < 128],
authorIsNotBlocked: AuthorIsNotBlocked[input],
sanitized: Sanitized[input],
...
}
where you might have the following functions (which are all examples of parse don't validate)
function checkIfAuthorIsBlocked(author: String, input: String): Maybe[AuthorIsNotBlocked[input]] = ...
// Create a pair that contains both the sanitized String and a tag that it has been sanitized
function sanitizeString(input: String): (output: String, Sanitized[output]) = ...
where just by types alone I know that e.g. length checking must occur after sanitization (because sanitizeString generates a new `output` that is distinct from `input`) and don't have to write down in docs somewhere that you might cause a bug if you check lengths before sanitization because maybe sanitization changes the length of the input.
Note that this is also strictly stronger than a simple precondition/postcondition system or some sort of assertion system because properties of the input that we care about may not be observable at runtime/from the input alone (e.g. AuthorIsNotBlocked can't be asserted based only on input: you'd have to change the runtime representation of input to include that information).
Note that this is also strictly stronger than a simple precondition/postcondition system or some sort of assertion system because properties of the input that we care about may not be observable at runtime/from the input alone (e.g. AuthorIsNotBlocked can't be asserted based only on input: you'd have to change the runtime representation of input to include that information).