6 people like it.

Fully Type-Safe Generic Programs

Proof of concept combining HKT encodings à la Higher and object algebras to create a fully type-safe, performant and extensible apparatus for writing generic programs in F#

HKT Encoding

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
// Higher-style HKT encoding, c.f. https://github.com/palladin/Higher

type App<'F, 't> = App of 'F * obj
type App<'F, 't1, 't2> = App<App<'F, 't1>, 't2> 
    
/// Arrow HKT encoding
type Hom private () =
    static let w = new Hom()
    static member Pack(value : 'a -> 'b) : App<Hom, 'a, 'b> = App(App(w, value), null)
    static member Unpack(App(App(_,value),_) : App<Hom, 'a, 'b>) : 'a -> 'b = value :?> _
    
/// Used for flipping arguments to HKTs
type Flip<'F> private () =
    static let w = new Flip<'F>()
    static member Pack(value : App<'F, 'a, 'b>) : App<Flip<'F>, 'b, 'a> = App(App(w, value), null)
    static member Unpack(App(App(_,value),_) : App<Flip<'F>, 'b, 'a>) : App<'F, 'a, 'b> = value :?> _

Defining a Type Algebra

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
// c.f. http://fssnip.net/7Sx/title/Extensibility-for-the-Masses

type TypeAlg<'F> =
    abstract Int : App<'F, int>
    abstract Bool : App<'F, bool>
    abstract Tuple : App<'F, 't1> -> App<'F, 't2> -> App<'F, 't1 * 't2> 
    abstract List : App<'F, 't> -> App<'F, 't list>
    abstract Option : App<'F, 't> -> App<'F, 't option>

// defining types as church encodings
type TypeExpr<'F, 't> = TypeAlg<'F> -> App<'F, 't>

let int : TypeExpr<_, _> = fun alg -> alg.Int
let bool : TypeExpr<_, _> = fun alg -> alg.Bool
let tuple t1 t2 : TypeExpr<_,_> = fun alg -> alg.Tuple (t1 alg) (t2 alg)
let list ts : TypeExpr<_,_> = fun alg -> alg.List (ts alg)
let option topt : TypeExpr<_,_> = fun alg -> alg.Option (topt alg)

// church encoding of (int option * (int * bool) list)
let test () = tuple (option int) (list (tuple int bool))

Example, Defining a Generic PrettyPrinter

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
type PrettyPrinter = App<Flip<Hom>, string> // Hom(_,string)

module PrettyP =
    let pack (f : 't -> string) : App<PrettyPrinter, 't> = f |> Hom.Pack |> Flip.Pack
    let unpack (f : App<PrettyPrinter, 't>) : 't -> string = f |> Flip.Unpack |> Hom.Unpack
    
type PrettyPrinterAlg() =
    interface TypeAlg<PrettyPrinter> with
        member __.Bool = PrettyP.pack (function true -> "true" | false -> "false")
        member __.Int = PrettyP.pack (fun i -> i.ToString())
        member __.Tuple f1 f2 =
            let f1 = PrettyP.unpack f1
            let f2 = PrettyP.unpack f2
            PrettyP.pack (fun (t1,t2) -> sprintf "(%s, %s)" (f1 t1) (f2 t2))
            
        member __.List f =
            let f = PrettyP.unpack f
            PrettyP.pack (fun ts -> ts |> Seq.map f |> String.concat "; " |> sprintf "[%s]")

        member __.Option f =
            let f = PrettyP.unpack f
            PrettyP.pack (function None -> "None" | Some s -> sprintf "Some(%s)" (f s))
            
let eval (expr : TypeExpr<_,_>) : 't -> string = expr (new PrettyPrinterAlg()) |> PrettyP.unpack

Tests

1: 
2: 
3: 
4: 
5: 
6: 
7: 
let p1 = eval (tuple int bool)

p1 (42, false)

let p2 = eval (list (option int))

p2 ([Some 42; None])
Multiple items
union case App.App: 'F * obj -> App<'F,'t>

--------------------
type App<'F,'t> = | App of 'F * obj

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

Full name: Microsoft.FSharp.Core.obj
Multiple items
type Hom =
  private new : unit -> Hom
  static member Pack : value:('a -> 'b) -> App<Hom,'a,'b>
  static member Unpack : App<Hom,'a,'b> -> ('a -> 'b)

Full name: Script.Hom


 Arrow HKT encoding


--------------------
private new : unit -> Hom
val w : Hom
static member Hom.Pack : value:('a -> 'b) -> App<Hom,'a,'b>

Full name: Script.Hom.Pack
val value : ('a -> 'b)
static member Hom.Unpack : App<Hom,'a,'b> -> ('a -> 'b)

Full name: Script.Hom.Unpack
val value : obj
Multiple items
type Flip<'F> =
  private new : unit -> Flip<'F>
  static member Pack : value:App<'F,'a,'b> -> App<Flip<'F>,'b,'a>
  static member Unpack : App<Flip<'F>,'b,'a> -> App<'F,'a,'b>

Full name: Script.Flip<_>


 Used for flipping arguments to HKTs


--------------------
private new : unit -> Flip<'F>
val w : Flip<'F>
static member Flip.Pack : value:App<'F,'a,'b> -> App<Flip<'F>,'b,'a>

Full name: Script.Flip`1.Pack
val value : App<'F,'a,'b>
static member Flip.Unpack : App<Flip<'F>,'b,'a> -> App<'F,'a,'b>

Full name: Script.Flip`1.Unpack
type TypeAlg<'F> =
  interface
    abstract member List : App<'F,'t> -> App<'F,'t list>
    abstract member Option : App<'F,'t> -> App<'F,'t option>
    abstract member Tuple : App<'F,'t1> -> App<'F,'t2> -> App<'F,('t1 * 't2)>
    abstract member Bool : App<'F,bool>
    abstract member Int : App<'F,int>
  end

Full name: Script.TypeAlg<_>
abstract member TypeAlg.Int : App<'F,int>

Full name: Script.TypeAlg`1.Int
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<_>
abstract member TypeAlg.Bool : App<'F,bool>

Full name: Script.TypeAlg`1.Bool
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
abstract member TypeAlg.Tuple : App<'F,'t1> -> App<'F,'t2> -> App<'F,('t1 * 't2)>

Full name: Script.TypeAlg`1.Tuple
Multiple items
abstract member TypeAlg.List : App<'F,'t> -> App<'F,'t list>

Full name: Script.TypeAlg`1.List

--------------------
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
  interface IEnumerable
  interface IEnumerable<'T>
  member GetSlice : startIndex:int option * endIndex:int option -> 'T list
  member Head : 'T
  member IsEmpty : bool
  member Item : index:int -> 'T with get
  member Length : int
  member Tail : 'T list
  static member Cons : head:'T * tail:'T list -> 'T list
  static member Empty : 'T list

Full name: Microsoft.FSharp.Collections.List<_>
type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>
Multiple items
abstract member TypeAlg.Option : App<'F,'t> -> App<'F,'t option>

Full name: Script.TypeAlg`1.Option

--------------------
module Option

from Microsoft.FSharp.Core
type 'T option = Option<'T>

Full name: Microsoft.FSharp.Core.option<_>
type TypeExpr<'F,'t> = TypeAlg<'F> -> App<'F,'t>

Full name: Script.TypeExpr<_,_>
Multiple items
val int : alg:TypeAlg<'a> -> App<'a,int>

Full name: Script.int

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

Full name: Microsoft.FSharp.Core.int

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

Full name: Microsoft.FSharp.Core.int<_>
val alg : TypeAlg<'a>
property TypeAlg.Int: App<'a,int>
Multiple items
val bool : alg:TypeAlg<'a> -> App<'a,bool>

Full name: Script.bool

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

Full name: Microsoft.FSharp.Core.bool
property TypeAlg.Bool: App<'a,bool>
val tuple : t1:(TypeAlg<'a> -> App<'a,'b>) -> t2:(TypeAlg<'a> -> App<'a,'c>) -> alg:TypeAlg<'a> -> App<'a,('b * 'c)>

Full name: Script.tuple
val t1 : (TypeAlg<'a> -> App<'a,'b>)
val t2 : (TypeAlg<'a> -> App<'a,'c>)
abstract member TypeAlg.Tuple : App<'F,'t1> -> App<'F,'t2> -> App<'F,('t1 * 't2)>
Multiple items
val list : ts:(TypeAlg<'a> -> App<'a,'b>) -> alg:TypeAlg<'a> -> App<'a,'b list>

Full name: Script.list

--------------------
type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>
val ts : (TypeAlg<'a> -> App<'a,'b>)
abstract member TypeAlg.List : App<'F,'t> -> App<'F,'t list>
Multiple items
val option : topt:(TypeAlg<'a> -> App<'a,'b>) -> alg:TypeAlg<'a> -> App<'a,'b option>

Full name: Script.option

--------------------
type 'T option = Option<'T>

Full name: Microsoft.FSharp.Core.option<_>
val topt : (TypeAlg<'a> -> App<'a,'b>)
abstract member TypeAlg.Option : App<'F,'t> -> App<'F,'t option>
val test : unit -> (TypeAlg<'a> -> App<'a,(int option * (int * bool) list)>)

Full name: Script.test
type PrettyPrinter = App<Flip<Hom>,string>

Full name: Script.PrettyPrinter
type Flip<'F> =
  private new : unit -> Flip<'F>
  static member Pack : value:App<'F,'a,'b> -> App<Flip<'F>,'b,'a>
  static member Unpack : App<Flip<'F>,'b,'a> -> App<'F,'a,'b>

Full name: Script.Flip<_>


 Used for flipping arguments to HKTs
type Hom =
  private new : unit -> Hom
  static member Pack : value:('a -> 'b) -> App<Hom,'a,'b>
  static member Unpack : App<Hom,'a,'b> -> ('a -> 'b)

Full name: Script.Hom


 Arrow HKT encoding
Multiple items
val string : value:'T -> string

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

--------------------
type string = System.String

Full name: Microsoft.FSharp.Core.string
val pack : f:('t -> string) -> App<PrettyPrinter,'t>

Full name: Script.PrettyP.pack
val f : ('t -> string)
static member Hom.Pack : value:('a -> 'b) -> App<Hom,'a,'b>
static member Flip.Pack : value:App<'F,'a,'b> -> App<Flip<'F>,'b,'a>
val unpack : f:App<PrettyPrinter,'t> -> ('t -> string)

Full name: Script.PrettyP.unpack
val f : App<PrettyPrinter,'t>
static member Flip.Unpack : App<Flip<'F>,'b,'a> -> App<'F,'a,'b>
static member Hom.Unpack : App<Hom,'a,'b> -> ('a -> 'b)
Multiple items
type PrettyPrinterAlg =
  interface TypeAlg<PrettyPrinter>
  new : unit -> PrettyPrinterAlg

Full name: Script.PrettyPrinterAlg

--------------------
new : unit -> PrettyPrinterAlg
override PrettyPrinterAlg.Bool : App<PrettyPrinter,bool>

Full name: Script.PrettyPrinterAlg.Bool
module PrettyP

from Script
val __ : PrettyPrinterAlg
override PrettyPrinterAlg.Int : App<PrettyPrinter,int>

Full name: Script.PrettyPrinterAlg.Int
val i : int
System.Int32.ToString() : string
System.Int32.ToString(provider: System.IFormatProvider) : string
System.Int32.ToString(format: string) : string
System.Int32.ToString(format: string, provider: System.IFormatProvider) : string
override PrettyPrinterAlg.Tuple : f1:App<PrettyPrinter,'c> -> f2:App<PrettyPrinter,'d> -> App<PrettyPrinter,('c * 'd)>

Full name: Script.PrettyPrinterAlg.Tuple
val f1 : App<PrettyPrinter,'c>
val f2 : App<PrettyPrinter,'d>
val f1 : ('c -> string)
val f2 : ('d -> string)
val t1 : 'c
val t2 : 'd
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
Multiple items
override PrettyPrinterAlg.List : f:App<PrettyPrinter,'b> -> App<PrettyPrinter,'b list>

Full name: Script.PrettyPrinterAlg.List

--------------------
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
  interface IEnumerable
  interface IEnumerable<'T>
  member GetSlice : startIndex:int option * endIndex:int option -> 'T list
  member Head : 'T
  member IsEmpty : bool
  member Item : index:int -> 'T with get
  member Length : int
  member Tail : 'T list
  static member Cons : head:'T * tail:'T list -> 'T list
  static member Empty : 'T list

Full name: Microsoft.FSharp.Collections.List<_>
val f : App<PrettyPrinter,'b>
val f : ('b -> string)
val ts : 'b list
module Seq

from Microsoft.FSharp.Collections
val map : mapping:('T -> 'U) -> source:seq<'T> -> seq<'U>

Full name: Microsoft.FSharp.Collections.Seq.map
module String

from Microsoft.FSharp.Core
val concat : sep:string -> strings:seq<string> -> string

Full name: Microsoft.FSharp.Core.String.concat
Multiple items
override PrettyPrinterAlg.Option : f:App<PrettyPrinter,'a> -> App<PrettyPrinter,'a option>

Full name: Script.PrettyPrinterAlg.Option

--------------------
module Option

from Microsoft.FSharp.Core
val f : App<PrettyPrinter,'a>
val f : ('a -> string)
union case Option.None: Option<'T>
union case Option.Some: Value: 'T -> Option<'T>
val s : 'a
val eval : expr:TypeExpr<PrettyPrinter,'t> -> ('t -> string)

Full name: Script.eval
val expr : TypeExpr<PrettyPrinter,'t>
val p1 : (int * bool -> string)

Full name: Script.p1
val p2 : (int option list -> string)

Full name: Script.p2
Raw view New version

More information

Link:http://fssnip.net/7Wp
Posted:2 months ago
Author:Eirik Tsarpalis
Tags: generic programming , object algebra , higher-kinded types