Sylvester.Arithmetic 0.2.8

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>