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<int> * Expr<int> * Eq<'a, int>
    | IfThenElse of Expr<bool> * 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<Id, 'a>, _ : 'a) = ()
    // helper functions
    static member To (eq : Eq<'a, 'b>) (x : 'a) = eq.To<Id>(HKT.pack x) |> HKT.unpack
    static member From (eq : Eq<'a, 'b>) (x : 'b) = eq.From<Id>(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<Thunk, 'a>, _ : unit -> 'a) = ()

    static member To (eq : Eq<'a, 'b>) (x : unit -> 'a) = eq.To<Thunk>(HKT.pack x) |> HKT.unpack
    static member From (eq : Eq<'a, 'b>) (x : unit -> 'b) = eq.From<Thunk>(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>

Full name: Script.Expr.add
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
Raw view Test code New version

More information

Link:http://fssnip.net/7Xa
Posted:4 years ago
Author:Eirik Tsarpalis
Tags: generic programming