F# version of John Hughes talk https://youtu.be/zvRAyq5wj38

pbt.fsx

#r "nuget:FsCheck"

open System
open FsCheck

module JohnHughes =
    // F# version of John Hughes talk https://youtu.be/zvRAyq5wj38
    
    type BST<'k, 'v when 'k : comparison>  =
        | Leaf
        | Branch of BST<'k,'v> * ('k * 'v) * BST<'k,'v>
    
    type Find<'k, 'v when 'k : comparison> = 'k -> BST<'k, 'v> -> 'v option
    
    type Nil<'k, 'v when 'k : comparison> = BST<'k, 'v>
    
    type Insert<'k, 'v when 'k : comparison> = 'k -> 'v -> BST<'k, 'v> -> BST<'k, 'v>
    
    type Delete<'k, 'v when 'k : comparison> = 'k -> BST<'k, 'v> -> BST<'k, 'v>
    
    type Union<'k, 'v when 'k : comparison> = BST<'k, 'v> -> BST<'k, 'v> -> BST<'k, 'v>
    
    type ToList<'k, 'v when 'k : comparison> = BST<'k, 'v> -> ('k * 'v) list
    
    type Keys<'k, 'v when 'k : comparison> = BST<'k, 'v> -> 'k list
    
    let nil<'k, 'v when 'k : comparison> = BST<'k,'v>.Leaf

    let rec foldBst fLeaf fBranch acc tree : 'r =
        let recurse = foldBst fLeaf fBranch
        
        match tree with
        | Leaf ->
            fLeaf acc
        | Branch (left, kv, right) ->
            let newAcc = fBranch acc kv
            recurse (recurse newAcc left) right
     
    let rec foldBackBst fLeaf fBranch tree generator : 'r =
        let recurse = foldBackBst fLeaf fBranch
        
        match tree with
        | Leaf ->
            fLeaf () |> generator
        | Branch (left, kv, right) ->
            recurse left (fun innerLeft ->
                recurse right (fun innerRight ->
                        fBranch innerLeft kv innerRight |> generator
                    )
                )
    
    let toListFold tree =
        let fLeaf () = []
        
        let fBranch innerLeft kv innerRight =
            innerLeft @ [kv] @ innerRight
        
        foldBackBst fLeaf fBranch tree id
    
    let insertOrder tree =
        let fLeaf acc =
            acc
        
        let fBranch acc kv =
            kv :: acc
        
        foldBst fLeaf fBranch [] tree |> List.rev
    
    let insert k v t =
        let rec loop k v generator t : 'r =
            let recurse = loop k v
            
            match t with
            | Leaf ->
                generator (Branch (Leaf, (k, v), Leaf))
            | Branch (left, (k',_), right) when k = k' ->
                generator (Branch (left, (k', v), right))
                
            | Branch (left, (k',v'), right) when k < k' ->
                let newGenerator innerLeft =
                    generator (Branch (innerLeft, (k', v'), right))
                
                recurse newGenerator left
            | Branch (left, (k',v'), right) when k > k' ->
                let newGenerator innerRight =
                    generator (Branch (left, (k', v'), innerRight))
                
                recurse newGenerator right
            | _ -> generator t
        
        loop k v id t
     
    let rec cataBst fLeaf fBranch tree : 'r =
        let recurse = cataBst fLeaf fBranch
        
        match tree with
        | Leaf -> fLeaf ()
        | Branch (left, kv, right) ->
            let left = recurse left
            let right = recurse right
            
            fBranch (left, kv, right)
    
    let deeplyNestedTree depth =
        let rec loop depth treeSoFar =
            match depth with
            | 0 -> treeSoFar
            | n -> loop (n - 1) (insert n 1 treeSoFar )
        
        loop depth Leaf
    
    let sumValue tree =
        let fLeaf () = 0
        
        let fBranch innerLeft (k, v) innerRight =
            innerLeft + v + innerRight
        
        foldBackBst fLeaf fBranch tree id
    
    let find k tree =
        let fLeaf () = None
        
        let fBranch (left, (k', v), right) =
            match left, right with
            | None, None ->
                if k = k'
                then Some v
                else None
            | Some v, _ -> Some v
            | _, Some v -> Some v
        
        cataBst fLeaf fBranch tree
    
    let delete k tree =
        let fLeaf () = Leaf
        
        let fBranch (left, (k', v), right) =
            if k = k'
            then Leaf
            else Branch (left, (k', v), right)
    
        cataBst fLeaf fBranch tree
    
    let toListCata tree =
        let fLeaf () = []
        
        let fBranch (left, kv, right) =
            left @ [kv] @ right
        
        cataBst fLeaf fBranch tree
    
    let union t t' =
        t
        |> toListCata
        |> List.fold (fun s (k,v) -> insert k v s) t'
    
    let keys tree =
        tree
        |> toListCata
        |> List.map fst

module JohnHughesProperties =
    open JohnHughes
    let uncurry f (x, y) = f x y
    
    let rec valid t =
        match t with
        | Leaf -> true
        | Branch (left, (k, _), right) ->
            valid left &&
            valid right &&
            keys left |> List.forall (fun k' -> k' < k) &&
            keys right |> List.forall (fun k' -> k' > k)
    
    let tree<'k, 'v when 'k : comparison> =
        Arb.generate<('k*'v) list>
        |> Gen.map (fun kvs -> List.foldBack (uncurry insert) kvs nil)
    
    let shrink t =
        Arb.Default.Derive().Shrinker t
        |> Seq.filter valid
  
    type MyGenerators =
        static member Tree() =
            {new Arbitrary<BST<'k, 'v>>() with
                override x.Generator = tree<'k, 'v>
                override x.Shrinker t = shrink t
                }
    
    let (===) left right = left = right |@ $"%A{left} != %A{right}"
    
    let (=~=) left right = toListCata left === toListCata right
    
    // 1. Is there an invariant?
    
    type Properties =
        static member ``FsCheck Generator produces valid trees`` (t: BST<int32, int32>) =
            valid t
        
        static member ``FsCheck Shrink produces valid trees`` (t: BST<int32, int32>) =
            valid t ==> (shrink t |> Seq.forall valid)
        
        static member ``Nil is valid`` () =
            valid nil
        
        static member ``Inserting produces a valid tree`` k v (t: BST<int32, int32>) =
            valid (insert k v t)
        
        static member ``Deleting produces a valid tree`` k (t: BST<int32, int32>) =
            valid (delete k t)
        
        static member ``Union of two trees is valid`` (t: BST<int32, int32>) (t': BST<int32, int32>) =
            valid (union t t')
        
        // 2. What are the post conditions
        static member ``Value is findable after inserting`` k v (t: BST<int32, int32>) k' =
            let findResult = find k' (insert k v t)
            let expectResult = if k = k' then Some v else find k' t
            
            findResult === expectResult
    
        static member ``Finds a value when present`` k v (t: BST<int32, int32>) =
            find k (insert k v t) = Some v
        
        static member ``Does not find a value when not present`` k (t: BST<int32, int32>) =
            find k (delete k t) = None
        
        // 3. Metamorphic properties
        static member ``Insert is associative`` (k, v) (k', v') (t: BST<int32, int32>) =
            insert k v (insert k' v' t) =~= if k = k' then insert k v t else insert k' v' (insert k v t)
        
        // 4. Inductive properties
        static member ``Union with nil`` (t: BST<int32, int32>) =
            union nil t === t
        
        static member ``Union insert`` (t: BST<int32, int32>) (t': BST<int32, int32>) (k, v) =
            union (insert k v t) t' =~= insert k v (union t t')
        
        // 5. Model based properties
        static member ``Insert using model testing`` (k, v) (t: BST<int32, int32>) =
            let deleteKey k list =
                list |> List.filter (fun (k', _) -> k <> k')
                
            List.sort (toListCata (insert k v t)) === List.sort ((k,v) :: (deleteKey k (toListCata t)))
    
    Check.All<Properties>({Config.Quick with Arbitrary = [ typeof<MyGenerators> ]; MaxTest = 100})
    
    let inserts = [
        5, 5
        9, 9
        3, 3
        4, 4
        6, 6
        8, 8
        10, 10
        1, 1
        7, 7
    ]
    
    let myBst = inserts |> List.fold (fun s (k,v) -> insert k v s) nil

    let noFour = myBst |> delete 4
    
    let withZero = myBst |> insert 0 0
    
    let join<'a> (strs: 'a list) =
        String.Join (", ", strs)
    
    printfn $"{myBst |> toListFold |> List.map snd |> join}"
    
    printfn $"{noFour |> toListFold |> List.map snd |> join}"
    
    printfn $"{withZero |> toListFold |> List.map snd |> join}"
    
    printfn $"{union noFour withZero |> toListFold |> List.map snd |> join}"
    
    printfn $"{nil |> insert 0 0 |> insert 0 0 |> insert 0 0 |> toListFold |> List.map fst |> join}"
    
    printfn $"{myBst |> find 3}"
    
    printfn $"Insert Order: {myBst |> insertOrder |> List.map fst |> join}"
    
    myBst
    |> (fun bst -> bst |> Arb.shrink)
    |> fun bsts -> printfn $"Before filter: {Seq.length bsts}"; bsts
    |> Seq.filter valid
    |> fun bsts -> printfn $"After filter: {Seq.length bsts}"; bsts