1 people like it.

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'
Raw view Test code New version

More information

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