Lightweight Dependent Types for Scientific Computing

FunConf 2019 presentation.ipynb

{
  "cells": [
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "<img src=\"http://fsharp.org/img/logo/fsharp512.png\" style=\"align:center\" />\n\n# Lightweight Dependent Types for Scientific Computing\n# Allister Beharry"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "skip"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "/// Setup MathJax and HTML helpers\n@\"<script src=\"\"https://raw.githubusercontent.com/mathjax/MathJax/master/latest.js?config=TeX-AMS-MML_CHTM\"\"></script>\" |> Util.Html |> Display\n\nlet html x = { Html = x }\n\nlet h1 text = { Html = \"<h1>\" + text + \"</h1>\" }\n\nlet h2 text = { Html = \"<h2>\" + text + \"</h2>\" }\n\nlet h3 text = { Html = \"<h3>\" + text + \"</h3>\" }\n\nlet ul text = { Html = \"<ul><li>\" + text + \"</li></ul>\" }\n\nlet ul3 text = { Html = \"<ul><li><h3>\" + text + \"</h3></li></ul>\" }\n\nlet img url = { Html = \"<img src=\\\"\" + url + \"\\\"\" + \" style=\\\"align:center\\\" />\" }\n\nlet uli text url = { Html = \"<ul><li>\" + text + \"<img src=\\\"\" + url + \"\\\"\" + \" style=\\\"align:center\\\" />\" + \"</li></ul>\" }\n\nlet uli2 text url = { Html = \"<h2><ul><li>\" + text + \"<img src=\\\"\" + url + \"\\\"\" + \" style=\\\"align:center\\\" />\" + \"</li></ul></h2>\" }\n\nlet uli3 text url = { Html = \"<h3><ul><li>\" + text + \"<img src=\\\"\" + url + \"\\\"\" + \" style=\\\"align:center\\\" />\" + \"</li></ul></h3>\" }\n\nlet inline (^+^) (x:HtmlOutput) (y:HtmlOutput) = { Html = x.Html + y.Html }",
      "execution_count": 1,
      "outputs": [
        {
          "output_type": "display_data",
          "data": {
            "text/html": "<script src=\"https://raw.githubusercontent.com/mathjax/MathJax/master/latest.js?config=TeX-AMS-MML_CHTM\"></script>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "skip"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "// Use the Sylvester.Tensors package from NuGet\n#load \"Paket.fsx\"\nPaket.Package[\"Sylvester.Arithmetic\"; \"Sylvester.Tensors\"; \"Sylvester.DataFrame\"; \"FSharp.Interop.Dynamic\"] \n#load \"Paket.Generated.Refs.fsx\"",
      "execution_count": 2,
      "outputs": []
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "skip"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "open System\nopen System.Collections.Generic\nopen System.Linq;\n\nopen FSharp.Interop.Dynamic\n\nopen Sylvester.Data\nopen Sylvester.Arithmetic\nopen Sylvester.Arithmetic.N10\nopen Sylvester.Arithmetic.Collections\nopen Sylvester.Tensors",
      "execution_count": 20,
      "outputs": []
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "# About me\n\n"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "* ### From Trinidad W.I."
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        },
        "trusted": true,
        "hide_input": true
      },
      "cell_type": "code",
      "source": "uli2 \"West Indies\" \"https://upload.wikimedia.org/wikipedia/commons/9/98/Caribbean_general_map.png\"",
      "execution_count": 4,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 4,
          "data": {
            "text/html": "<h2><ul><li>West Indies<img src=\"https://upload.wikimedia.org/wikipedia/commons/9/98/Caribbean_general_map.png\" style=\"align:center\" /></li></ul></h2>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        },
        "trusted": true,
        "hide_input": true
      },
      "cell_type": "code",
      "source": "uli2 \"Indians came to Trinidad in the 19th century as indentured labourers\" \"https://thepeopleafterslavery.files.wordpress.com/2014/03/indentured-labourers-2.png\"",
      "execution_count": 31,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 31,
          "data": {
            "text/html": "<h2><ul><li>Indians came to Trinidad in the 19th century as indentured labourers<img src=\"https://thepeopleafterslavery.files.wordpress.com/2014/03/indentured-labourers-2.png\" style=\"align:center\" /></li></ul></h2>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "trusted": true,
        "slideshow": {
          "slide_type": "subslide"
        },
        "hide_input": true
      },
      "cell_type": "code",
      "source": "uli2 \"Today Trinidad is multi-ethnic and multi-cultural\" \"http://currentriggers.com/wp-content/uploads/2016/11/4-17.jpg\"",
      "execution_count": 6,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 6,
          "data": {
            "text/html": "<h2><ul><li>Today Trinidad is multi-ethnic and multi-cultural<img src=\"http://currentriggers.com/wp-content/uploads/2016/11/4-17.jpg\" style=\"align:center\" /></li></ul></h2>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "trusted": true,
        "hide_input": true,
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "code",
      "source": "uli2 \"Divali and other religious festivals celebrated by all\" \"https://www.guardian.co.tt/image-3.1974716.c274fa76ed?size=512\"",
      "execution_count": 25,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 25,
          "data": {
            "text/html": "<h2><ul><li>Divali and other religious festivals celebrated by all<img src=\"https://www.guardian.co.tt/image-3.1974716.c274fa76ed?size=512\" style=\"align:center\" /></li></ul></h2>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "trusted": true,
        "slideshow": {
          "slide_type": "subslide"
        },
        "hide_input": true
      },
      "cell_type": "code",
      "source": "uli2 \"Cricket!\" \"https://akm-img-a-in.tosshub.com/indiatoday/images/story/201810/AP18297590913026.jpeg?P8W81HcX8oQiGA9xATv_s0lOWQKR3LH9\"",
      "execution_count": 9,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 9,
          "data": {
            "text/html": "<h2><ul><li>Cricket!<img src=\"https://akm-img-a-in.tosshub.com/indiatoday/images/story/201810/AP18297590913026.jpeg?P8W81HcX8oQiGA9xATv_s0lOWQKR3LH9\" style=\"align:center\" /></li></ul></h2>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "# About Sylvester project\n\n## https://github.com/allisterb/Sylvester\n"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Sylvester\n* An F# DSL for scientific computing focused on safety, expressiveness, and interoperability\n* Take the best bits of typed functional programming and apply it to scientific and mathematical computing\n* Use F# features to create a more advanced type system for scientific computing"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "# Why functional programming for scientific computing?"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Scientific programming today\n* Dominated by C/C++, Fortran, Java, Matlab, Python, R, Julia,  \n* Older languages are statically typed and procedural\n* Newer languages are dynamically typed and have object-oriented features\n* All are imperative languages that depend on mutable state and variables\n* Newer languages like Python and Julia rely heavily on meta-programming"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## F# Language Strengths\n* Functional first: \n    - Everything is an expression\n    - Functions as first-class citizens\n    - Higher-order functions\n    - Immutable variables\n    - Avoid side-effects\n    - Pattern matching\n    - User-defined operators"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## F# Language Strengths\n* Best of both worlds: \n    - Functional + object-oriented\n    - Immutable + mutable variables\n    - Static + dynamic types using the .NET DLR\n* Classes, interfaces, inheritance, polymorphism\n* Type extensibility with object expressions, extension methods\n* Powerful meta-programming capabilities: type providers, computation expressions\n* Interoperabilty - Can interoperate with any library or language with C FFI\n    - C++, Python, Java  \n    - NumPy, Keras, TensorFlow, Torch"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Example - Exploratory Data Analysis in F# using Sylvester"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "let titanic = new CsvFile(\"https://raw.githubusercontent.com/datasciencedojo/datasets/master/titanic.csv\")\ntitanic.[\"Pclass\"].First().Type <- typeof<int>\nlet dt = Frame(titanic)\n\nquery {\n    for r in dt do\n    groupBy r?Pclass into g\n    sortBy g.Key\n    select (\n        let survived = (g.Where(fun p -> p?Survived = \"1\").Count()) |> float\n        let died = (g.Where(fun p -> p?Survived = \"0\").Count()) |> float\n        let ctotal = survived + died\n        let psurvived = round(100.0 * survived / ctotal)\n        let pdied = round(100.0 * died / ctotal) \n        (g.Key, pdied, psurvived)\n)} |> Util.Table",
      "execution_count": 10,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 10,
          "data": {
            "text/html": "<table><thead><tr><th>Item1</th><th>Item2</th><th>Item3</th></tr></thead><tbody><tr><td>1</td><td>37</td><td>63</td></tr><tr><td>2</td><td>53</td><td>47</td></tr><tr><td>3</td><td>76</td><td>24</td></tr><tbody></tbody></table>"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## F# Language Strengths\n* Built on .NET runtime and SDK \n* Comprehensive open-source tooling and environments - .NET Core / VS Code / Jupyter,...et.al\n* Huge open-source community providing libraries, resources, support\n* Microsoft fully committed to open source .NET and regularly releases libraries like ML.NET "
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": " # We can use F# features to create more advanced type systems for scientific programming..."
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "let v1 = Vec<1000>.Rand //Create a vector of length 1000\nlet v2 = Vec<500>.Rand //Create a vector of length 500\nv1 + v2 //Can we do this?",
      "execution_count": 11,
      "outputs": [
        {
          "output_type": "stream",
          "text": "Type constraint mismatch. The type \n    'Vector<float32,0,0,0,0,0,0,0,5,0,0>'    \nis not compatible with type\n    'Vector<float32,0,0,0,0,0,0,1,0,0,0>'    \n",
          "name": "stderr"
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "# Lightweight Dependent Types"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Dependent types depend on values\n* E.g. A vector or array type that depends on its length\n* More advanced program verification than regular types\n* More errors can be caught before the program is run"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Example "
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Full spectrum dependent types\n\n* Types can depend on most *runtime* values \n* Idris, Agda, ATS, F*....\n* Programmers write proof-carrying code\n"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        },
        "trusted": true
      },
      "cell_type": "markdown",
      "source": "## Full spectrum dependent types are cool...\n\n>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\n\n>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\n"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "...but "
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "* Still a niche area in programming\n* Languages like Idris and ATS have a relatively small user community\n* Lack of tooling, libraries, resources, commercial support"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## Light-weight or restricted dependent typing\n* http://okmij.org/ftp/Computation/lightweight-dependent-typing.html\n* Attempt to bring safety benefits of dependent typing to mainstream languages\n* Began with Dependent ML - precursor to ATS"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "> 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."
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "* Values must be statically known before evaluation  "
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "## Sylvester implements light-weight dependent typing for arrays, vectors, matrices, tensors..."
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        }
      },
      "cell_type": "markdown",
      "source": "* Type-level arithmetic on natural number dimensions\n    - Addition, subtraction, multiplication, equal to, greater than, et..al\n* Define function constraints which accept only objects of certain dimensions e.g only 3x3 real matrices\n* Define function constraints which accept objects with dimensions in a certain range e.g matrix functions that only accept square matrices\n*  Sylvester can express type-level constraints and conditions simply without elaborate logical apparatus"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "### Type-level programming vs. lightweight dependent typing\n* Many languages like C++ and D support type-level arithmetic\n* C++ can use static numeric values as template parameters\n* Both languages can use static checks and compiler asserts to do type level static checks"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "### Lightweight dependent types\n* Types can vary with values and not simply fail statjc checks \n* Do not rely on compiler asserts\n* Types are part of the problem domain e.g. arithmetic, linear algebra\n* Rich set of type operators and constraints and checks e.g arithmetic comparison operators"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "## (Lightweight) dependently-typed natural number arithmetic"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "// Create typed instance of some natural numbers\nlet a = new N<1000>()\nlet b = new N<900>()\na +< b",
      "execution_count": 14,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 14,
          "data": {
            "text/plain": "Sylvester.Arithmetic.Bool+False"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "a +> b",
      "execution_count": 15,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 15,
          "data": {
            "text/plain": "Sylvester.Arithmetic.Bool+True"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "a +!= b",
      "execution_count": 16,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 16,
          "data": {
            "text/plain": "Sylvester.Arithmetic.Bool+True"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "a +== b",
      "execution_count": 17,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 17,
          "data": {
            "text/plain": "Sylvester.Arithmetic.Bool+False"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "check((b * a) +== zero) //Causes type error",
      "execution_count": 18,
      "outputs": [
        {
          "output_type": "stream",
          "text": "This expression was expected to have type\n    'Success'    \nbut here has type\n    'Failure'    ",
          "name": "stderr"
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "check ((a - b) +> zero) // But this is ok",
      "execution_count": 19,
      "outputs": []
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "fragment"
        },
        "trusted": true
      },
      "cell_type": "code",
      "source": "zero - a //This results in another type, not a compiler error",
      "execution_count": 21,
      "outputs": [
        {
          "output_type": "execute_result",
          "execution_count": 21,
          "data": {
            "text/plain": "N10Underflow"
          },
          "metadata": {}
        }
      ]
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "## (Lightweight) dependently-typed vectors and matrices"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "subslide"
        }
      },
      "cell_type": "markdown",
      "source": "### Example"
    },
    {
      "metadata": {
        "slideshow": {
          "slide_type": "slide"
        }
      },
      "cell_type": "markdown",
      "source": "\n## https://github.com/allisterb/Sylvester\n\n## @allisterbeharry"
    },
    {
      "metadata": {
        "trusted": true
      },
      "cell_type": "code",
      "source": "",
      "execution_count": null,
      "outputs": []
    }
  ],
  "metadata": {
    "kernelspec": {
      "name": "ifsharp",
      "display_name": "F#",
      "language": "fsharp"
    },
    "language_info": {
      "mimetype": "text/x-fsharp",
      "nbconvert_exporter": "",
      "name": "fsharp",
      "pygments_lexer": "",
      "version": "4.3.1.0",
      "file_extension": ".fs",
      "codemirror_mode": ""
    },
    "language": "fsharp",
    "celltoolbar": "Slideshow"
  },
  "nbformat": 4,
  "nbformat_minor": 2
}