1 people like it.
Like the snippet!

Generic Numeric Literals and Compile time Peano arithmetic

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22:

type Peano = interface end
and Zero = Zero with
    static member inline (|*|) (f, Zero) = f $ Zero
    interface Peano
and Succ<'a when 'a :> Peano> = Succ of 'a  with
    static member inline (|*|) (f, Succ(x)) = f $ Succ(x) 
    interface Peano 

module NumericLiteralG =
    let inline FromZero () = Zero
    let inline FromOne () = Succ Zero


type Add = Add with
    static member ($) (Add, Zero) = fun n -> n
    static member inline ($) (Add, Succ n) = fun n' ->
        Succ ((Add |*| n) n')

let inline (+) a b = (Add $ a) b

let three = 1G + 1G + 1G // Succ<Succ<Succ<Zero>>>
let three' = three + 0G // Succ<Succ<Succ<Zero>>>

Multiple items
union case Zero.Zero: Zero

--------------------
type Zero =
  | Zero
  interface Peano
  static member ( |*| ) : f:'a * Zero:Zero -> '_arg5 (requires member ( $ ))

Full name: Script.Zero

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

type Peano

Full name: Script.Peano

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

--------------------
type Succ<'a (requires 'a :> Peano)> =
  | Succ of 'a
  interface Peano
  static member ( |*| ) : f:'a0 * Succ<'b> -> '_arg8 (requires member ( $ ) and 'b :> Peano)

Full name: Script.Succ<_>

val f : 'a (requires member ( $ ) and 'b :> Peano)

val x : #Peano

val FromZero : unit -> Zero

Full name: Script.NumericLiteralG.FromZero

val FromOne : unit -> Succ<Zero>

Full name: Script.NumericLiteralG.FromOne

Multiple items
union case Add.Add: Add

--------------------
type Add =
  | Add
  static member ( $ ) : Add:Add * Zero:Zero -> ('a -> 'a)
  static member ( $ ) : Add:Add * Succ<'a> -> ('b -> Succ<'c>) (requires 'a :> Peano and member ( |*| ) and 'c :> Peano)

Full name: Script.Add

val n : 'a

val n : 'a (requires 'a :> Peano and member ( |*| ) and 'c :> Peano)

val n' : 'b

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

val b : 'b

val three : Succ<Succ<Succ<Zero>>>

Full name: Script.three

val three' : Succ<Succ<Succ<Zero>>>

Full name: Script.three'

Raw view Test code New version

More information

Link:	http://fssnip.net/7PG
Posted:	8 years ago
Author:	Nick Palladinos
Tags:	peano , type level , numeric literals