Lightweight Dependent Types for Scientific Computing

Allister Beharry

About me

  • ### From Trinidad W.I.
In [4]:
uli2 "West Indies" "https://upload.wikimedia.org/wikipedia/commons/9/98/Caribbean_general_map.png"
Out[4]:

  • West Indies

In [31]:
uli2 "Indians came to Trinidad in the 19th century as indentured labourers" "https://thepeopleafterslavery.files.wordpress.com/2014/03/indentured-labourers-2.png"
Out[31]:

  • Indians came to Trinidad in the 19th century as indentured labourers

In [6]:
uli2 "Today Trinidad is multi-ethnic and multi-cultural" "http://currentriggers.com/wp-content/uploads/2016/11/4-17.jpg"
Out[6]:

  • Today Trinidad is multi-ethnic and multi-cultural

In [25]:
uli2 "Divali and other religious festivals celebrated by all" "https://www.guardian.co.tt/image-3.1974716.c274fa76ed?size=512"
Out[25]:

  • Divali and other religious festivals celebrated by all

In [9]:
uli2 "Cricket!" "https://akm-img-a-in.tosshub.com/indiatoday/images/story/201810/AP18297590913026.jpeg?P8W81HcX8oQiGA9xATv_s0lOWQKR3LH9"
Out[9]:

  • Cricket!

Sylvester

  • An F# DSL for scientific computing focused on safety, expressiveness, and interoperability
  • Take the best bits of typed functional programming and apply it to scientific and mathematical computing
  • Use F# features to create a more advanced type system for scientific computing

Why functional programming for scientific computing?

Scientific programming today

  • Dominated by C/C++, Fortran, Java, Matlab, Python, R, Julia,
  • Older languages are statically typed and procedural
  • Newer languages are dynamically typed and have object-oriented features
  • All are imperative languages that depend on mutable state and variables
  • Newer languages like Python and Julia rely heavily on meta-programming

F# Language Strengths

  • Functional first:
    • Everything is an expression
    • Functions as first-class citizens
    • Higher-order functions
    • Immutable variables
    • Avoid side-effects
    • Pattern matching
    • User-defined operators

F# Language Strengths

  • Best of both worlds:
    • Functional + object-oriented
    • Immutable + mutable variables
    • Static + dynamic types using the .NET DLR
  • Classes, interfaces, inheritance, polymorphism
  • Type extensibility with object expressions, extension methods
  • Powerful meta-programming capabilities: type providers, computation expressions
  • Interoperabilty - Can interoperate with any library or language with C FFI
    • C++, Python, Java
    • NumPy, Keras, TensorFlow, Torch

Example - Exploratory Data Analysis in F# using Sylvester

In [10]:
let titanic = new CsvFile("https://raw.githubusercontent.com/datasciencedojo/datasets/master/titanic.csv")
titanic.["Pclass"].First().Type <- typeof<int>
let dt = Frame(titanic)

query {
    for r in dt do
    groupBy r?Pclass into g
    sortBy g.Key
    select (
        let survived = (g.Where(fun p -> p?Survived = "1").Count()) |> float
        let died = (g.Where(fun p -> p?Survived = "0").Count()) |> float
        let ctotal = survived + died
        let psurvived = round(100.0 * survived / ctotal)
        let pdied = round(100.0 * died / ctotal) 
        (g.Key, pdied, psurvived)
)} |> Util.Table
Out[10]:
Item1Item2Item3
13763
25347
37624

F# Language Strengths

  • Built on .NET runtime and SDK
  • Comprehensive open-source tooling and environments - .NET Core / VS Code / Jupyter,...et.al
  • Huge open-source community providing libraries, resources, support
  • Microsoft fully committed to open source .NET and regularly releases libraries like ML.NET

We can use F# features to create more advanced type systems for scientific programming...

In [11]:
let v1 = Vec<1000>.Rand //Create a vector of length 1000
let v2 = Vec<500>.Rand //Create a vector of length 500
v1 + v2 //Can we do this?
Type constraint mismatch. The type 
    'Vector<float32,0,0,0,0,0,0,0,5,0,0>'    
is not compatible with type
    'Vector<float32,0,0,0,0,0,0,1,0,0,0>'    

Lightweight Dependent Types

Dependent types depend on values

  • E.g. A vector or array type that depends on its length
  • More advanced program verification than regular types
  • More errors can be caught before the program is run

Example

Full spectrum dependent types

  • Types can depend on most runtime values
  • Idris, Agda, ATS, F*....
  • Programmers write proof-carrying code

Full spectrum dependent types are cool...

The Future of Programming is Dependent Types... https://medium.com/background-thread/the-future-of-programming-is-dependent-types-programming-word-of-the-day-fcd5f2634878

Idris, a language that will change the way you think about programming...https://crufter.com/idris-a-language-that-will-change-the-way-you-think-about-programming

...but

  • Still a niche area in programming
  • Languages like Idris and ATS have a relatively small user community
  • Lack of tooling, libraries, resources, commercial support

Light-weight or restricted dependent typing

Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.

  • Values must be statically known before evaluation

Sylvester implements light-weight dependent typing for arrays, vectors, matrices, tensors...

  • Type-level arithmetic on natural number dimensions
    • Addition, subtraction, multiplication, equal to, greater than, et..al
  • Define function constraints which accept only objects of certain dimensions e.g only 3x3 real matrices
  • Define function constraints which accept objects with dimensions in a certain range e.g matrix functions that only accept square matrices
  • Sylvester can express type-level constraints and conditions simply without elaborate logical apparatus

Type-level programming vs. lightweight dependent typing

  • Many languages like C++ and D support type-level arithmetic
  • C++ can use static numeric values as template parameters
  • Both languages can use static checks and compiler asserts to do type level static checks

Lightweight dependent types

  • Types can vary with values and not simply fail statjc checks
  • Do not rely on compiler asserts
  • Types are part of the problem domain e.g. arithmetic, linear algebra
  • Rich set of type operators and constraints and checks e.g arithmetic comparison operators

(Lightweight) dependently-typed natural number arithmetic

In [14]:
// Create typed instance of some natural numbers
let a = new N<1000>()
let b = new N<900>()
a +< b
Out[14]:
Sylvester.Arithmetic.Bool+False
In [15]:
a +> b
Out[15]:
Sylvester.Arithmetic.Bool+True
In [16]:
a +!= b
Out[16]:
Sylvester.Arithmetic.Bool+True
In [17]:
a +== b
Out[17]:
Sylvester.Arithmetic.Bool+False
In [18]:
check((b * a) +== zero) //Causes type error
This expression was expected to have type
    'Success'    
but here has type
    'Failure'    
In [19]:
check ((a - b) +> zero) // But this is ok
In [21]:
zero - a //This results in another type, not a compiler error
Out[21]:
N10Underflow

(Lightweight) dependently-typed vectors and matrices

Example

In [ ]: