5 people like it.

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

More information

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