Type Safe Higher-order abstract syntax

Type Safe 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:

type Expr<'T> = 
    abstract Eval : unit -> 'T

let eval (x : Expr<'T>) = x.Eval()
let lift (value : 'T) = 
    {   new Expr<'T> with
            member self.Eval () = value 
    }

let tup (first : Expr<'T>) (second : Expr<'S>) = 
    {   new Expr<'T * 'S> with
            member self.Eval () = (eval first, eval second)
    }


let lam (f : Expr<'T> -> Expr<'R>) = 
    {   new Expr<'T -> 'R> with
            member self.Eval () = eval << f << lift 
    }

let app (f : Expr<'T -> 'R>) (x : Expr<'T>) = 
    {   new Expr<'R> with
            member self.Eval () = eval f <| eval x
    }

let rec fix (f : Expr<('T -> 'R) -> ('T -> 'R)>) =
    {   new Expr<'T -> 'R> with
            member self.Eval () = eval f <| (fun x -> eval (fix f) x)
    }

let fact = fix (lam (fun f -> lam (fun y -> lift (if eval y = 0 then 1 else eval y * (eval f) (eval y - 1)))))
    
eval fact 4

abstract member Expr.Eval : unit -> 'T

Full name: Script.Expr`1.Eval

type unit = Unit

Full name: Microsoft.FSharp.Core.unit

val eval : x:Expr<'T> -> 'T

Full name: Script.eval

val x : Expr<'T>

type Expr<'T> =
  interface
    abstract member Eval : unit -> 'T
  end

Full name: Script.Expr<_>

abstract member Expr.Eval : unit -> 'T

val lift : value:'T -> Expr<'T>

Full name: Script.lift

val value : 'T

val self : Expr<'T>

val tup : first:Expr<'T> -> second:Expr<'S> -> Expr<'T * 'S>

Full name: Script.tup

val first : Expr<'T>

val second : Expr<'S>

val self : Expr<'T * 'S>

val lam : f:(Expr<'T> -> Expr<'R>) -> Expr<('T -> 'R)>

Full name: Script.lam

val f : (Expr<'T> -> Expr<'R>)

val self : Expr<('T -> 'R)>

val app : f:Expr<('T -> 'R)> -> x:Expr<'T> -> Expr<'R>

Full name: Script.app

val f : Expr<('T -> 'R)>

val self : Expr<'R>

val fix : f:Expr<(('T -> 'R) -> 'T -> 'R)> -> Expr<('T -> 'R)>

Full name: Script.fix

val f : Expr<(('T -> 'R) -> 'T -> 'R)>

val x : 'T

val fact : Expr<(int -> int)>

Full name: Script.fact

val f : Expr<(int -> int)>

val y : Expr<int>

Raw view Test code New version

More information

Link:	http://fssnip.net/gt
Posted:	11 years ago
Author:	Nick Palladinos
Tags:	hoas , gadt