Type-level Fold

Generic Type-level Fold for Boolean Algebra

 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:

type Bool = interface end
and True = True with
    static member inline (|*|) (f, True) = f $ True
    interface Bool
and False = False with
    static member inline (|*|) (f, False) = f $ False
    interface Bool
and And<'a, 'b when 'a :> Bool and 'b :> Bool> = And of 'a * 'b  with
    static member inline (|*|) (f, x) = (BoolFold ? (f) <- x)
    interface Bool
and Or<'a, 'b when 'a :> Bool and 'b :> Bool> = Or of 'a * 'b  with
    static member inline (|*|) (f, x) = (BoolFold ? (f) <- x)
    interface Bool
and Not<'a when 'a :> Bool> = Not of 'a with
    static member inline (|*|) (f, x) = (BoolFold ? (f) <- x)
    interface Bool

and BoolFold = BoolFold with
    static member inline (?<-) (BoolFold, f, True) = f $ True
    static member inline (?<-) (BoolFold, f, False) = f $ False
    static member inline (?<-) (BoolFold, f, And(a, b)) = 
        let app = And (f |*| a, f |*| b)
        f $ app
    static member inline (?<-) (BoolFold, f, Or(a, b)) = 
        let app = Or (f |*| a, f |*| b)
        f $ app
    static member inline (?<-) (BoolFold, f, Not(a)) = 
        let app = Not (f |*| a)
        f $ app

type Eval = Eval with
    static member inline ($) (Eval, True) = True
    static member inline ($) (Eval, False) = False
    static member inline ($) (Eval, And(True, True)) = True 
    static member inline ($) (Eval, And(True, False)) = False 
    static member inline ($) (Eval, And(False, True)) = False
    static member inline ($) (Eval, And(False, False)) = False 
    static member inline ($) (Eval, Or(True, True)) = True 
    static member inline ($) (Eval, Or(True, False)) = True 
    static member inline ($) (Eval, Or(False, True)) = True
    static member inline ($) (Eval, Or(False, False)) = False  
    static member inline ($) (Eval, Not(True)) = False  
    static member inline ($) (Eval, Not(False)) = True  
       
type BitFlip = BitFlip with
    static member inline ($) (BitFlip, True) = False
    static member inline ($) (BitFlip, False) = True
    static member inline ($) (BitFlip, And(x, y)) = And(x, y)
    static member inline ($) (BitFlip, Or(x, y)) = Or(x, y) 
    static member inline ($) (BitFlip, Not(x)) = Not(x) 
        

let (<&>) a b = And (a, b)
let (<|>) a b = Or (a, b)
let inline fold f (x : ^R) = (BoolFold ? (f) <- x) 

//// Examples

let t = fold BitFlip False // t : True
let f = fold BitFlip True // f : False
let a = fold BitFlip (True <&> False) // And<False,True>
let e = fold Eval (True <&> False) // e : False
let n = fold Eval (True <|> False) // n : True
let k = fold Eval (Not True <|> False) // k : False

Multiple items
union case True.True: True

--------------------
type True =
  | True
  interface Bool
  static member ( |*| ) : f:'a * True:True -> '_arg15 (requires member ( $ ))

Full name: Script.True

val f : 'a (requires member ( $ ))

type Bool

Full name: Script.Bool

Multiple items
union case False.False: False

--------------------
type False =
  | False
  interface Bool
  static member ( |*| ) : f:'a * False:False -> '_arg18 (requires member ( $ ))

Full name: Script.False

Multiple items
union case And.And: 'a * 'b -> And<'a,'b>

--------------------
type And<'a,'b (requires 'a :> Bool and 'b :> Bool)> =
  | And of 'a * 'b
  interface Bool
  static member ( |*| ) : f:'a0 * x:'b1 -> '_arg22 (requires member ( ?<- ))

Full name: Script.And<_,_>

val f : 'a (requires member ( ?<- ))

val x : 'b (requires member ( ?<- ))

Multiple items
union case BoolFold.BoolFold: BoolFold

--------------------
type BoolFold =
  | BoolFold
  static member ( ?<- ) : BoolFold:BoolFold * f:'a * True:True -> '_arg33 (requires member ( $ ))
  static member ( ?<- ) : BoolFold:BoolFold * f:'a * False:False -> '_arg36 (requires member ( $ ))
  static member ( ?<- ) : BoolFold:BoolFold * f:'a * And<'b,'c> -> '_arg45 (requires member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg39 :> Bool and 'c :> Bool and '_arg42 :> Bool)
  static member ( ?<- ) : BoolFold:BoolFold * f:'a * Or<'b,'c> -> '_arg54 (requires member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg48 :> Bool and 'c :> Bool and '_arg51 :> Bool)
  static member ( ?<- ) : BoolFold:BoolFold * f:'a * Not<'b> -> '_arg60 (requires member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg57 :> Bool)

