4 people like it.

An attempt at encoding GADTs

Demonstrates a possible encoding for GADTs in F#. It is type safe, uses no reflection and pattern matches can be declared outside of the definition itself. See also http://lambda-the-ultimate.org/node/1134

  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: 
//type Expr<'T> =
//    Const : 'T -> Expr<'T>
//    Add : Expr<int> -> Expr<int> -> Expr<int>
//    IfThenElse : Expr<bool> -> Expr<'T> -> Expr<'T> -> Expr<'T>
//    App : Expr<'T -> 'S> -> Expr<'T> -> Expr<'S>
//    Lam : (Expr<'T> -> Expr<'S>) -> Expr<'T -> 'S>
//    Fix : Expr<('T -> 'S) -> 'T -> 'S> -> Expr<'T -> 'S>

[<AbstractClass>]
type Expr<'T> internal () =
    abstract Match : IPatternMatch<'T, 'R> -> 'R

// instaces of IPatternMatch encode a match expression

and IPatternMatch<'T, 'R> =
    abstract Const : 'T -> 'R
    abstract Add : Expr<int> -> Expr<int> -> 'R
    abstract IfThenElse : Expr<bool> -> Expr<'T> -> Expr<'T> -> 'R
    abstract App<'S> : Expr<'S -> 'T> -> Expr<'S> -> 'R
    abstract Lam<'T1, 'T2> : (Expr<'T1> -> Expr<'T2>) -> 'R
    abstract Fix<'T1, 'T2> : Expr<('T1 -> 'T2) -> 'T1 -> 'T2> -> 'R

// concrete case implementations

type internal Const<'T>(value : 'T) =
    inherit Expr<'T> ()
    override __.Match (m : IPatternMatch<'T, 'R>) = m.Const value

