GenericsExperiment.fs

module GenericsExperiment

/// Generic property interface. Since F# lacks higher kinds,
/// we cannot write code parametric in `P`, so instead write code with casts
/// in terms of an open type `P<'T>`.
type P<'T> =
    interface
    end

/// Implements derivation rules for a certain generic property.
type IRules =

    /// Conjunction.
    abstract And<'A,'B> : P<'A> -> P<'B> -> P<'A * 'B>

    /// Functor (accepting a bijection).
    abstract Map<'A,'B> : ('A -> 'B) -> ('B -> 'A) -> P<'A> -> P<'B>

    /// Unit instance.
    abstract Unit : P<unit>

/// Plumbing combinators. How it works is not important.
[<Sealed>]
type Tool(rules: IRules) =

    member this.Const(x: 'T) : P<'T> =
        rules.Map (fun () -> x) (fun x -> ()) rules.Unit

    member this.Record(x: 'P)(p: P<'P -> 'R>) : P<'R> =
        rules.Map (fun f -> f x) (fun x y -> x) p

    member this.Field(proj: 'R -> 'F)(pf: P<'F>)(par: P<'A->'R>) : P<('F->'A)->'R> =
        rules.Map
            (fun (f, g) h -> g (h f))
            (fun h ->
                let r = h (fun _ -> Unchecked.defaultof<_>)
                (proj r, fun a -> h (fun _ -> a)))
            (rules.And pf par)

    member this.End<'R>() : P<'R->'R> =
        this.Const(fun x -> x)

/// For this style, need a right-associative apply combinator, like Haskell `$`.
let ( @- ) f x = f x

/// Example datatype. Details do not matter.
type Contact =
    {
        Street : string
        Phone : int
    }

    /// Derives any generic property on `Contact`.
    /// Implementation is boilerplate mechanically determined by the structure of `Contact`.
    static member Derive<'T when 'T :> P<Contact>>(rules: IRules, sp: P<string>, ip: P<int>) : 'T =
        let t = Tool rules
        t.Record (fun s p -> { Street = s; Phone = p })
            @- t.Field (fun c -> c.Street) sp
            @- t.Field (fun c -> c.Phone) ip
            @- t.End () :?> _

/// Another example datatype.
type Person =
    {
        Name : string
        Surname : string
        Age : int
        Contact : Contact
    }

    /// Derives any generic property on `Person`.
    /// Implementation is boilerplate mechanically determined by the structure of `Person`.
    static member Derive<'T when 'T :> P<Person>>(rules: IRules, sp: P<string>, ip: P<int>) : 'T =
        let t = Tool rules
        t.Record (fun n s a c -> { Name = n; Surname = s; Age = a; Contact = c })
            @- t.Field (fun p -> p.Name) sp
            @- t.Field (fun p -> p.Surname) sp
            @- t.Field (fun p -> p.Age) ip
            @- t.Field (fun p -> p.Contact)
                (Contact.Derive(rules, sp, ip))
            @- t.End () :?> _

(* Examlpe # 1 of a generic property: writer. *)

[<Sealed>]
type Writer<'T>(write: 'T -> unit) =
    interface P<'T>
    member this.Write(x) = write x

module Writer =

    let (!) (x: P<'T>) : Writer<'T> = x :?> _
    let W (w: Writer<'T>) x = w.Write x

    let And x y = Writer(fun (a, b) -> W x a; stdout.Write(';'); W y b)
    let Map f x = Writer (f >> W x)
    let Unit = Writer ignore

    let S = Writer<string> stdout.Write
    let I = Writer<int> stdout.Write

    let Rules =
        {
            new IRules with
                member this.And x y = And !x !y :> _
                member this.Map f g w = Map g !w :> _
                member this.Unit = Unit :> _
        }

(* Examlpe # 2 of a generic property: generator of random instances. *)

[<Sealed>]
type Generator<'T>(gen: System.Random -> 'T) =
    interface P<'T>
    member this.Generate rand = gen rand

module Generator =

    let (!) (x: P<'T>) : Generator<'T> = x :?> _

    let G (g: Generator<'T>) rand = g.Generate rand
    let And x y = Generator (fun r -> (G x r, G y r))
    let Map f x = Generator (fun r -> f (G x r))
    let Unit = Generator (fun _ -> ())

    let S = Generator (fun r -> string (char (int 'a' + r.Next(0, 25))))
    let I = Generator (fun r -> r.Next(0, 10))

    let Rules =
        {
            new IRules with
                member this.And x y = And !x !y :> _
                member this.Map f g w = Map f !w :> _
                member this.Unit = Unit :> _
        }

/// Putting it all together: the appeal of generic programming is that
/// you define K properties and N datatypes to obtain KN instances.
/// This saves work compared to writing instances manually.
let test () =
    let w : Writer<Person> = Person.Derive(Writer.Rules, Writer.S, Writer.I)
    let g : Generator<Person> = Person.Derive(Generator.Rules, Generator.S, Generator.I)
    let rand = System.Random()
    for i in 1 .. 10 do
        w.Write (g.Generate rand)
        stdout.WriteLine()

GenericsExperiment.v

Axiom I S : Type.

Definition P (t: Type) := t -> S.
Axiom s_concat : S -> S -> S.
Axiom s_empty : S.
Axiom i_to_s : I -> S.

Definition p_and  {a b} (pa: P a) (pb: P b) : P (a * b) :=
  fun ab => s_concat (pa (fst ab)) (pb (snd ab)).

Definition p_map {a b} (f: a -> b) (g: b -> a) (p: P a) : P b :=
  fun x => p (g x).

Definition p_unit : P unit :=
  fun x => s_empty.

Definition pS : P S := fun x => x.
Definition pI : P I := i_to_s.

Definition p_const {a} (x : a) : P a :=
  p_map (fun tt => x) (fun x => tt)  p_unit.

Definition DRP acc r := P (acc -> r).

Definition const {a b} (x: a) (y: b) : a := x.

Axiom U : forall {t}, t.

Definition def {a r} (x: a) (p: DRP a r) : P r :=
  p_map (fun f => f x) const p.

Definition fld {a f r} (proj: r -> f) (pf: P f) (par: DRP a r) : DRP (f -> a) r :=
  p_map
  (fun fg h => (snd fg) (h (fst fg)))
  (fun h => (proj (h (const U)), fun a => h (const a)))
  (p_and pf par).

Definition done {r} : DRP r r :=
  p_const (fun x => x).

Record Person := MkPerson { name: S; sur: S; age: I }.

Definition app {a b} (f: a -> b) (x: a) : b := f x.
Notation "a $ b" := (app a b) (at level 80, right associativity).

Definition test :=
  def MkPerson
  $ fld name pS
  $ fld sur pS
  $ fld age pI
  $ done.

Ltac computed t :=
  let R := fresh "R" in
    let r := eval compute in t in set (R := r).

Definition test_opt : P Person.
Proof. computed test; auto. Defined.

Extraction test.

(*

let test =
  app (def (fun x x0 x1 -> { name = x; sur = x0; age = x1 }))
    (app (fld name pS) (app (fld sur pS) (app (fld age pI) done0)))

*)

Extraction test_opt.

(*

let test_opt x =
  s_concat x.name (s_concat x.sur (s_concat (i_to_s x.age) s_empty))

*)

The relevant blogpost is not displaying this gist.