3 people like it.

# Generic programming with Leibniz Equality

Uses Leibniz equality to generalize an example presented in https://skillsmatter.com/skillscasts/14430-f-sharpunctional-londoners-september

## HKT encoding

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: ``` ``````type App<'F, 't> = private App of payload : obj module HKT = let inline pack (value : 'Fa) : App<'F, 'a> when 'F : (static member Assign : App<'F, 'a> * 'Fa -> unit) = App value let inline unpack (App value : App<'F, 'a>) : 'Fa when 'F : (static member Assign : App<'F, 'a> * 'Fa -> unit) = value :?> _ let inline (|Unpack|) app = unpack app ``````

## Leibniz Equality

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: ``` ``````// Leibniz equality c.f. http://okmij.org/ftp/Computation/extra-polymorphism.html?new#injectivity // NB `To` implies `From`, proof omitted for brevity type Eq<'a,'b> = abstract To<'F> : App<'F, 'a> -> App<'F, 'b> abstract From<'F> : App<'F, 'b> -> App<'F, 'a> module Eq = // Equivalence axioms let refl<'a> = { new Eq<'a, 'a> with member __.To x = x member __.From x = x } let sym (eq : Eq<'a,'b>) = { new Eq<'b, 'a> with member __.To x = eq.From x member __.From x = eq.To x } let trans (eq : Eq<'a, 'b>) (eq' : Eq<'b, 'c>) = { new Eq<'a, 'c> with member __.To x = eq'.To(eq.To(x)) member __.From x = eq.From(eq'.From(x)) } ``````

## Typed Expressions

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: ``` ``````type Expr<'a> = | Bool of bool * Eq<'a, bool> | Int of int * Eq<'a, int> | Add of Expr * Expr * Eq<'a, int> | IfThenElse of Expr * Expr<'a> * Expr<'a> module Expr = let bool b = Bool(b, Eq.refl) let int i = Int(i , Eq.refl) let add x y = Add(x, y, Eq.refl) let ifThenElse b x y = IfThenElse(b, x, y) let testExpr = Expr.ifThenElse (Expr.bool true) (Expr.add (Expr.int 10) (Expr.int 32)) (Expr.int -2) ``````

## Simple Evaluator

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: ``` ``````// Identity functor encoding type Id = static member Assign(_ : App, _ : 'a) = () // helper functions static member To (eq : Eq<'a, 'b>) (x : 'a) = eq.To(HKT.pack x) |> HKT.unpack static member From (eq : Eq<'a, 'b>) (x : 'b) = eq.From(HKT.pack x) |> HKT.unpack let rec eval<'t> (e : Expr<'t>) : 't = match e with | Bool(b, eq) -> Id.From eq b | Int (i, eq) -> Id.From eq i | Add (x, y, eq) -> Id.From eq (eval x + eval y) | IfThenElse(b, x, y) -> if eval b then eval x else eval y eval testExpr ``````

## Evaluating to thunks

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: ``` ``````type Thunk = static member Assign(_ : App, _ : unit -> 'a) = () static member To (eq : Eq<'a, 'b>) (x : unit -> 'a) = eq.To(HKT.pack x) |> HKT.unpack static member From (eq : Eq<'a, 'b>) (x : unit -> 'b) = eq.From(HKT.pack x) |> HKT.unpack let rec toThunk<'t> (e : Expr<'t>) : (unit -> 't) = match e with | Bool (b, eq) -> Thunk.From eq (fun () -> b) | Int (i, eq) -> Thunk.From eq (fun () -> i) | Add (x, y, eq) -> let xt = toThunk x let yt = toThunk y Thunk.From eq (fun () -> xt () + yt ()) | IfThenElse (b,x,y) -> let bt = toThunk b let xt = toThunk x let yt = toThunk y (fun () -> if bt() then xt() else yt()) // interpret once let f = toThunk testExpr // evaluate many times without interpretation costs [ for i in 1 .. 100 -> f () ] ``````
Multiple items
union case App.App: payload: obj -> App<'F,'t>

--------------------
type App<'F,'t> = private | App of payload: obj

Full name: Script.App<_,_>
type obj = System.Object

Full name: Microsoft.FSharp.Core.obj
val pack : value:'Fa -> App<'F,'a> (requires member Assign)

Full name: Script.HKT.pack
val value : 'Fa
type unit = Unit

Full name: Microsoft.FSharp.Core.unit
val unpack : App<'F,'a> -> 'Fa (requires member Assign)

Full name: Script.HKT.unpack
val value : obj
val app : App<'a,'b> (requires member Assign)
type Eq<'a,'b> =
interface
abstract member From : App<'F,'b> -> App<'F,'a>
abstract member To : App<'F,'a> -> App<'F,'b>
end

Full name: Script.Eq<_,_>
abstract member Eq.To : App<'F,'a> -> App<'F,'b>

Full name: Script.Eq`2.To
abstract member Eq.From : App<'F,'b> -> App<'F,'a>

