docs/HolisticProjections.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Holistic Projections"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mimport \u001b[36mjava.text.SimpleDateFormat\u001b[0m\n",
       "\u001b[32mimport \u001b[36mjava.util.{Date, Locale}\u001b[0m"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import java.text.SimpleDateFormat\n",
    "import java.util.{Date, Locale}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Projections are associated with product types (see the [Wiki](https://en.wikipedia.org/wiki/Product_%28category_theory%29) article)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[36mdf\u001b[0m: \u001b[32mSimpleDateFormat\u001b[0m = java.text.SimpleDateFormat@f84b7e00\n",
       "defined \u001b[32mclass \u001b[36mPerson\u001b[0m"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "val df = new SimpleDateFormat(\"yyyy-mm-dd\", Locale.ENGLISH)\n",
    "case class Person(name: String, surname: String, birthday: Date)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Product types of size $N$ can be constructed by passing $N$ arguments to the companion constructor."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[36mp\u001b[0m: \u001b[32mPerson\u001b[0m = \u001b[33mPerson\u001b[0m(\u001b[32m\"John\"\u001b[0m, \u001b[32m\"Doe\"\u001b[0m, Fri Jan 27 00:04:00 CET 1961)\n",
       "\u001b[36mn\u001b[0m: \u001b[32mString\u001b[0m = \u001b[32m\"John\"\u001b[0m"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "val p = Person(\"John\", \"Doe\", df.parse(\"1961-04-27\"))\n",
    "val n = p.name"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In LNF, the above expression will have a val (with an associated symbol) for each sub-expression."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[36mx1\u001b[0m: \u001b[32mString\u001b[0m = \u001b[32m\"John\"\u001b[0m\n",
       "\u001b[36mx2\u001b[0m: \u001b[32mString\u001b[0m = \u001b[32m\"Doe\"\u001b[0m\n",
       "\u001b[36mx3\u001b[0m: \u001b[32mString\u001b[0m = \u001b[32m\"1961-04-27\"\u001b[0m\n",
       "\u001b[36mx4\u001b[0m: \u001b[32mDate\u001b[0m = Fri Jan 27 00:04:00 CET 1961\n",
       "\u001b[36mp1\u001b[0m: \u001b[32mPerson\u001b[0m = \u001b[33mPerson\u001b[0m(\u001b[32m\"John\"\u001b[0m, \u001b[32m\"Doe\"\u001b[0m, Fri Jan 27 00:04:00 CET 1961)\n",
       "\u001b[36mn1\u001b[0m: \u001b[32mString\u001b[0m = \u001b[32m\"John\"\u001b[0m"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "val x1 = \"John\"\n",
    "val x2 = \"Doe\"\n",
    "val x3 = \"1961-04-27\"\n",
    "val x4 = df.parse(x3)\n",
    "val p1 = Person(x1, x2, x4)\n",
    "val n1 = p.name"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Based on the categorical definition of a product, we can infer that the following equations hold in the above example."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": []
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "assert( p1.name     == x1 )\n",
    "assert( p1.surname  == x2 )\n",
    "assert( p1.birthday == x4 )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Based on that, and the aditional equations of the form `val s = p1.proj` occurring in the ANF form, we can infer the following equivalence classes of symbols."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\\begin{equation}\n",
    "\\{ x_1, n_1 \\} \\\\\n",
    "\\{ x_2 \\} \\\\\n",
    "\\{ x_4 \\} \\\\\n",
    "\\end{equation}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The first thing that we want to do is to implement an analysis function that computes equivalence classes like in the exmaple above. \n",
    "\n",
    "One implementation approach can be based on the following steps:\n",
    "\n",
    "1. Do a code pass in order to compute\n",
    "  * the initial set of fields $S$, as well as \n",
    "  * the set of equivalences over those fields that can be inferred based on the code and the prodcut type axioms.\n",
    "1. Compute the transitive closure $S^*$ of $S$.\n",
    "\n",
    "Things can get complicated due to the following aspects.  \n",
    "\n",
    "* Nested product types, e.g. `(Int, (Double, String))`.\n",
    "* Second-order function semantics, e.g. in chains of $\\mathsf{map}$ applications."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Scala 2.11",
   "language": "scala211",
   "name": "scala211"
  },
  "language_info": {
   "codemirror_mode": "text/x-scala",
   "file_extension": ".scala",
   "mimetype": "text/x-scala",
   "name": "scala211",
   "pygments_lexer": "scala",
   "version": "2.11.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}