5 people like it.

Peano constructs

Here we define Peano arithmetic using F# abstract data types.

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

(* Peano constructs *)

type Num = 
  | Zero           (* zero = {} *)
  | Succ of Num    (* or a successor of n = {0, 1, 2, ..., n-1} *)

let rec plus x y =
    match y with
    | Zero    -> x
    | Succ y' -> Succ (plus x y')

plus Zero (Succ Zero) /// -> Succ Zero
plus (Succ (Succ Zero)) (Succ Zero) /// Succ Succ Succ Zero = 3

let rec mult x y =
    match y with
    | Zero -> Zero
    | Succ y' -> plus x (mult x y')

mult (Succ Zero) (Succ (Succ (Succ Zero)))
mult (Succ (Succ Zero)) (Succ (Succ Zero))
union case Num.Zero: Num
union case Num.Succ: Num -> Num
type Num =
  | Zero
  | Succ of Num

Full name: Script.Num
val plus : x:Num -> y:Num -> Num

Full name: Script.plus
val x : Num
val y : Num
val y' : Num
val mult : x:Num -> y:Num -> Num

Full name: Script.mult


 -> Succ Zero
 Succ Succ Succ Zero = 3
Raw view Test code New version

More information

Link:http://fssnip.net/ag
Posted:12 years ago
Author:Daniil
Tags: numbers , types

This web site is created using F# and Suave web server. It is hosted on Azure and the source code is on GitHub. Contributions are welcome!

The first version of fssnip.net has been created by @tomaspetricek back in 2010. This web site is a new, open-source and contribution-friendly version.