Sylvester.Arithmetic
0.2.5.1
Typelevel natural number arithmetic and constraints using fixedpoint decimal types.
InstallPackage Sylvester.Arithmetic Version 0.2.5.1
dotnet add package Sylvester.Arithmetic version 0.2.5.1
<PackageReference Include="Sylvester.Arithmetic" Version="0.2.5.1" />
paket add Sylvester.Arithmetic version 0.2.5.1
#r "nuget: Sylvester.Arithmetic, 0.2.5.1"
Sylvester.Arithmetic
This library implements lightweight dependently typed natural number arithmetic and constraints which enable arithmetic operations like bounds checking to be performed at compiletime by the F# type checker as long as the values for the operations are known at compiletime.
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<0,0,0,0,0,0,0,4,0,0> and the type of c
is N10<0,0,0,6,5,7,7,7,0,0>.
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 typelevel constraints to be written which run at compiletime
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 compiletime
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 lightweight dependently typed natural number arithmetic and constraints which enable arithmetic operations like bounds checking to be performed at compiletime by the F# type checker as long as the values for the operations are known at compiletime.
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<0,0,0,0,0,0,0,4,0,0> and the type of c
is N10<0,0,0,6,5,7,7,7,0,0>.
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 typelevel constraints to be written which run at compiletime
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 compiletime
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>
Release Notes
Add Name member.
Dependencies

 FSharp.Core (>= 4.3.4)
Used By
NuGet packages (3)
Showing the top 3 NuGet packages that depend on Sylvester.Arithmetic:
Package  Downloads 

Sylvester.tf
Highlevel functional and verifiable TensorFlow 2.0 API.


Sylvester.Collections
Sylvester numberparameterized collection types. These collection types can perform static verification of lengths and indices as long as some information about these values is available at compile time.


Sylvester.Tensors
Linear algebra types with typelevel numeric dimensions

GitHub repositories
This package is not used by any popular GitHub repositories.
Version History
Version  Downloads  Last updated 

0.2.5.1  188  2/6/2020 
0.2.5  194  2/6/2020 
0.2.4  344  1/16/2020 
0.2.3  162  1/16/2020 
0.2.2.1  451  1/3/2020 
0.2.2  185  1/3/2020 
0.2.1  196  12/30/2019 
0.2.0  181  12/30/2019 
0.1.7  211  6/23/2019 
0.1.6  205  6/22/2019 
0.1.5.1  234  6/21/2019 
0.1.3  200  6/12/2019 
0.1.2.2  202  6/10/2019 
0.1.2.1  212  6/10/2019 