Normalisation by evaluation

Normalisation of "F# quotations" by evaluation.

 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:

open System
open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.Patterns


// Helper active patters for System.Type
let (|Arrow|_|) (t : Type) = 
    if t.IsGenericType && t.GetGenericTypeDefinition() = typedefof<_ -> _> then
        let args = t.GetGenericArguments()
        Some (args.[0], args.[1])
    else
        None

let (|Base|_|) (t : Type) =
    if t = typeof<obj> then
        Some t
    else
        None


// Semantic Domain
type Sem = 
    | Lam of (Sem -> Sem)
    | Expr of Expr

// reflect : Expr -> Sem
let rec reflect (expr : Expr) = 
    match expr.Type with
    | Arrow (a, b) -> 
        Lam (fun sem -> reflect <| Expr.Application(expr, reify a sem)) 
    | Base _ -> Expr expr 
    | t -> failwithf "Not supported, type: %s" t.Name

// reify : Type -> Sem -> Expr
and reify (t : Type) (sem : Sem) = 
    match t, sem with
    | Arrow (a, b), Lam f -> 
        let var = new Var("var", a) // fresh var
        Expr.Lambda(var, reify b (f (reflect (Expr.Var(var)))))
    | Base _, Expr expr -> expr
    | _ -> failwith "Invalid state"

// meaning : Map<Var, Sem> -> Expr -> Sem
let rec meaning (ctx : Map<Var, Sem>) (expr : Expr) = 
    match expr with
    | Var var -> ctx.[var]
    | Lambda (var, body) -> 
        Lam (fun sem -> meaning (Map.add var sem ctx) body)
    | Application (f, s) -> 
        match meaning ctx f with
        | Lam f' -> f' (meaning ctx s)
        | _ -> failwith "Invalid state"
    | _ -> failwithf "Not supported, expr: %A" expr

// nbe : Expr -> Expr
let nbe (expr : Expr) = 
    reify expr.Type (meaning Map.empty expr)

// Example
let K () = <@ fun x y -> x @>
let S () = <@ fun x y z -> x z (y z) @>
let SKK () = <@ (%S ()) (%K ()) (%K ()) @>

nbe <| SKK () // Lambda (var, var)

namespace System

namespace Microsoft

namespace Microsoft.FSharp

namespace Microsoft.FSharp.Quotations

module Patterns

from Microsoft.FSharp.Quotations

val t : Type

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

property Type.IsGenericType: bool

Type.GetGenericTypeDefinition() : Type

val typedefof<'T> : Type

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

val args : Type []

Type.GetGenericArguments() : Type []

union case Option.Some: Value: 'T -> Option<'T>

union case Option.None: Option<'T>

val typeof<'T> : Type

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

type obj = Object

Full name: Microsoft.FSharp.Core.obj

type Sem =
| Lam of (Sem -> Sem)
| Expr of Expr

Full name: Script.Sem

union case Sem.Lam: (Sem -> Sem) -> Sem

Multiple items
union case Sem.Expr: Expr -> Sem

--------------------
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 reflect : expr:Expr -> Sem

Full name: Script.reflect

val expr : Expr

property Expr.Type: Type

active recognizer Arrow: Type -> (Type * Type) option

Full name: Script.( |Arrow|_| )

val a : Type

val b : Type

val sem : Sem

static member Expr.Application : functionExpr:Expr * argument:Expr -> Expr

val reify : t:Type -> sem:Sem -> Expr

Full name: Script.reify

active recognizer Base: Type -> Type option

Full name: Script.( |Base|_| )

val failwithf : format:Printf.StringFormat<'T,'Result> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.failwithf

property Reflection.MemberInfo.Name: string

val f : (Sem -> Sem)

val var : Var

Multiple items
active recognizer Var: Expr -> Var option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Var|_| )

--------------------
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

static member Expr.Lambda : parameter:Var * body:Expr -> Expr

static member Expr.Var : variable:Var -> Expr

val failwith : message:string -> 'T

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

val meaning : ctx:Map<Var,Sem> -> expr:Expr -> Sem

Full name: Script.meaning

val ctx : Map<Var,Sem>

Multiple items
module Map

from Microsoft.FSharp.Collections

--------------------
type Map<'Key,'Value (requires comparison)> =
  interface IEnumerable
  interface IComparable
  interface IEnumerable<KeyValuePair<'Key,'Value>>
  interface ICollection<KeyValuePair<'Key,'Value>>
  interface IDictionary<'Key,'Value>
  new : elements:seq<'Key * 'Value> -> Map<'Key,'Value>
  member Add : key:'Key * value:'Value -> Map<'Key,'Value>
  member ContainsKey : key:'Key -> bool
  override Equals : obj -> bool
  member Remove : key:'Key -> Map<'Key,'Value>
  ...

Full name: Microsoft.FSharp.Collections.Map<_,_>

--------------------
new : elements:seq<'Key * 'Value> -> Map<'Key,'Value>

active recognizer Lambda: Expr -> (Var * Expr) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Lambda|_| )

val body : Expr

val add : key:'Key -> value:'T -> table:Map<'Key,'T> -> Map<'Key,'T> (requires comparison)

Full name: Microsoft.FSharp.Collections.Map.add

active recognizer Application: Expr -> (Expr * Expr) option

Full name: Microsoft.FSharp.Quotations.Patterns.( |Application|_| )

val f : Expr

val s : Expr

val f' : (Sem -> Sem)

val nbe : expr:Expr -> Expr

Full name: Script.nbe

val empty<'Key,'T (requires comparison)> : Map<'Key,'T> (requires comparison)

Full name: Microsoft.FSharp.Collections.Map.empty

val K : unit -> Expr<('a -> 'b -> 'a)>

Full name: Script.K

val x : 'a

val y : 'b

val S : unit -> Expr<(('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c)>

Full name: Script.S

val x : ('a -> 'b -> 'c)

val y : ('a -> 'b)

val z : 'a

val SKK : unit -> Expr<('a -> 'a)>

Full name: Script.SKK

Raw view Test code New version

More information

Link:	http://fssnip.net/q1
Posted:	9 years ago
Author:	Nick Palladinos
Tags:	quotations