Sylvester.Arithmetic 0.1.2.1

This library implements dependently type natural number arithmetic and constraints using fixed-point decimal types.

There is a newer version of this package available.
See the version list below for details.
Install-Package Sylvester.Arithmetic -Version 0.1.2.1
dotnet add package Sylvester.Arithmetic --version 0.1.2.1
<PackageReference Include="Sylvester.Arithmetic" Version="0.1.2.1" />
For projects that support PackageReference, copy this XML node into the project file to reference the package.
paket add Sylvester.Arithmetic --version 0.1.2.1
The NuGet Team does not provide support for this client. Please contact its maintainers for support.

Sylvester.Arithmetic

This library implements dependently typed natural number arithmetic and constraints which enable arithmetic operations like bounds checking to be performed at compile-time by the F# type checker as long as the values for the operations are known at compile-time.

#load "Paket.fsx"
Paket.Package["Sylvester.Arithmetic"] ///Use the Sylvester.Arithmetic NuGet package

#load "Paket.Generated.Refs.fsx"

open Sylvester.Arithmetic
open Sylvester.Arithmetic.N10

///Create typed representations of some natural numbers
let a,b,c = new N<400>(), new N<231111>(), new N<6577700>()

a + b + c
N<6809211UL>

These values have types derived from Sylvester.Arithmetic.N10. The type of a is N10&lt;0,0,0,0,0,0,0,4,0,0&gt; and the type of c is N10&lt;0,0,0,6,5,7,7,7,0,0&gt;.

c.GetType()
Sylvester.Arithmetic.N10+N10`10[Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+6,Sylvester.Arithmetic.Base10+5,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0]

The types of the results of arithmetic operations depend on the values of the operands.

let d = (a + b + c) * four

d
N<27236844UL>
d.GetType()
Sylvester.Arithmetic.N10+N10`10[Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+2,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+2,Sylvester.Arithmetic.Base10+3,Sylvester.Arithmetic.Base10+6,Sylvester.Arithmetic.Base10+8,Sylvester.Arithmetic.Base10+4,Sylvester.Arithmetic.Base10+4]

This enables type-level constraints to be written which run at compile-time

check(d +< ten) /// Type error
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
a - (two * a) /// A negative number results in a type representing an underflow at compile-time 
N10Underflow
let myop a b c d =
    check(a +> b)
    check (b +== zero)
    check (c +== (a + one))
    a + b + c + d
    
myop four five four ten  ///Type error. Program will not compile
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
let myop a b c d =
    check(a +> b)
    check (b +== zero)
    check (c +== (a + one))
    a + b + c + d
    
myop seven zero eight ten  ///Program compiles once the parameters to myop satisfy the arithmetic constraints
N<25UL>

Sylvester.Arithmetic

This library implements dependently typed natural number arithmetic and constraints which enable arithmetic operations like bounds checking to be performed at compile-time by the F# type checker as long as the values for the operations are known at compile-time.

#load "Paket.fsx"
Paket.Package["Sylvester.Arithmetic"] ///Use the Sylvester.Arithmetic NuGet package

#load "Paket.Generated.Refs.fsx"

open Sylvester.Arithmetic
open Sylvester.Arithmetic.N10

///Create typed representations of some natural numbers
let a,b,c = new N<400>(), new N<231111>(), new N<6577700>()

a + b + c
N<6809211UL>

These values have types derived from Sylvester.Arithmetic.N10. The type of a is N10&lt;0,0,0,0,0,0,0,4,0,0&gt; and the type of c is N10&lt;0,0,0,6,5,7,7,7,0,0&gt;.

c.GetType()
Sylvester.Arithmetic.N10+N10`10[Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+6,Sylvester.Arithmetic.Base10+5,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0]

The types of the results of arithmetic operations depend on the values of the operands.

let d = (a + b + c) * four

d
N<27236844UL>
d.GetType()
Sylvester.Arithmetic.N10+N10`10[Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+0,Sylvester.Arithmetic.Base10+2,Sylvester.Arithmetic.Base10+7,Sylvester.Arithmetic.Base10+2,Sylvester.Arithmetic.Base10+3,Sylvester.Arithmetic.Base10+6,Sylvester.Arithmetic.Base10+8,Sylvester.Arithmetic.Base10+4,Sylvester.Arithmetic.Base10+4]

This enables type-level constraints to be written which run at compile-time

check(d +< ten) /// Type error
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
a - (two * a) /// A negative number results in a type representing an underflow at compile-time 
N10Underflow
let myop a b c d =
    check(a +> b)
    check (b +== zero)
    check (c +== (a + one))
    a + b + c + d
    
myop four five four ten  ///Type error. Program will not compile
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
Type mismatch. Expecting a
    'Constraint<Success>'    
but given a
    'Constraint<Failure>'    
The type 'Success' does not match the type 'Failure'
let myop a b c d =
    check(a +> b)
    check (b +== zero)
    check (c +== (a + one))
    a + b + c + d
    
myop seven zero eight ten  ///Program compiles once the parameters to myop satisfy the arithmetic constraints
N<25UL>

This package is not used by any popular GitHub repositories.

Version History

Version Downloads Last updated
0.2.5.1 65 2/6/2020
0.2.5 85 2/6/2020
0.2.4 104 1/16/2020
0.2.3 42 1/16/2020
0.2.2.1 73 1/3/2020
0.2.2 81 1/3/2020
0.2.1 70 12/30/2019
0.2.0 81 12/30/2019
0.1.7 100 6/23/2019
0.1.6 88 6/22/2019
0.1.5.1 85 6/21/2019
0.1.3 91 6/12/2019
0.1.2.2 96 6/10/2019
0.1.2.1 99 6/10/2019
Show less