Motivated simulation of GADTs in F#, quite motivational

GADTMotivation.fs

module GADTMotivation

(*
Here is a simple motivational example for GADTs and their usefulness for library design and domain modeling. Suppose we
need to work with settings which can be displayed and adjusted in a GUI. The set of possible setting "types" is fixed
and known in advance: integers, strings and booleans (check-boxes).
The GUI should show an example value for each possible setting type, e.g. 1337 for an integer setting and "Hello" for a
string setting. How can we model this small domain of setting types and computing example values?
*)

// A straightforward way is defining setting types as a DU:

type SettingType =
    | IntegerSetting
    | StringSetting
    | BoolSetting

// If we try defining the "example value" function, we immediately see a problem: what should its return type be?

let exampleValue = function
    | IntegerSetting -> failwith "We'd like to return 1377 but this will not compile"
    | StringSetting -> failwith """We'd like to return "Hello" but this will not compile"""
    | BoolSetting -> failwith "We'd like to return true but this will not compile"

// Well, that was a bit too naive, of course we cannot return different types in a match expression! So we unify them
// in a single type:

let exampleValue1 = function
    | IntegerSetting -> Choice1Of3 1377
    | StringSetting -> Choice2Of3 "Hello"
    | BoolSetting -> Choice3Of3 true

// Yay! DUs are cool so just wrap all possible outcomes in one and crush all those other peasant languages with the
// power of F# type system! Right?
// But is this actually nice (and I don't mean the language)? Value 'Choice1Of3 1377' is not literally an example of a
// integer setting, that would be value '1377'! Similarly for other cases. Even worse, the function is not "type safe"
// because nothing prevents erroneously returning 'Choice1Of3 ()' or some other garbage for the 'IntegerSetting' case! 

// Would it help if we make the function polymorphic in result type? Could it then return an integer or a string and so
// on in respective cases? So something along the lines of

let exampleValue2 (setting : SettingType) : 'a =
    match setting with
    | IntegerSetting -> failwith "Returning 1377 will still not compile"
    | StringSetting -> failwith "Similarly"
    | BoolSetting -> failwith "Nope"

// But this won't work either. A pure function of type 'SettingType -> a' cannot conjure up a value of _any_ type 'a'
// out of thin air, unless 'SettingType' contains enough information to construct an 'a'. It cannot know what 'a' is
// exactly because it is polymorphic, so client functions get to pick 'a' and they could pick anything! Because the
// function is pure, function input is the only potential source of information about 'a'. Or the _type_ of the input!
// Let's try making the settings type DU polymorphic where the type variable represents the intended setting type:

type SettingType<'a> =
    | IntegerSetting
    | StringSetting 
    | BoolSetting

// And the example value function becomes:

let exampleValue3 (setting : SettingType<'a>) : 'a =
    match setting with
    | IntegerSetting
    | StringSetting
    | BoolSetting -> failwith "We still want to return types of different values, but they don't unify with 'a'!"

// This did not help for the same reason: we don't know what 'a' is. Returning an integer won't unify its type with
// whatever the client function picked for 'a'. In fact, it could pick something which is neither integer, string nor
// boolean! According to our requirements 'SettingType<float>' is not a thing, but even more outrageous combinations
// like 'SettingType<List<unit>>' also become possible!

// However 'exampleValue3' does look nice, if you look carefully. Ignoring problems with the implementation, the
// signature could be read as "Given a setting type 'a', I will return you a value of type 'a'" and so this type is
// spot-on! In particular, the return value is not an ugly 'Choice3' thing as above, but ultimate to-the-point
// specification of what we want. Also 'exampleValue3' cannot return a wrong value, unlike with 'Choice3': the type
// system guarantees that if we ask for, say, a 'bool' that we also get a 'bool' and nothing else.
//
// At this point one could despair about the problems we uncovered while working on this simple domain. Luckily, FP
// does not end here and we _can_ have a nice solution using Generalized Algebraic Data Types (GADT). Well, not really,
// because F# does not support them, however a partial simulation is possible. The essence of GADTs is that we can have
// a polymorphic 'SettingType<a>' DU type and at the same time constrain 'a' to our three setting type types!

open Leibniz

type SettingTypeGADT<'a> =
    | IntSetting of Leibniz<int,'a>
    | StringSetting of Leibniz<string,'a>
    | BoolSetting of Leibniz<bool,'a>

// Riiight, what is going on? A value of type 'Leibniz<A,B>' can be understood as a _proof_ or _evidence_ that types
// 'A' and 'B' are equal, i.e. same. By carrying such a proof each DU constructor says "In my case 'a is int"
// or "In my case 'a is string" and so on. Elsewhere we can use these proof values for fun and profit. In fact, here is
// the type-safe, no-bullshit-Choice-wrappers function which returns an example value for each setting type:

let example (st : SettingTypeGADT<'a>) : 'a =
    match st with    
    | IntSetting proof -> coerce proof 1377
    | StringSetting proof -> coerce proof "Hello"
    | BoolSetting proof -> coerce proof true

// There is some serious funkyzeit happening here. For starters, we are almost returning values of different types in
// the match expression, which did not work above (of course). Only now, we use proof values carried by constructors of
// the GADT to convince the type system that 1377, which is an 'int', is also an 'a' and similarly that "Hello" being a
// 'string' is also an 'a', in that case only.
// At this point it must be mentioned that there is no reflection or unsafe casts involved. Yes, the relatively safe
// type casting using 'unbox' is employed, but it is alway safe due to how proof values ("the Leibniz") are constructed:
// essentially it cannot be anything else than the identity function in disguise. But leaving such operational mindset
// behind, it is still kind of magical that in 'example' we can apply the proof of int ~ 'a to seemingly go "up" from
// 'int' to 'a' without sub-typing or inheritance. Instead, this is just the ruthlessly mechanical substitution at work:
// 'proof' says that int ~ 'a, so we can "fill it in" in the signature of the function to see that it returns an 'int'!
// And if you are still in disbelief, here you go:

// Some helpers instead of using DU/GADT constructors directly. Not essential, only cosmetic. 'refl' is the proof that
// a type is equal to itself, which is true by definition of equivalence relations.
let intSetting = IntSetting refl
let stringSetting = StringSetting refl
let boolSetting = BoolSetting refl

let intExample : int = example intSetting
let boolExample : bool = example boolSetting
// let doesNotTypeCheck : int = example stringSetting

// This is almost ridiculous.

Leibniz.fs

module Leibniz

/// A context we cannot inspect or construct and therefore know nothing about.
type F<'a> = private | Dummy

/// A value of type 'Leibniz<a,b>' is a proof (witness) that types 'a' and 'b' are equal, i.e. are the same type.
[<NoEquality; NoComparison>]
type Leibniz<'a,'b> = Leibniz of (F<'a> -> F<'b>)

/// Any type 'a' is equal to itself.
let refl = Leibniz id

/// If type 'a' is equal to type 'b', then 'b' is equal to 'a'.
let symm (_ : Leibniz<'a,'b>) : Leibniz<'b,'a> = Leibniz unbox

/// Given a proof that types 'a' and 'b' are equal and a value of type 'a', we also have a value of type 'b', namely
/// the same value.
let coerce (_ : Leibniz<'a,'b>) (a: 'a) : 'b = unbox a

This is amazing. Thank you.