type internal Add(left : Expr<int>, right : Expr<int>) =
    inherit Expr<int> ()
    override __.Match (m : IPatternMatch<int, 'R>) = m.Add left right

type internal IfThenElse<'T>(b : Expr<bool>, l : Expr<'T>, r : Expr<'T>) =
    inherit Expr<'T> ()
    override __.Match (m : IPatternMatch<'T, 'R>) = m.IfThenElse b l r

type internal App<'T,'S> (f : Expr<'S -> 'T>, x : Expr<'S>) =
    inherit Expr<'T> ()
    override __.Match (m : IPatternMatch<'T, 'R>) = m.App f x

type internal Lam<'T1,'T2> (f : Expr<'T1> -> Expr<'T2>) =
    inherit Expr<'T1 -> 'T2> ()
    override __.Match (m : IPatternMatch<'T1 -> 'T2, 'R>) = m.Lam f

type internal Fix<'T, 'S> (f : Expr<('T -> 'S) -> 'T -> 'S>) =
    inherit Expr<'T -> 'S> ()
    override __.Match (m : IPatternMatch<'T -> 'S, 'R>) = m.Fix f

// constructor api

let constant x = Const<_>(x) :> Expr<_>
let add x y = Add(x,y) :> Expr<_>
let ifThenElse b l r = IfThenElse<_>(b,l,r) :> Expr<_>
let app f x = App<_,_>(f,x) :> Expr<_>
let lam f = Lam<_,_>(f) :> Expr<_>
let fix f = Fix<_,_>(f) :> Expr<_>

let pmatch (x : Expr<'T>) (pattern : IPatternMatch<'T, 'R>) = x.Match pattern


// example 1 : pretty print

let rec pretty<'T> (expr : Expr<'T>) : string =
    pmatch expr {
        new IPatternMatch<'T, string> with
            member __.Const x = sprintf "(%A)" x
            member __.Add x y = sprintf "(%s + %s)" (pretty x) (pretty y)
            member __.IfThenElse b x y = sprintf "if %s then %s else %s" (pretty b) (pretty x) (pretty y)
            member __.App f x = sprintf "(%s %s)" (pretty f) (pretty x)
            // unhandled cases
            member __.Lam _ = invalidOp ""
            member __.Fix _ = invalidOp ""
    }

pretty (ifThenElse (constant true) (constant (Some 12)) (constant None))

// example 2 : eval

// use cast to reconcile type variables of equal type
let cast<'S,'T> (x : 'T) = unbox<'S> x

let rec eval<'T> (expr : Expr<'T>) : 'T =
    pmatch expr {
        new IPatternMatch<'T, 'T> with
            member __.Const x = x
            member __.Add x y = cast<_,int>(eval x + eval y)
            member __.IfThenElse b x y = if eval b then eval x else eval y
            member __.App f x = (eval f) (eval x)
            member __.Lam<'S1,'S2> f = cast<_, 'S1 -> 'S2>(eval << f << constant)
            member __.Fix<'S1,'S2> f = cast<_, 'S1 -> 'S2>(eval f (fun x -> eval (fix f) x))
    }

eval (app (lam (fun b -> ifThenElse b (constant 12) (constant 42))) (constant false))

let multiply = 
    fix (lam(fun f -> 
        lam(fun n -> 
            ifThenElse (constant (eval n = 0)) 
                (lam (fun _ -> constant 0)) 
                (lam (fun m -> add m (app (app f (add n (constant -1))) m))))))

eval (app (app multiply (constant 6)) (constant 7))
Multiple items
type AbstractClassAttribute =
  inherit Attribute
  new : unit -> AbstractClassAttribute

Full name: Microsoft.FSharp.Core.AbstractClassAttribute

--------------------
new : unit -> AbstractClassAttribute
Multiple items
type Expr<'T> =
  internal new : unit -> Expr<'T>
  abstract member Match : IPatternMatch<'T,'R> -> 'R

Full name: Script.Expr<_>

--------------------
internal new : unit -> Expr<'T>
abstract member Expr.Match : IPatternMatch<'T,'R> -> 'R

Full name: Script.Expr`1.Match
type IPatternMatch<'T,'R> =
  interface
    abstract member Add : Expr<int> -> Expr<int> -> 'R
    abstract member App : Expr<('S -> 'T)> -> Expr<'S> -> 'R
    abstract member Const : 'T -> 'R
    abstract member Fix : Expr<(('T1 -> 'T2) -> 'T1 -> 'T2)> -> 'R
    abstract member IfThenElse : Expr<bool> -> Expr<'T> -> Expr<'T> -> 'R
    abstract member Lam : (Expr<'T1> -> Expr<'T2>) -> 'R
  end

Full name: Script.IPatternMatch<_,_>
abstract member IPatternMatch.Const : 'T -> 'R

Full name: Script.IPatternMatch`2.Const
abstract member IPatternMatch.Add : Expr<int> -> Expr<int> -> 'R

Full name: Script.IPatternMatch`2.Add
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 IPatternMatch.IfThenElse : Expr<bool> -> Expr<'T> -> Expr<'T> -> 'R

Full name: Script.IPatternMatch`2.IfThenElse
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
abstract member IPatternMatch.App : Expr<('S -> 'T)> -> Expr<'S> -> 'R

Full name: Script.IPatternMatch`2.App
abstract member IPatternMatch.Lam : (Expr<'T1> -> Expr<'T2>) -> 'R

Full name: Script.IPatternMatch`2.Lam
abstract member IPatternMatch.Fix : Expr<(('T1 -> 'T2) -> 'T1 -> 'T2)> -> 'R

Full name: Script.IPatternMatch`2.Fix
Multiple items
type internal Const<'T> =
  inherit Expr<'T>
  new : value:'T -> Const<'T>
  override Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.Const<_>

--------------------
internal new : value:'T -> Const<'T>
val value : 'T
override internal Const.Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.Const`1.Match
val m : IPatternMatch<'T,'a>
abstract member IPatternMatch.Const : 'T -> 'R
Multiple items
type internal Add =
  inherit Expr<int>
  new : left:Expr<int> * right:Expr<int> -> Add
  override Match : m:IPatternMatch<int,'a> -> 'a

Full name: Script.Add

--------------------
internal new : left:Expr<int> * right:Expr<int> -> Add
val left : Expr<int>
val right : Expr<int>
override internal Add.Match : m:IPatternMatch<int,'a> -> 'a

Full name: Script.Add.Match
val m : IPatternMatch<int,'a>
abstract member IPatternMatch.Add : Expr<int> -> Expr<int> -> 'R
Multiple items
type internal IfThenElse<'T> =
  inherit Expr<'T>
  new : b:Expr<bool> * l:Expr<'T> * r:Expr<'T> -> IfThenElse<'T>
  override Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.IfThenElse<_>

--------------------
internal new : b:Expr<bool> * l:Expr<'T> * r:Expr<'T> -> IfThenElse<'T>
val b : Expr<bool>
val l : Expr<'T>
val r : Expr<'T>
override internal IfThenElse.Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.IfThenElse`1.Match
abstract member IPatternMatch.IfThenElse : Expr<bool> -> Expr<'T> -> Expr<'T> -> 'R
Multiple items
type internal App<'T,'S> =
  inherit Expr<'T>
  new : f:Expr<('S -> 'T)> * x:Expr<'S> -> App<'T,'S>
  override Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.App<_,_>

--------------------
internal new : f:Expr<('S -> 'T)> * x:Expr<'S> -> App<'T,'S>
val f : Expr<('S -> 'T)>
val x : Expr<'S>
override internal App.Match : m:IPatternMatch<'T,'a> -> 'a

Full name: Script.App`2.Match
abstract member IPatternMatch.App : Expr<('S -> 'T)> -> Expr<'S> -> 'R
Multiple items
type internal Lam<'T1,'T2> =
  inherit Expr<('T1 -> 'T2)>
  new : f:(Expr<'T1> -> Expr<'T2>) -> Lam<'T1,'T2>
  override Match : m:IPatternMatch<('T1 -> 'T2),'a> -> 'a

Full name: Script.Lam<_,_>

--------------------
internal new : f:(Expr<'T1> -> Expr<'T2>) -> Lam<'T1,'T2>
val f : (Expr<'T1> -> Expr<'T2>)
override internal Lam.Match : m:IPatternMatch<('T1 -> 'T2),'a> -> 'a

Full name: Script.Lam`2.Match
val m : IPatternMatch<('T1 -> 'T2),'a>
abstract member IPatternMatch.Lam : (Expr<'T1> -> Expr<'T2>) -> 'R
Multiple items
type internal Fix<'T,'S> =
  inherit Expr<('T -> 'S)>
  new : f:Expr<(('T -> 'S) -> 'T -> 'S)> -> Fix<'T,'S>
  override Match : m:IPatternMatch<('T -> 'S),'a> -> 'a

Full name: Script.Fix<_,_>

--------------------
internal new : f:Expr<(('T -> 'S) -> 'T -> 'S)> -> Fix<'T,'S>
val f : Expr<(('T -> 'S) -> 'T -> 'S)>
override internal Fix.Match : m:IPatternMatch<('T -> 'S),'a> -> 'a

Full name: Script.Fix`2.Match
val m : IPatternMatch<('T -> 'S),'a>
abstract member IPatternMatch.Fix : Expr<(('T1 -> 'T2) -> 'T1 -> 'T2)> -> 'R
val constant : x:'a -> Expr<'a>

Full name: Script.constant
val x : 'a
val add : x:Expr<int> -> y:Expr<int> -> Expr<int>

Full name: Script.add
val x : Expr<int>
val y : Expr<int>
val ifThenElse : b:Expr<bool> -> l:Expr<'a> -> r:Expr<'a> -> Expr<'a>

Full name: Script.ifThenElse
val l : Expr<'a>
val r : Expr<'a>
val app : f:Expr<('a -> 'b)> -> x:Expr<'a> -> Expr<'b>

Full name: Script.app
val f : Expr<('a -> 'b)>
val x : Expr<'a>
val lam : f:(Expr<'a> -> Expr<'b>) -> Expr<('a -> 'b)>

Full name: Script.lam
val f : (Expr<'a> -> Expr<'b>)
val fix : f:Expr<(('a -> 'b) -> 'a -> 'b)> -> Expr<('a -> 'b)>

Full name: Script.fix
val f : Expr<(('a -> 'b) -> 'a -> 'b)>
val pmatch : x:Expr<'T> -> pattern:IPatternMatch<'T,'R> -> 'R

Full name: Script.pmatch
val x : Expr<'T>
val pattern : IPatternMatch<'T,'R>
abstract member Expr.Match : IPatternMatch<'T,'R> -> 'R
val pretty : expr:Expr<'T> -> string

Full name: Script.pretty
val expr : Expr<'T>
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 x : 'T
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val __ : IPatternMatch<'T,string>
val y : Expr<'T>
val f : Expr<('a -> 'T)>
val invalidOp : message:string -> 'T

Full name: Microsoft.FSharp.Core.Operators.invalidOp
union case Option.Some: Value: 'T -> Option<'T>
union case Option.None: Option<'T>
val cast : x:'T -> 'S

Full name: Script.cast
val unbox : value:obj -> 'T

Full name: Microsoft.FSharp.Core.Operators.unbox
val eval : expr:Expr<'T> -> 'T

Full name: Script.eval
val __ : IPatternMatch<'T,'T>
val f : (Expr<'S1> -> Expr<'S2>)
val f : Expr<(('S1 -> 'S2) -> 'S1 -> 'S2)>
val x : 'S1
val multiply : Expr<(int -> int -> int)>

Full name: Script.multiply
val f : Expr<(int -> int -> int)>
val n : Expr<int>
val m : Expr<int>

More information

Link:http://fssnip.net/mq
Posted:9 years ago
Author:Eirik Tsarpalis
Tags: gadts