@@ -0,0 +1,123 @@
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'", which is exactly what
// we want! 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 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 going on 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.
Savelenko revised this gist