0 people like it.

Staged HOAS

Staged Higher-order abstract syntax via GADT encoding.

  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: 
 27: 
 28: 
 29: 
 30: 
 31: 
 32: 
 33: 
 34: 
 35: 
 36: 
 37: 
 38: 
 39: 
 40: 
 41: 
 42: 
 43: 
 44: 
 45: 
 46: 
 47: 
 48: 
 49: 
 50: 
 51: 
 52: 
 53: 
 54: 
 55: 
 56: 
 57: 
 58: 
 59: 
 60: 
 61: 
 62: 
 63: 
 64: 
 65: 
 66: 
 67: 
 68: 
 69: 
 70: 
 71: 
 72: 
 73: 
 74: 
 75: 
 76: 
 77: 
 78: 
 79: 
 80: 
 81: 
 82: 
 83: 
 84: 
 85: 
 86: 
 87: 
 88: 
 89: 
 90: 
 91: 
 92: 
 93: 
 94: 
 95: 
 96: 
 97: 
 98: 
 99: 
100: 
101: 
102: 
103: 
104: 
105: 
106: 
107: 
108: 
109: 
110: 
111: 
// Staged Higher-order abstract syntax via GADT encoding

#r "packages/FSharp.Compiler.Service.1.3.1.0/lib/net45/FSharp.Compiler.Service.dll"
#r "packages/QuotationCompiler.0.0.7-alpha/lib/net45/QuotationCompiler.dll"

open System
open QuotationCompiler
open Microsoft.FSharp.Quotations

// helper functions
let counter = ref 0
let rec generateVars (types : Type list) : Var list = 
    match types with 
    | [] -> []
    | t :: ts -> 
        incr counter
        let var = new Var(sprintf "__paramTemp_%d__" !counter, t)
        var :: generateVars ts

// <@ fun x -> (% <@ x @> ) @> ~ lambda (fun x -> x)
let lambda (f : Expr<'T> -> Expr<'R>) : Expr<'T -> 'R> =
    let [var] = generateVars [typeof<'T>]
    Expr.Cast<_>(Expr.Lambda(var,  f (Expr.Cast<_>(Expr.Var var))))

// Helper Equality type
module Eq = 
    type Eq<'A, 'B> = private Refl of (Expr<'A> -> Expr<'B>) * (Expr<'B> -> Expr<'A>)
    
    let refl<'A> () : Eq<'A, 'A> = Refl (id, id)
    let cast : Eq<'A, 'B> -> Expr<'A> -> Expr<'B> = fun (Refl (f, _)) -> f

open Eq

// HOAS for a simple language
type Exp<'T> = 
    abstract member Invoke : Lambda<'T> -> Expr<'T>
and Lambda<'T> = 
    abstract member Invoke<'S> : Eq<'S, 'T> * Expr<'S> -> Expr<'T>
    abstract member Invoke<'S, 'K> : Eq<'S * 'K, 'T> * Exp<'S> * Exp<'K> -> Expr<'T>
    abstract member Invoke<'S, 'K> : Eq<'S -> 'K, 'T> * (Exp<'S> -> Exp<'K>) -> Expr<'T>
    abstract member Invoke<'S, 'K> : Eq<'K, 'T> * (Exp<'S -> 'K>) * Exp<'S> -> Expr<'T>
    abstract member Invoke<'S, 'K> : Eq<'S -> 'K, 'T> * (Exp<('S -> 'K) -> ('S -> 'K)>) -> Expr<'T>


type Value<'T>(value : Expr<'T>) =
    interface Exp<'T> with
        member sekf.Invoke lambda = lambda.Invoke(refl (), value) 

type Tup<'T, 'S>(first : Exp<'T>, second : Exp<'S>) =
    interface Exp<'T * 'S> with
        member sekf.Invoke lambda = lambda.Invoke(refl (), first, second)

type Lam<'T, 'S>(f : Exp<'T> -> Exp<'S>) =
    interface Exp<'T -> 'S> with
        member sekf.Invoke lambda = lambda.Invoke(refl (), f)

