Ghosts of departed proofs using F#

Explanation.fs

module Explanation

(*

So what is going on in module `ValidatedSum`? This is a more detailed explanation and a piece of guidance. The goal of
all of this is being able to define libraries with "safe" APIs. To be more precise, "safe" means that functions with
interesting preconditions can only be used (applied) such that the precondition is guaranteed to hold; it is impossible
to apply a function on inputs for which the precondition does not hold.

A well-known example is `List.head`. The precondition of applying this function to list `l` is that `l` is non-empty. If
`l` is empty, the function crashes. This means that `List.head` is a partial function and partial functions are not
nice. In particular, the precondition is _implicit_ and it is the responsibility and, more importantly, discipline of
the library user to ensure that in expression `List.head l` list `l` is not empty.

`List.head` is just one example of an unsafe library API. Preconditions can be more involved than that of a non-empty
list. The example precondition in module `ValidatedSum` is that the two integers are validated by the same rules.
Another example of a precondition is that the user is authorized to perform a specific action.

The "Ghost of departed proofs" (GDP) involves three parties:

- You and your library
- Users of the library, whom you want to force to use your library in a correct way
- The GDP library

Your library (the library from now on):

- Depends on GDP
- Might use the `Named` type
- Defines abstract "evidence" types with private representation and public functions which compute evidence
- Requires evidence values in the API signatures

Type `Valid<'validator,'a>` is an example of an evidence type. It serves as a _proof_ that 'a was validated using a
specific validator. Users of the library can only obtain this proof by using a function provided by the library. That
function is trusted by the library and it is impossible for a client module to provide a self-made (false) proof.

Users of the library (client modules):

- Depend on GDP
- Depend on the (your) library
- Attach names to values using f-n `name`, `name2`, etc.
- Responsible for constructing evidence values using functions provided by the library
- Invoke actual library functions of interest using evidence values and "normal" arguments (if any) using `Context`.

Next we rewrite the example from `ValidatedSum` to better illustrate this division:

*)

