Sylvester.Arithmetic
0.2.5.1
Type-level natural number arithmetic and constraints using fixed-point decimal types.
Install-Package 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 compile-time by the F# type checker as long as the values for the operations are known at compile-time.
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 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 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
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 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>
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
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 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 |