Full name: Script.Eq`2.From
val refl<'a> : Eq<'a,'a>

Full name: Script.Eq.refl
abstract member Eq.To : App<'F,'a> -> App<'F,'b>
val x : App<'b,'a>
val __ : Eq<'a,'a>
abstract member Eq.From : App<'F,'b> -> App<'F,'a>
val sym : eq:Eq<'a,'b> -> Eq<'b,'a>

Full name: Script.Eq.sym
val eq : Eq<'a,'b>
val x : App<'c,'b>
val __ : Eq<'b,'a>
val x : App<'c,'a>
val trans : eq:Eq<'a,'b> -> eq':Eq<'b,'c> -> Eq<'a,'c>

Full name: Script.Eq.trans
val eq' : Eq<'b,'c>
val x : App<'d,'a>
val __ : Eq<'a,'c>
val x : App<'d,'c>
type Expr<'a> =
| Bool of bool * Eq<'a,bool>
| Int of int * Eq<'a,int>
| Add of Expr<int> * Expr<int> * Eq<'a,int>
| IfThenElse of Expr<bool> * Expr<'a> * Expr<'a>

Full name: Script.Expr<_>
union case Expr.Bool: bool * Eq<'a,bool> -> Expr<'a>
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
Multiple items
module Eq

from Script

--------------------
type Eq<'a,'b> =
interface
abstract member From : App<'F,'b> -> App<'F,'a>
abstract member To : App<'F,'a> -> App<'F,'b>
end

Full name: Script.Eq<_,_>
union case Expr.Int: int * Eq<'a,int> -> Expr<'a>
Multiple items
val int : value:'T -> int (requires member op_Explicit)

Full name: Microsoft.FSharp.Core.Operators.int

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
union case Expr.Add: Expr<int> * Expr<int> * Eq<'a,int> -> Expr<'a>
union case Expr.IfThenElse: Expr<bool> * Expr<'a> * Expr<'a> -> Expr<'a>
Multiple items
val bool : b:bool -> Expr<bool>

Full name: Script.Expr.bool

--------------------
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
val b : bool
Multiple items
val int : i:int -> Expr<int>

Full name: Script.Expr.int

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
val i : int
val add : x:Expr<int> -> y:Expr<int> -> Expr<int>

val x : Expr<int>
val y : Expr<int>
val ifThenElse : b:Expr<bool> -> x:Expr<'a> -> y:Expr<'a> -> Expr<'a>

Full name: Script.Expr.ifThenElse
val b : Expr<bool>
val x : Expr<'a>
val y : Expr<'a>
val testExpr : Expr<int>

Full name: Script.testExpr
Multiple items
module Expr

from Script

--------------------
type Expr<'a> =
| Bool of bool * Eq<'a,bool>
| Int of int * Eq<'a,int>
| Add of Expr<int> * Expr<int> * Eq<'a,int>
| IfThenElse of Expr<bool> * Expr<'a> * Expr<'a>

Full name: Script.Expr<_>
val bool : b:bool -> Expr<bool>

Full name: Script.Expr.bool
val int : i:int -> Expr<int>

Full name: Script.Expr.int
type Id =
static member Assign : App<Id,'a> * 'a -> unit
static member From : eq:Eq<'a,'b> -> x:'b -> 'a
static member To : eq:Eq<'a,'b> -> x:'a -> 'b

Full name: Script.Id
static member Id.Assign : App<Id,'a> * 'a -> unit

Full name: Script.Id.Assign
static member Id.To : eq:Eq<'a,'b> -> x:'a -> 'b

Full name: Script.Id.To
val x : 'a
module HKT

from Script
static member Id.From : eq:Eq<'a,'b> -> x:'b -> 'a

Full name: Script.Id.From
val x : 'b
val eval : e:Expr<'t> -> 't

Full name: Script.eval
val e : Expr<'t>
val eq : Eq<'t,bool>
static member Id.From : eq:Eq<'a,'b> -> x:'b -> 'a
val eq : Eq<'t,int>
val x : Expr<'t>
val y : Expr<'t>
type Thunk =
static member Assign : App<Thunk,'a> * (unit -> 'a) -> unit
static member From : eq:Eq<'a,'b> -> x:(unit -> 'b) -> (unit -> 'a)
static member To : eq:Eq<'a,'b> -> x:(unit -> 'a) -> (unit -> 'b)

Full name: Script.Thunk
static member Thunk.Assign : App<Thunk,'a> * (unit -> 'a) -> unit

Full name: Script.Thunk.Assign
static member Thunk.To : eq:Eq<'a,'b> -> x:(unit -> 'a) -> (unit -> 'b)

Full name: Script.Thunk.To
val x : (unit -> 'a)
static member Thunk.From : eq:Eq<'a,'b> -> x:(unit -> 'b) -> (unit -> 'a)

Full name: Script.Thunk.From
val x : (unit -> 'b)
val toThunk : e:Expr<'t> -> (unit -> 't)

Full name: Script.toThunk
static member Thunk.From : eq:Eq<'a,'b> -> x:(unit -> 'b) -> (unit -> 'a)
val xt : (unit -> int)
val yt : (unit -> int)
val bt : (unit -> bool)
val xt : (unit -> 't)
val yt : (unit -> 't)
val f : (unit -> int)

Full name: Script.f