Savelenko

module Bounded =

    type IBound =
        static abstract Bound : int

    type Bounded = private Bounded of int // Abstract data type

    let bounded<'bound when 'bound :> IBound> (value : int) : Option<Bounded> =
        if value <= 'bound.Bound then Some (Bounded value) else None

Savelenko

module Handler

open System.Threading.Tasks
open Giraffe
open Giraffe.FormatExpressions
open Microsoft.AspNetCore.Http
open Microsoft.Extensions.Logging

(* Core definitions *)

Savelenko

type Pete<'T> (wrapped : 'T) =

  member this.Bind (binder : 'T -> Pete<'U>) : Pete<'U> =
    binder wrapped

Savelenko

module VehicleMaintenance

open TypeEquality // See my other gists for this module

(*
A vehicle shop can perform certain maintenance procedures on cars and bicycles. Every maintenance procedure has a price.
For bicycles prices are fixed. For cars the price may depend on engine capacity.
*)

// Vehicles and prices

Savelenko

(*
An exercise in modeling. Users can be verified or banned. A user can be banned only if their username is "offensive".

We assume the Onion architecture. Modules `User` and `Verification` belong to the model. Module `UserVerification`
belongs to the application layer. Data access layer is omitted completely; it should be fairly trivial.

Note that the verified/banned aspect of a user is modeled "externally" to the notion of user itself. In particular,
there are no "aggregates" below which combine all aspects of a user.
*)

Savelenko

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

Savelenko

newtype Money currency = Money Number -- Constructor is not exported

sumMoney :: forall currency. Money currency -> Money currency -> Money currency
sumMoney (Money a) (Money b) = Money (a `add` b)

infixl 6 sumMoney as +

multiplyMoney :: forall currency. Number -> Money currency -> Money currency
multiplyMoney multiplier (Money a) = Money (multiplier `mul` a)

Savelenko

type IEncodable<'t> =
    static abstract Encode : 't -> byte[]

/// Selects Base64 encoding for `a`.
type Base64<'a when 'a :> IEncodable<'a>> = Base64 of 'a with
    
    interface IEncodable<Base64<'a>> with
        member this.Encode (Base64 a) =
            let toBase64 = failwith "..."
            toBase64 ('a.Encode a)

Savelenko

(*
The original applicative validation type is defined like this in FsToolkit.ErrorHandling:
*)

/// Validation<'a, 'err> is defined as Result<'a, 'err list> meaning you can use many of the functions found in the
/// Result module.
type Validation<'ok, 'error> = Result<'ok, List<'error>>

(*
We can abstract the `List` away by requiring any structure which supports concatenation, of which the list's (@) is an

Savelenko

module Facility

/// A facility which admits visitors (or does it?).
type Facility =
    | BlackMesa
    | DeathStar
    | TeaHouse

(*