module Library =

    open Ghosts

    type Validator = int -> Result<int,string>

    let greaterThanZero : Validator = fun a ->
        if 0 < a then Ok a else Error $"{a} is not greater than zero."
    
    let even : Validator = fun a ->
        if a % 2 = 0 then Ok a else Error $"{a} is not even."

    /// The evidence/proof type.
    type Valid<'validator,'a> = private Valid of 'a

    /// Produces evidence.
    let validate (Named validator : Named<'validator,Validator>) a : Result<Valid<'validator,int>,string> =
        match validator a with
        | Ok a -> Ok (Valid a)
        | Error e -> Error e

    /// The "core" library function with the precondition about same validation encoded explicitly in the type.
    let addValidated (Valid a : Valid<'validator,_>) (Valid b : Valid<'validator,_>) = a + b

module Client =

    open Ghosts
    open Library

    let validateAndAdd (a : int) (b : int) : Result<int,_> =
        name greaterThanZero { new Context<Validator,_> with
            member _.WithNamed validator =
                match validate validator a, validate validator b with
                | Ok valid_a, Ok valid_b -> Ok (addValidated valid_a valid_b)
                | Error e, _ -> Error e
                | _, Error e -> Error e
        }

(*

The pattern where a trusted function provides "special" values of abstract types as tokens/evidence/whatever is well
known. What GDP adds is the possibility to express relations between different values using phantom type variables --
"names". For example, a permission token (evidence value) can be related to the object it applies to without risk of
checking authorization for one object and erroneously passing another object. In our example, the relation is between
two integers which are validated using the same rule. This scheme becomes more interesting and powerful when evidence
types have not one but two or more phantom type variables for "names". Then more values can be related by types.

Finally, the role of `Context` must be clarified. For technical reasons explained further, it must be used in a client
module, but the required object expression syntax combined with application of function `make` makes the complete
function somewhat less readable. This is a matter of understanding and getting used to the structure of what is going
on. Namely, if one looks closely at

name greaterThanZero { new Context<Validator,_> with
    member _.WithNamed validator = <expression>
}

it is, in spirit, the same as

name greaterThanZero (fun validator -> <expression>).

This is the essence of GDP: function `name` accepts a plain value (`greaterThanZero`), internally attaches to it a
unique type-level name and then passes it to the given function, binding the now named value to `validator`. The reason
for using `Context` is that F# lacks higher-ranked types in regular functions; members, which can have their own "local"
type variables can be used as a substitution for the price of verbosity. In Haskell and PureScript this additional
"layer" is not needed and the "desugared" lambda can esed directly as above.

Finally, the core question about why this works at all: where does the unique type "name" come from? There is nothing
special or magical here. Consider the implementation of `name` from module `Ghosts` in relation to member `WithNamed`:

type Context<'a,'r> =
    abstract WithNamed<'name> : Named<'name,'a> -> 'r

let name (a : 'a) (context : Context<'a,'r>) : 'r = context.WithNamed (Named a)

When value `Named a` is passed to `WithNamed`, what is its type _inside_ of this member? `WithNamed` is polymorphic in
both 'a and 'name. While 'a is fixed "on the outside" and instantiated by a client module, type parameter 'name is not.
This means that inside of `WithNamed` it is not really known (expectedly, because it is a polymorphic member after all).
In this situation, the type system (or the compiler, however you want to see it) chooses, or "generates" a fresh type
for 'name. This can be observed by hovering the mouse above `valid_a` and `valid_b` above and inside of counter-example
functions in module `ValidatedSum` where distinct names can be clearly seen. Interestingly, the F# compiler is
implemented such that it chooses a nice sequence of 'a, 'b, etc.

*)

Ghosts.fs

/// A basic library based on the "Ghosts of departed proofs" paper. Study the usage example module first!
module Ghosts

/// A value with an attached type-level name.
type Named<'name,'a> = private Named of 'a

/// Access to the named value as a pattern.
let (|Named|) (Named a) = a

/// A context within which a result of type 'r can be computed from a named value of type 'a with some (unknown) name.
type Context<'a,'r> =
    abstract WithNamed<'name> : Named<'name,'a> -> 'r

/// Given a value, attach a name to this value and compute a result within the context of that name.
let name (a : 'a) (context : Context<'a,'r>) : 'r =
    context.WithNamed (Named a)

/// A context withing which a result of type 'r can be computed from names values of types 'a and 'b with some (unknown
/// but distinct) names.
type Context2<'a, 'b, 'r> =
    abstract WithNamed : Named<'name1,'a> -> Named<'name2,'b> -> 'r

/// Given two values, attaches distinct names to those values and compute a result within the context of those names.
let name2 (a : 'a) (b : 'b) (context : Context2<'a,'b,'r>) : 'r =
    context.WithNamed (Named a) (Named b)

ValidatedSum.fs

module ValidatedSum

// Suppose we want to validate integer numbers. We capture this by the following type:

type Validator = int -> Result<int,string>

// Obviously there are multiple ways of validating and two different validations cannot be distinguished by this type
// only. As an example, we define two different validators:

let greaterThanZero : Validator = fun a ->
    if 0 < a then Ok a else Error $"{a} is not greater than zero."

let even : Validator = fun a ->
    if a % 2 = 0 then Ok a else Error $"{a} is not even."

// Despite having the same type, these two validation functions obviously implement very different validation rules.

// Now we want to implement addition of integers, with interesting requirements:
//
// (1) only validated integers may be added,
// (2) validation rules may not be mixed.
//
// Requirement (2) is easy to realize by passing a single `Validator` along the two integers to sum:

let addValidatedNaive (a : int) (b : int) (validator : Validator) = failwith "Implementation goes here"

// This approach works, but has two shortcomings:
//
// - The function has two responsibilities: actually adding (the "logic") and validating. This goes against the beloved
//   single responsibility principle.
//
// - More interestingly, the result type of the function is not convenient: if `addValidatedNaive` performs validation
//   internally, it cannot just return a simple `int` as a result. For when validation fails, this has to be
//   communicated to the caller. So the result type must also be a `Result<int,string>`, unless we opt for raising an
//   exception. Which we don't.
//
// A way of solving both of the above points is to move the responsibility of validation to the caller, but in such a
// way that only _valid_ integers can be passed to the function. Then the function can return a simple `int`. Note that
// the following is _not_ a solution, because `Result<int,string>` can be `Error`, i.e. an invalid integer:

let addValidateNaive2 (a : Result<int,string>) (b : Result<int,string>) : int = failwith "Does not work"

// Instead, we introduce a type values of which serve as evidence that the wrapped integer is valid. Crucially, only
// this module can provide evidence by actually performing validation; this is achieved by making the type abstract:

type Valid<'a> = private Valid of 'a // Note "private" here

let validate (validator : Validator) a =
    match validator a with
    | Ok a -> Ok (Valid a)
    | Error e -> Error e

// Now the addition function can become much nicer:

let addBetter (Valid a : Valid<int>) (Valid b : Valid<int>) : int = a + b

// Both of the shortcomings above are solved: the function has a single responsibility (addition) and the result type is
// easy to consume by a client module which performed validation work as a "price".
//
// While `addBetter` satisfies requirement (1), it does not satisfy (2): nothing prevents a client module to mix
// different validations:

let wrong : Result<int,string> =
    let map2 = failwith "standard applicative glue stuff, not interesting here"
    map2 addBetter (validate greaterThanZero 3) (validate even 3) // Validation mixed here

// We can use types to enforce that both integers have been validated by the same validator. For this to work, we
// introduce a type parameter which will be the (type-level) "name" of a `Validator`. Then we will enforce the same
// "name" in all signatures.

/// A valid value of type 'a validated by a `Validator` with name 'validator.
///
/// or:
///
/// A value of type 'a along with a proof that it is valid according to `Validator` named 'validator. 
type Valid<'validator,'a> = private Valid of 'a // Also private, as above

// Module `Ghosts` provides machinery to do all of this. First we need a variant of function `validate` which can
// work with names. Specifically, it preserves the name of the validator in the validation outcome.

open Ghosts

let validateNamed (Named validator : Named<'validator,Validator>) a : Result<Valid<'validator,int>,string> =
    match validator a with
    | Ok a -> Ok (Valid a)
    | Error e -> Error e

// Observe how type parameter `validator above is "passed" from the input to the output type. This is how we can
// "record" the validator used in the validation outcome value (again, using its type). It is satisfying that the
// actual implementation of the function does not differ from the original `validate`: all of the "naming" stuff happens
// on type level, via type inference.
//
// We forgot to define the main function of interest which adds two valid integers. Also it is pleasantly simple:

let addValidated (Valid a : Valid<'validator,_>) (Valid b : Valid<'validator,_>) = a + b

// Crucially, `addValidated` now _enforces_ in its type that the same validator was applied to both `a` and `b`, by
// repeating the validator "name". This implementation satisfies both requirements (1) and (2).
//
// The final step is to combine `validateNamed` and `addValidated` into one program. The following function chooses a
// single `Validator` and using the machinery of module `Ghosts` attaches a name to it in order to validate raw integers
// prior to applying function `addValidated`.

let validateAndAdd (a : int) (b : int) : Result<int,_> =
    // Attach a type-level name to the `greaterThanZero` validator
    name greaterThanZero { new Context<Validator,_> with
        member _.WithNamed validator =
            // Validate both raw integers with the (named) validator
            match validateNamed validator a, validateNamed validator b with
            // Apply the core function safely and cleanly
            | Ok valid_a, Ok valid_b -> Ok (addValidated valid_a valid_b)
            // Validation failure cases
            | Error e, _ -> Error e
            | _, Error e -> Error e
    }

// validateAndAdd 3 4 = Ok 7

// It is impossible to apply function `addValidated` in an unsafe way, i.e. when the inputs are validated differently.
// An attempt of doing so might look like below, where we try introduce a second named `validator2`. The function does
// not type check, because each application of `name` generates a fresh type-level name, incompatible with all other
// generated names.

let validateAndAddWrong (a : int) (b : int) : Result<int,_> =
    // The first validator
    name greaterThanZero { new Context<Validator,_> with
        member _.WithNamed validator1 =
            // The second, different validator
            name even { new Context<Validator,_> with
                member _.WithNamed validator2 =
                    // Validate raw integers using the two different validators
                    match validateNamed validator1 a, validateNamed validator2 b with
                    | Ok valid_a, Ok valid_b -> Ok (addValidated valid_a valid_b) // A nice type error here
                    | Error e, _ -> Error e
                    | _, Error e -> Error e
            }
    }

// Module `Ghosts` provides a `Context` for working with two named values at the same time, avoiding nesting as above.
// This won't fix the above function, but we can rewrite it more compactly.

let validateAndAddWrong2 (a : int) (b : int) : Result<int,_> =
    name2 greaterThanZero even { new Context2<Validator,Validator,_> with
        member _.WithNamed validator1 validator2 =
            match validateNamed validator1 a, validateNamed validator2 b with
            | Ok valid_a, Ok valid_b -> Ok (addValidated valid_a valid_b) // Same nice type error here
            | Error e, _ -> Error e
            | _, Error e -> Error e
    }

// Of course, this function is a deliberate counter-example and therefore does not compile. It does illustrate usage
// of `Context` together with `name2`. `Context3` with `name3` etc. can be defined as well.