Full name: Script.BoolFold

Multiple items
union case Or.Or: 'a * 'b -> Or<'a,'b>

--------------------
type Or<'a,'b (requires 'a :> Bool and 'b :> Bool)> =
  | Or of 'a * 'b
  interface Bool
  static member ( |*| ) : f:'a0 * x:'b1 -> '_arg26 (requires member ( ?<- ))

Full name: Script.Or<_,_>

Multiple items
union case Not.Not: 'a -> Not<'a>

--------------------
type Not<'a (requires 'a :> Bool)> =
  | Not of 'a
  interface Bool
  static member ( |*| ) : f:'a0 * x:'b -> '_arg30 (requires member ( ?<- ))

Full name: Script.Not<_>

val f : 'a (requires member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg39 :> Bool and 'c :> Bool and '_arg42 :> Bool)

val a : 'b (requires 'b :> Bool and member ( |*| ) and member ( |*| ) and member ( $ ) and '_arg39 :> Bool and 'c :> Bool and '_arg42 :> Bool)

val b : 'c (requires 'c :> Bool and member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg39 :> Bool and '_arg42 :> Bool)

val app : And<#Bool,#Bool>

val f : 'a (requires member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg48 :> Bool and 'c :> Bool and '_arg51 :> Bool)

val a : 'b (requires 'b :> Bool and member ( |*| ) and member ( |*| ) and member ( $ ) and '_arg48 :> Bool and 'c :> Bool and '_arg51 :> Bool)

val b : 'c (requires 'c :> Bool and member ( |*| ) and member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg48 :> Bool and '_arg51 :> Bool)

val app : Or<#Bool,#Bool>

val f : 'a (requires member ( |*| ) and member ( $ ) and 'b :> Bool and '_arg57 :> Bool)

val a : 'b (requires 'b :> Bool and member ( |*| ) and member ( $ ) and '_arg57 :> Bool)

val app : Not<#Bool>

Multiple items
union case Eval.Eval: Eval

--------------------
type Eval =
  | Eval
  static member ( $ ) : Eval:Eval * True:True -> True
  static member ( $ ) : Eval:Eval * False:False -> False
  static member ( $ ) : Eval:Eval * And<True,True> -> True
  static member ( $ ) : Eval:Eval * And<True,False> -> False
  static member ( $ ) : Eval:Eval * And<False,True> -> False
  static member ( $ ) : Eval:Eval * And<False,False> -> False
  static member ( $ ) : Eval:Eval * Or<True,True> -> True
  static member ( $ ) : Eval:Eval * Or<True,False> -> True
  static member ( $ ) : Eval:Eval * Or<False,True> -> True
  static member ( $ ) : Eval:Eval * Or<False,False> -> False
  static member ( $ ) : Eval:Eval * Not<True> -> False
  static member ( $ ) : Eval:Eval * Not<False> -> True

Full name: Script.Eval

Multiple items
union case BitFlip.BitFlip: BitFlip

--------------------
type BitFlip =
  | BitFlip
  static member ( $ ) : BitFlip:BitFlip * True:True -> False
  static member ( $ ) : BitFlip:BitFlip * False:False -> True
  static member ( $ ) : BitFlip:BitFlip * And<'d,'e> -> And<'d,'e> (requires 'd :> Bool and 'e :> Bool)
  static member ( $ ) : BitFlip:BitFlip * Or<'b,'c> -> Or<'b,'c> (requires 'b :> Bool and 'c :> Bool)
  static member ( $ ) : BitFlip:BitFlip * Not<'a> -> Not<'a> (requires 'a :> Bool)

Full name: Script.BitFlip

val x : #Bool

val y : #Bool

val a : #Bool

val b : #Bool

val fold : f:'a -> x:'R -> '_arg4 (requires member ( ?<- ))

Full name: Script.fold

val x : 'R (requires member ( ?<- ))

val t : True

Full name: Script.t

val f : False

Full name: Script.f

val a : And<False,True>

Full name: Script.a

val e : False

Full name: Script.e

val n : True

Full name: Script.n

val k : False

Full name: Script.k

Next Version Raw view Test code New version

More information

Link:	http://fssnip.net/tz
Posted:	8 years ago
Author:	Nick Palladinos
Tags:	generic , type-level , fold