1 people like it.
Like the snippet!
Generic Numeric Literals and Compile time Peano arithmetic
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'
More information