Sylvester.Arithmetic 0.2.8.1

.NET Standard 2.0 .NET Framework 4.5
dotnet add package Sylvester.Arithmetic --version 0.2.8.1
NuGet\Install-Package Sylvester.Arithmetic -Version 0.2.8.1
This command is intended to be used within the Package Manager Console in Visual Studio, as it uses the NuGet module's version of Install-Package.
<PackageReference Include="Sylvester.Arithmetic" Version="0.2.8.1" />
For projects that support PackageReference, copy this XML node into the project file to reference the package.
paket add Sylvester.Arithmetic --version 0.2.8.1
#r "nuget: Sylvester.Arithmetic, 0.2.8.1"
#r directive can be used in F# Interactive, C# scripting and .NET Interactive. Copy this into the interactive tool or source code of the script to reference the package.
// Install Sylvester.Arithmetic as a Cake Addin
#addin nuget:?package=Sylvester.Arithmetic&version=0.2.8.1

// Install Sylvester.Arithmetic as a Cake Tool
#tool nuget:?package=Sylvester.Arithmetic&version=0.2.8.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 compile-time by the F# type checker as long as the values for the operations are known at compile-time.

open Sylvester.Arithmetic

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

a + b + c
nat<6809211>

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
nat<27236844>
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
nat<25>
Product Versions
.NET net5.0 net5.0-windows net6.0 net6.0-android net6.0-ios net6.0-maccatalyst net6.0-macos net6.0-tvos net6.0-windows net7.0 net7.0-android net7.0-ios net7.0-maccatalyst net7.0-macos net7.0-tvos net7.0-windows
.NET Core netcoreapp2.0 netcoreapp2.1 netcoreapp2.2 netcoreapp3.0 netcoreapp3.1
.NET Standard netstandard2.0 netstandard2.1
.NET Framework net45 net451 net452 net46 net461 net462 net463 net47 net471 net472 net48
MonoAndroid monoandroid
MonoMac monomac
MonoTouch monotouch
Tizen tizen40 tizen60
Xamarin.iOS xamarinios
Xamarin.Mac xamarinmac
Xamarin.TVOS xamarintvos
Xamarin.WatchOS xamarinwatchos
Compatible target framework(s)
Additional computed target framework(s)
Learn more about Target Frameworks and .NET Standard.

NuGet packages (3)

Showing the top 3 NuGet packages that depend on Sylvester.Arithmetic:

Package Downloads
Sylvester.tf

High-level functional and verifiable TensorFlow 2.0 API.

Sylvester.Collections

Sylvester number-parameterized 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 type-level numeric dimensions

GitHub repositories

This package is not used by any popular GitHub repositories.

Version Downloads Last updated
0.2.8.1 279 5/11/2021
0.2.8 199 5/11/2021
0.2.7 252 3/8/2021
0.2.6.1 281 3/7/2021
0.2.6 276 3/7/2021
0.2.5.1 370 2/6/2020
0.2.5 378 2/6/2020
0.2.4 1,072 1/16/2020
0.2.3 343 1/16/2020
0.2.2.1 1,272 1/3/2020
0.2.2 358 1/3/2020
0.2.1 435 12/30/2019
0.2.0 359 12/30/2019
0.1.7 404 6/23/2019
0.1.6 461 6/22/2019
0.1.5.1 563 6/21/2019
0.1.3 410 6/12/2019
0.1.2.2 419 6/10/2019
0.1.2.1 429 6/10/2019

Move types and functions to module instead of namespace and remove unneeded code. Add max and min functions.