4 people like it.

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

More information

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