Generic Peano arithmetic

An attempt at defining Peano arithmetic for all numeric types

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

let inline zero () : ^T = LanguagePrimitives.GenericZero< ^T>
let inline succ (x : ^T) = x + LanguagePrimitives.GenericOne< ^T> : ^T
let inline incr (x : ^T ref) = x := succ !x

let inline infiniteSeq (x : ^T) =
    let rec infinite x = seq { yield x ; yield! infinite (succ x) }
    infinite x


infiniteSeq 42 |> Seq.take 5 |> Seq.toArray
infiniteSeq 3.14 |> Seq.take 10 |> Seq.toArray

type Peano = Zero | Succ of Peano
with
    static member (+) (x : Peano, y : Peano) =
        let rec add x = function Zero -> x | Succ y -> add (Succ x) y
        add x y

    static member One = Succ Zero     
        
infiniteSeq Zero |> Seq.take 10 |> Seq.toArray

val zero : unit -> 'T (requires member get_Zero)

Full name: Script.zero

module LanguagePrimitives

from Microsoft.FSharp.Core

val GenericZero<'T (requires member get_Zero)> : 'T (requires member get_Zero)

Full name: Microsoft.FSharp.Core.LanguagePrimitives.GenericZero

val succ : x:'T -> 'T (requires member ( + ) and member get_One)

Full name: Script.succ

val x : 'T (requires member ( + ) and member get_One)

val GenericOne<'T (requires member get_One)> : 'T (requires member get_One)

Full name: Microsoft.FSharp.Core.LanguagePrimitives.GenericOne

val incr : x:'T ref -> unit (requires member ( + ) and member get_One)

Full name: Script.incr

val x : 'T ref (requires member ( + ) and member get_One)

Multiple items
val ref : value:'T -> 'T ref

Full name: Microsoft.FSharp.Core.Operators.ref

--------------------
type 'T ref = Ref<'T>

Full name: Microsoft.FSharp.Core.ref<_>

val infiniteSeq : x:'T -> seq<'T> (requires member ( + ) and member get_One)

Full name: Script.infiniteSeq

val infinite : ('T -> seq<'T>) (requires member ( + ) and member get_One)

Multiple items
val seq : sequence:seq<'T> -> seq<'T>

Full name: Microsoft.FSharp.Core.Operators.seq

--------------------
type seq<'T> = System.Collections.Generic.IEnumerable<'T>

Full name: Microsoft.FSharp.Collections.seq<_>

module Seq

from Microsoft.FSharp.Collections

val take : count:int -> source:seq<'T> -> seq<'T>

Full name: Microsoft.FSharp.Collections.Seq.take

val toArray : source:seq<'T> -> 'T []

Full name: Microsoft.FSharp.Collections.Seq.toArray

type Peano =
  | Zero
  | Succ of Peano
  static member One : Peano
  static member ( + ) : x:Peano * y:Peano -> Peano

Full name: Script.Peano

union case Peano.Zero: Peano

union case Peano.Succ: Peano -> Peano

val x : Peano

val y : Peano

val add : (Peano -> Peano -> Peano)

static member Peano.One : Peano

Full name: Script.Peano.One

Previous Version Raw view Test code New version

More information

Link:	http://fssnip.net/hO
Posted:	11 years ago
Author:	Eirik Tsarpalis
Tags:	peano , static generics