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: 

//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<'T1, 'T2> (f : Expr<('T1 -> 'T2) -> 'T1 -> 'T2>) =
    inherit Expr<'T1 -> 'T2> ()
    override __.Match (m : IPatternMatch<'T1 -> 'T2, '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 (pattern : IPatternMatch<'T, 'R>) (x : Expr<'T>) = x.Match pattern

// example : implement evaluator using pattern match

let cast (x : 'T) = x :> obj :?> 'S

let rec eval<'T> (expr : Expr<'T>) : 'T =
    pmatch {
        new IPatternMatch<'T, 'T> with
            member __.Const x = x
            member __.Add x y = cast(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 f = cast(eval << f << constant)
            member __.Fix f = cast(eval f (fun x -> eval (fix f) x))
    } expr

// tests

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 multiply) 6 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<'T1,'T2> =
  inherit Expr<('T1 -> 'T2)>
  new : f:Expr<(('T1 -> 'T2) -> 'T1 -> 'T2)> -> Fix<'T1,'T2>
  override Match : m:IPatternMatch<('T1 -> 'T2),'a> -> 'a

Full name: Script.Fix<_,_>

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

Full name: Script.Fix`2.Match
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 : pattern:IPatternMatch<'T,'R> -> x:Expr<'T> -> 'R

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

Full name: Script.cast
val x : 'T
type obj = System.Object

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

Full name: Script.eval
val expr : Expr<'T>
val __ : IPatternMatch<'T,'T>
val y : Expr<'T>
val f : Expr<('a -> 'T)>
val multiply : Expr<(int -> int -> int)>

Full name: Script.multiply
val f : Expr<(int -> int -> int)>
val n : Expr<int>
val m : Expr<int>
Next Version Raw view Test code New version

More information

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

This web site is created using F# and Suave web server. It is hosted on Azure and the source code is on GitHub. Contributions are welcome!

The first version of fssnip.net has been created by @tomaspetricek back in 2010. This web site is a new, open-source and contribution-friendly version.