Savelenko

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?
*)

Savelenko

namespace PhantomTypes

module User =

    type Username<'a> = private Username of string with
        member u.Value = let (Username username) = u in username

    type Short = interface end
    type Full = interface end

Savelenko

namespace PhantomTypes

module Phantom =

    // Private, so must use function 'prove'.
    type ProofOf<'a> = private | ProofOfA

    // A module proves that it can construct values of type 'a' by providing a value to this function.
    let prove (_ : 'a) : ProofOf<'a> = ProofOfA

Savelenko

// The engine interface and helpers

type IEngine<'a,'b> =
    abstract member Capacity : int // Does not depend on 'a or 'b; just an example
    // Some other stuff here possible depending on 'a and 'b

/// A function which works on any engine polymorphically and returns a result of type 'r'. Needed because
/// F# does not support higher-ranked types (not the same as HKT!) in regular functions. This does work in members.
type EngineFunction<'r> =
    abstract member Apply : IEngine<'a,'b> -> 'r

Savelenko

(* What if F# had type families? *)

// We are a message processing system. There are regular and confidential messages to be delivered. Several delivery
// methods are supported. The main "business rule" is that regular messages must be sent by e-mail and confidential
// messages by post.

// Delivery methods.
type EMail = DeliveryMethodEmail of string
type Post = DeliveryMethodPost of {| RecipientName : string; Address : string |}

Savelenko

// Type classes (a.k.a. traits in Rust or protocols in Swift) are similar to interfaces. Main
// difference: an "implementation" can be provided separately from a type definition itself,
// retroactively. In this example using hypothetical F# syntax we both define TC and their
// implementations next to each other, but this is not required.

trait Equality<'a> with
    equals : 'a -> 'a -> bool
    
// This definition says: "Type 'a belongs to a class (as in classification, characterization)
// of types which support equality. For every such type there is a function 'equals' with the

Savelenko

module Samples

open TypeEquality

(* Generic data needed for all samples. *)

type Identifier = Identifier of int64
type Site = Site of string

// Together

Savelenko

module TransactionalApp where

import Control.Monad.Writer
import Control.Monad.State

{- Model layer -}

data Account = Savings | Normal

deriving instance Eq Account

Savelenko

module FreeMonadPayment where

import Control.Monad.Free
import Control.Monad.Except
import Data.Text hiding (unpack)
import Control.Error
import Data.Function
import Data.Bifunctor
import Control.Newtype (unpack, Newtype)

Savelenko

[<EntryPoint>]
let main argv =
    printfn "Should be zero (netWeight emptyPallet): %A" Stock.shouldBeZero
    printfn "harvesterPartsWeight: %A" Stock.harvesterPartsWeight
    printfn "grossWeight harvesterParts: %A" (Stock.grossWeight Stock.harvesterParts)
    printfn "grossWeight emptyPallet: %A" (Stock.grossWeight Stock.emptyPallet)
    printfn "netWeight harvesterParts: %A" (Stock.netWeight Stock.harvesterParts)
    printfn "value harvesterParts: %A" (Stock.value Stock.harvesterParts)
    printfn "boxLabels harvesterParts: %A" (Stock.boxLabels Stock.harvesterParts)
    printfn "boxLabels emptyPallet: %A" (Stock.boxLabels Stock.emptyPallet)