type App<'T, 'S>(f : Exp<'T -> 'S>, x : Exp<'T>) =
    interface Exp<'S> with
        member sekf.Invoke lambda = lambda.Invoke(refl (), f, x)

type Rec<'T, 'S>(f : Exp<('T -> 'S) -> ('T -> 'S)>) =
    interface Exp<'T -> 'S> with
        member sekf.Invoke lambda = lambda.Invoke(refl (), f)
    
// helper combinators
let lift (value : Expr<'T>) : Exp<'T> = 
    new Value<'T>(value) :> _

let tup (first : Exp<'T>) (second : Exp<'S>) : Exp<'T * 'S>  = 
    new Tup<'T, 'S>(first, second) :> _

let lam (f : Exp<'T> -> Exp<'S>) : Exp<'T -> 'S> = 
    new Lam<'T, 'S>(f) :> _

let app (f : Exp<'T -> 'S>) (x : Exp<'T>) : Exp<'S> = 
    new App<'T, 'S>(f, x) :> _

let rec fix (f : Exp<('T -> 'S) -> ('T -> 'S)>) : Exp<'T -> 'S> =
    new Rec<'T, 'S>(f) :> _

// compile HOAS to quotation
let rec compile<'T> (exp : Exp<'T>) : Expr<'T> = 
    exp.Invoke {
        new Lambda<'T> with
            member self.Invoke<'S>(eq : Eq<'S, 'T>, v : Expr<'S>) : Expr<'T> = 
                cast eq v
            member self.Invoke<'S, 'K>(eq : Eq<'S * 'K, 'T>, first : Exp<'S>, second : Exp<'K>) : Expr<'T> = 
                cast eq <@ ((% compile first) , (% compile second)) @>
            member self.Invoke<'S, 'K>(eq : Eq<'S -> 'K, 'T>, f : Exp<'S> -> Exp<'K>) : Expr<'T> = 
                let f' = lambda (fun v -> (compile (f (lift v)))) 
                cast eq f'
            member self.Invoke<'S, 'K>(eq : Eq<'K, 'T>, f : Exp<'S -> 'K>, v : Exp<'S>) : Expr<'T> =
                let r = <@ (% compile f) (% compile v) @>
                cast eq r
            member self.Invoke<'S, 'K>(eq : Eq<'S -> 'K, 'T>, f : Exp<('S -> 'K) -> ('S -> 'K)>) : Expr<'T> = 
                let f' = <@ fun x ->
                             let rec loop x = 
                                (% compile f) loop x 
                             loop x @>
                cast eq f'
    }
// Example
let fact = compile 
              (fix (lam (fun f -> 
                    lam (fun y -> 
                        let y' = compile y
                        lift (<@ if %y' = 0 then 1 else %y' * (% compile f) (%y' - 1) @>)))))

let fact' = QuotationCompiler.ToFunc fact ()

fact' 4
namespace System
namespace QuotationCompiler
namespace Microsoft
namespace Microsoft.FSharp
namespace Microsoft.FSharp.Quotations
val counter : int ref

Full name: Script.counter
Multiple items
val ref : value:'T -> 'T ref

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

--------------------
type 'T ref = Ref<'T>

Full name: Microsoft.FSharp.Core.ref<_>
val generateVars : types:Type list -> Var list

Full name: Script.generateVars
val types : Type list
type Type =
  inherit MemberInfo
  member Assembly : Assembly
  member AssemblyQualifiedName : string
  member Attributes : TypeAttributes
  member BaseType : Type
  member ContainsGenericParameters : bool
  member DeclaringMethod : MethodBase
  member DeclaringType : Type
  member Equals : o:obj -> bool + 1 overload
  member FindInterfaces : filter:TypeFilter * filterCriteria:obj -> Type[]
  member FindMembers : memberType:MemberTypes * bindingAttr:BindingFlags * filter:MemberFilter * filterCriteria:obj -> MemberInfo[]
  ...

Full name: System.Type
type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>
Multiple items
type Var =
  interface IComparable
  new : name:string * typ:Type * ?isMutable:bool -> Var
  member IsMutable : bool
  member Name : string
  member Type : Type
  static member Global : name:string * typ:Type -> Var

Full name: Microsoft.FSharp.Quotations.Var

--------------------
new : name:string * typ:Type * ?isMutable:bool -> Var
val t : Type
val ts : Type list
val incr : cell:int ref -> unit

Full name: Microsoft.FSharp.Core.Operators.incr
val var : Var
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val lambda : f:(Expr<'T> -> Expr<'R>) -> Expr<('T -> 'R)>

Full name: Script.lambda
val f : (Expr<'T> -> Expr<'R>)
Multiple items
type Expr =
  override Equals : obj:obj -> bool
  member GetFreeVars : unit -> seq<Var>
  member Substitute : substitution:(Var -> Expr option) -> Expr
  member ToString : full:bool -> string
  member CustomAttributes : Expr list
  member Type : Type
  static member AddressOf : target:Expr -> Expr
  static member AddressSet : target:Expr * value:Expr -> Expr
  static member Application : functionExpr:Expr * argument:Expr -> Expr
  static member Applications : functionExpr:Expr * arguments:Expr list list -> Expr
  ...

Full name: Microsoft.FSharp.Quotations.Expr

--------------------
type Expr<'T> =
  inherit Expr
  member Raw : Expr

Full name: Microsoft.FSharp.Quotations.Expr<_>
val typeof<'T> : Type

Full name: Microsoft.FSharp.Core.Operators.typeof
static member Expr.Cast : source:Expr -> Expr<'T>
static member Expr.Lambda : parameter:Var * body:Expr -> Expr
static member Expr.Var : variable:Var -> Expr
type Eq<'A,'B> = private | Refl of (Expr<'A> -> Expr<'B>) * (Expr<'B> -> Expr<'A>)

Full name: Script.Eq.Eq<_,_>
union case Eq.Refl: (Expr<'A> -> Expr<'B>) * (Expr<'B> -> Expr<'A>) -> Eq<'A,'B>
val refl : unit -> Eq<'A,'A>

Full name: Script.Eq.refl
val id : x:'T -> 'T

Full name: Microsoft.FSharp.Core.Operators.id
val cast : Eq<'A,'B> -> (Expr<'A> -> Expr<'B>)

Full name: Script.Eq.cast
val f : (Expr<'A> -> Expr<'B>)
module Eq

from Script
type Exp<'T> =
  interface
    abstract member Invoke : Lambda<'T> -> Expr<'T>
  end

Full name: Script.Exp<_>
abstract member Exp.Invoke : Lambda<'T> -> Expr<'T>

Full name: Script.Exp`1.Invoke
type Lambda<'T> =
  interface
    abstract member Invoke : Eq<'S,'T> * Expr<'S> -> Expr<'T>
    abstract member Invoke : Eq<('S * 'K),'T> * Exp<'S> * Exp<'K> -> Expr<'T>
    abstract member Invoke : Eq<('S -> 'K),'T> * (Exp<'S> -> Exp<'K>) -> Expr<'T>
    abstract member Invoke : Eq<'K,'T> * Exp<('S -> 'K)> * Exp<'S> -> Expr<'T>
    abstract member Invoke : Eq<('S -> 'K),'T> * Exp<(('S -> 'K) -> 'S -> 'K)> -> Expr<'T>
  end

Full name: Script.Lambda<_>
abstract member Lambda.Invoke : Eq<'S,'T> * Expr<'S> -> Expr<'T>

Full name: Script.Lambda`1.Invoke
Multiple items
module Eq

from Script

--------------------
type Eq<'A,'B> = private | Refl of (Expr<'A> -> Expr<'B>) * (Expr<'B> -> Expr<'A>)

Full name: Script.Eq.Eq<_,_>
abstract member Lambda.Invoke : Eq<('S * 'K),'T> * Exp<'S> * Exp<'K> -> Expr<'T>

Full name: Script.Lambda`1.Invoke
abstract member Lambda.Invoke : Eq<('S -> 'K),'T> * (Exp<'S> -> Exp<'K>) -> Expr<'T>

Full name: Script.Lambda`1.Invoke
abstract member Lambda.Invoke : Eq<'K,'T> * Exp<('S -> 'K)> * Exp<'S> -> Expr<'T>

Full name: Script.Lambda`1.Invoke
abstract member Lambda.Invoke : Eq<('S -> 'K),'T> * Exp<(('S -> 'K) -> 'S -> 'K)> -> Expr<'T>

Full name: Script.Lambda`1.Invoke
Multiple items
type Value<'T> =
  interface Exp<'T>
  new : value:Expr<'T> -> Value<'T>

Full name: Script.Value<_>

--------------------
new : value:Expr<'T> -> Value<'T>
val value : Expr<'T>
val sekf : Value<'T>
override Value.Invoke : lambda:Lambda<'T> -> Expr<'T>

Full name: Script.Value`1.Invoke
val lambda : Lambda<'T>
abstract member Lambda.Invoke : Eq<'S,'T> * Expr<'S> -> Expr<'T>
abstract member Lambda.Invoke : Eq<('S -> 'K),'T> * (Exp<'S> -> Exp<'K>) -> Expr<'T>
abstract member Lambda.Invoke : Eq<('S -> 'K),'T> * Exp<(('S -> 'K) -> 'S -> 'K)> -> Expr<'T>
abstract member Lambda.Invoke : Eq<('S * 'K),'T> * Exp<'S> * Exp<'K> -> Expr<'T>
abstract member Lambda.Invoke : Eq<'K,'T> * Exp<('S -> 'K)> * Exp<'S> -> Expr<'T>
Multiple items
type Tup<'T,'S> =
  interface Exp<'T * 'S>
  new : first:Exp<'T> * second:Exp<'S> -> Tup<'T,'S>

Full name: Script.Tup<_,_>

--------------------
new : first:Exp<'T> * second:Exp<'S> -> Tup<'T,'S>
val first : Exp<'T>
val second : Exp<'S>
val sekf : Tup<'T,'S>
override Tup.Invoke : lambda:Lambda<'T * 'S> -> Expr<'T * 'S>

Full name: Script.Tup`2.Invoke
val lambda : Lambda<'T * 'S>
Multiple items
type Lam<'T,'S> =
  interface Exp<('T -> 'S)>
  new : f:(Exp<'T> -> Exp<'S>) -> Lam<'T,'S>

Full name: Script.Lam<_,_>

--------------------
new : f:(Exp<'T> -> Exp<'S>) -> Lam<'T,'S>
val f : (Exp<'T> -> Exp<'S>)
val sekf : Lam<'T,'S>
override Lam.Invoke : lambda:Lambda<('T -> 'S)> -> Expr<('T -> 'S)>

Full name: Script.Lam`2.Invoke
val lambda : Lambda<('T -> 'S)>
Multiple items
type App<'T,'S> =
  interface Exp<'S>
  new : f:Exp<('T -> 'S)> * x:Exp<'T> -> App<'T,'S>

Full name: Script.App<_,_>

--------------------
new : f:Exp<('T -> 'S)> * x:Exp<'T> -> App<'T,'S>
val f : Exp<('T -> 'S)>
val x : Exp<'T>
val sekf : App<'T,'S>
override App.Invoke : lambda:Lambda<'S> -> Expr<'S>

Full name: Script.App`2.Invoke
val lambda : Lambda<'S>
Multiple items
type Rec<'T,'S> =
  interface Exp<('T -> 'S)>
  new : f:Exp<(('T -> 'S) -> 'T -> 'S)> -> Rec<'T,'S>

Full name: Script.Rec<_,_>

--------------------
new : f:Exp<(('T -> 'S) -> 'T -> 'S)> -> Rec<'T,'S>
val f : Exp<(('T -> 'S) -> 'T -> 'S)>
val sekf : Rec<'T,'S>
override Rec.Invoke : lambda:Lambda<('T -> 'S)> -> Expr<('T -> 'S)>

Full name: Script.Rec`2.Invoke
val lift : value:Expr<'T> -> Exp<'T>

Full name: Script.lift
val tup : first:Exp<'T> -> second:Exp<'S> -> Exp<'T * 'S>

Full name: Script.tup
val lam : f:(Exp<'T> -> Exp<'S>) -> Exp<('T -> 'S)>

Full name: Script.lam
val app : f:Exp<('T -> 'S)> -> x:Exp<'T> -> Exp<'S>

Full name: Script.app
val fix : f:Exp<(('T -> 'S) -> 'T -> 'S)> -> Exp<('T -> 'S)>

Full name: Script.fix
val compile : exp:Exp<'T> -> Expr<'T>

Full name: Script.compile
val exp : Exp<'T>
abstract member Exp.Invoke : Lambda<'T> -> Expr<'T>
val self : Lambda<'T>
val eq : Eq<'S,'T>
val v : Expr<'S>
val eq : Eq<('S * 'K),'T>
val first : Exp<'S>
val second : Exp<'K>
val eq : Eq<('S -> 'K),'T>
val f : (Exp<'S> -> Exp<'K>)
val f' : Expr<('S -> 'K)>
val eq : Eq<'K,'T>
val f : Exp<('S -> 'K)>
val v : Exp<'S>
val r : Expr<'K>
val f : Exp<(('S -> 'K) -> 'S -> 'K)>
val x : 'S
val loop : ('S -> 'K)
val fact : Expr<(int -> int)>

Full name: Script.fact
val f : Exp<(int -> int)>
val y : Exp<int>
val y' : Expr<int>
val fact' : (int -> int)

Full name: Script.fact'
Multiple items
namespace QuotationCompiler

--------------------
type QuotationCompiler =
  private new : unit -> QuotationCompiler
  static member Eval : expr:Expr<'T> * ?useCache:bool -> 'T
  static member ToAssembly : expr:Expr * ?targetDirectory:string * ?assemblyName:string * ?compiledModuleName:string * ?compiledFunctionName:string -> string
  static member ToDynamicAssembly : expr:Expr * ?assemblyName:string -> MethodInfo
  static member ToFunc : expr:Expr<'T> * ?useCache:bool -> (unit -> 'T)

Full name: QuotationCompiler.QuotationCompiler
static member QuotationCompiler.ToFunc : expr:Expr<'T> * ?useCache:bool -> (unit -> 'T)
Raw view Test code New version

More information

Link:http://fssnip.net/7SF
Posted:7 years ago
Author:Nick Palladinos
Tags: hoas , staging